mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e e' : OpenPartialHomeomorph (B × F) (B × F)),
    e ∈
        ⋃ φ,
          ⋃ U,
            ⋃ (hU : IsOpen[inst✝⁷] U),
              ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                  {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} →
      e' ∈
          ⋃ φ,
            ⋃ U,
              ⋃ (hU : IsOpen[inst✝⁷] U),
                ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                  ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                    {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} →
        e ≫ₕ e' ∈
          ⋃ φ,
            ⋃ U,
              ⋃ (hU : IsOpen[inst✝⁷] U),
                ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                  ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                    {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
simp only [mem_aux]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e e' : OpenPartialHomeomorph (B × F) (B × F)),
    (∃ φ U,
        ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
          ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
      (∃ φ U,
          ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
            e'.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
        ∃ φ U,
          ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
            (e ≫ₕ e').EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
inst✝ : Subsingleton E
⊢ MDiff f

Tactic:
intro x
  have : Subsingleton H := I.injective.subsingleton
  have : DiscreteTopology M := discreteTopology H M
  simp only [mdifferentiableAt_iff, continuous_of_discreteTopology.continuousAt, true_and]
  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
⊢ e ∈
      ⋃ φ,
        ⋃ U,
          ⋃ (hU : IsOpen[inst✝⁷] U),
            ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
              ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} →
    e.symm ∈
      ⋃ φ,
        ⋃ U,
          ⋃ (hU : IsOpen[inst✝⁷] U),
            ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
              ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
simp only [mem_aux]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
⊢ (∃ φ U,
      ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
        ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
        e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
    ∃ φ U,
      ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
        ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
        e.symm.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : F
⊢ (Pretrivialization.symmₗ R e b) y = e.symm b y

Tactic:
simp [Pretrivialization.symmₗ, hb]

Goal state after:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∉ e.baseSet
y : F
⊢ (Pretrivialization.symmₗ R e b) y = 0

Tactic:
simp [Pretrivialization.symmₗ, hb]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e : OpenPartialHomeomorph (B × F) (B × F)),
    (∀ x ∈ e.source,
        ∃ s,
          IsOpen[instTopologicalSpaceProd] s ∧
            x ∈ s ∧
              e.restr s ∈
                ⋃ φ,
                  ⋃ U,
                    ⋃ (hU : IsOpen[inst✝⁷] U),
                      ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                        ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                          {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}) →
      e ∈
        ⋃ φ,
          ⋃ U,
            ⋃ (hU : IsOpen[inst✝⁷] U),
              ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                  {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
simp only [mem_aux]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e : OpenPartialHomeomorph (B × F) (B × F)),
    (∀ x ∈ e.source,
        ∃ s,
          IsOpen[instTopologicalSpaceProd] s ∧
            x ∈ s ∧
              ∃ φ U,
                ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
                  ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                  (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
      ∃ φ U,
        ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
          ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : HasMFDerivAt[s] f x 0
⊢ mfderiv[s] f x = 0

Tactic:
by
  simp only [mfld_simps, mfderivWithin, h.mdifferentiableWithinAt, ↓reduceIte]
  simp only [HasMFDerivWithinAt, mfld_simps] at h
  rw [fderivWithin, if_pos]
  exact h.2

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e e' : OpenPartialHomeomorph (B × F) (B × F)),
    e ∈
        ⋃ φ,
          ⋃ U,
            ⋃ (hU : IsOpen[inst✝⁷] U),
              ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                  {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} →
      e' ≈ e →
        e' ∈
          ⋃ φ,
            ⋃ U,
              ⋃ (hU : IsOpen[inst✝⁷] U),
                ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                  ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                    {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
simp only [mem_aux]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e e' : OpenPartialHomeomorph (B × F) (B × F)),
    (∃ φ U,
        ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
          ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
      e' ≈ e →
        ∃ φ U,
          ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
            e'.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
Module: Mathlib.Topology.VectorBundle.Constructions

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹² : TopologicalSpace B'
inst✝¹¹ : TopologicalSpace (TotalSpace F E)
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : (x : B) → AddCommMonoid (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝⁴ : FunLike K B' B
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
⊢ ∀ (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e], Trivialization.IsLinear 𝕜 e

Tactic:
rintro _ ⟨e, he, rfl⟩
    infer_instance

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ (mfderiv% fun x ↦ (f x, g x)) x = (mfderiv% f x).prod (mfderiv% g x)

Tactic:
simp_rw [← mfderivWithin_univ]
  exact mfderivWithin_prodMk hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I)

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case h₁
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    writtenInExtChartAt I I' x f

pp: case hx
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ (↑(extChartAt I x) x) = writtenInExtChartAt I I' x f (↑(extChartAt I x) x)

Tactic:
· have :
      (extChartAt I x).symm ⁻¹' {y | f₁ y = f y} ∈
        𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
      extChartAt_preimage_mem_nhdsWithin h₁
    apply Filter.mem_of_superset this fun y => _
    simp +contextual only [hx, mfld_simps]

Goal state after:
case hx
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ (↑(extChartAt I x) x) = writtenInExtChartAt I I' x f (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv[s] Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁶ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
inst✝¹⁰ : (x : B) → AddCommMonoid (E x)
inst✝⁹ : (x : B) → Module 𝕜 (E x)
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → TopologicalSpace (E x)
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle n F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph)) (e.target ∩ e'.target)

Tactic:
refine (contMDiffOn_fst.prodMk
    (contMDiffOn_fst.coordChange contMDiffOn_snd Hmaps.1 Hmaps.2)).congr ?_

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁶ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
inst✝¹⁰ : (x : B) → AddCommMonoid (E x)
inst✝⁹ : (x : B) → Module 𝕜 (E x)
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → TopologicalSpace (E x)
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle n F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) e.baseSet ∧ MapsTo Prod.fst (e.target ∩ e'.target) e'.baseSet
⊢ ∀ y ∈ e.target ∩ e'.target, ↑(e.symm ≫ₕ e'.toOpenPartialHomeomorph) y = (y.1, e.coordChange e' y.1 y.2)
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
p : TangentBundle I M
hg : MDiffAt g (f p.proj)
hf : MDiffAt f p.proj
⊢ (mfderiv% (g ∘ f) p.proj) p.snd = (mfderiv% g (f p.proj)) ((mfderiv% f p.proj) p.snd)

Tactic:
mfderiv_comp p.1 hg hf

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
g : M' → M''
p : TangentBundle I M
hg : MDiffAt g (f p.proj)
hf : MDiffAt f p.proj
⊢ (mfderiv% g (f p.proj) ∘SL mfderiv% f p.proj) p.snd = (mfderiv% g (f p.proj)) ((mfderiv% f p.proj) p.snd)
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p : H × E
q : TM
⊢ p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.proj).target

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]
  rw [PartialEquiv.prod_symm]
  simp +contextual only [and_iff_left_iff_imp, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ MDiffAt ↑(extChartAt I x) (↑(extChartAt I x).symm y)

Tactic:
apply mdifferentiableAt_extChartAt h''y

Goal state after:
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁶ : NormedAddCommGroup E'
inst✝¹⁵ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
H : Type u_5
inst✝¹² : TopologicalSpace H
H' : Type u_6
inst✝¹¹ : TopologicalSpace H'
G : Type u_7
inst✝¹⁰ : TopologicalSpace G
G' : Type u_8
inst✝⁹ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_10
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
N : Type u_11
inst✝⁴ : TopologicalSpace N
inst✝³ : ChartedSpace G N
N' : Type u_12
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] F
inst✝ : IsManifold I n M
⊢ IsManifold (I.transContinuousLinearEquiv e) n M

Tactic:
by
  refine isManifold_of_contDiffOn (I.transContinuousLinearEquiv e) n M fun e₁ e₂ h₁ h₂ => ?_
  refine e.contDiff.comp_contDiffOn
      (((contDiffGroupoid n I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn ?_)
  simp [preimage_comp, range_comp, mapsTo_iff_subset_preimage,
    ContinuousLinearEquiv.image_eq_preimage_symm]

Goal state after: