mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 n (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ ContDiffWithinAt 𝕜 m (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
convert! (this.of_le hmn).comp _ h _

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 n (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ ↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm = (↑I' ∘ ↑e' ∘ ↑I'.symm) ∘ ↑I' ∘ f ∘ ↑I.symm

𝕜 : 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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 n (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ MapsTo (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I'.symm ⁻¹' e'.source ∩ range ↑I')
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: case pos
𝕜 : 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
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
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∈ interior s
⊢ ContMDiffAt I I' n (s.piecewise f g) x

Tactic:
apply (hf x).congr_of_eventuallyEq
    filter_upwards [isOpen_interior.mem_nhds hx] with y hy
    rw [piecewise_eq_of_mem]
    apply interior_subset hy

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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
inst✝ : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst✝⁶] (s i)
hs' : ⋃ i, s i = univ
⊢ ContMDiff I I' n f

Tactic:
rw [← contMDiffOn_univ, ← hs']
  exact ContMDiffOn.iUnion_of_isOpen hf hs

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
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst✝³] U
hφ : ContinuousOn (fun x ↦ ↑(φ x)) U
h2φ : ContinuousOn (fun x ↦ ↑(φ x).symm) U
hU' : IsOpen[inst✝³] U'
hφ' : ContinuousOn (fun x ↦ ↑(φ' x)) U'
h2φ' : ContinuousOn (fun x ↦ ↑(φ' x).symm) U'
⊢ (openPartialHomeomorph φ hU hφ h2φ ≫ₕ openPartialHomeomorph φ' hU' hφ' h2φ').source = (U ∩ U') ×ˢ univ

Tactic:
dsimp only [FiberwiseLinear.openPartialHomeomorph]

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
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst✝³] U
hφ : ContinuousOn (fun x ↦ ↑(φ x)) U
h2φ : ContinuousOn (fun x ↦ ↑(φ x).symm) U
hU' : IsOpen[inst✝³] U'
hφ' : ContinuousOn (fun x ↦ ↑(φ' x)) U'
h2φ' : ContinuousOn (fun x ↦ ↑(φ' x).symm) U'
⊢ ({ toFun := fun x ↦ (x.1, (φ x.1) x.2), invFun := fun x ↦ (x.1, (φ x.1).symm x.2), source := U ×ˢ univ,
          target := U ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ } ≫ₕ
        { toFun := fun x ↦ (x.1, (φ' x.1) x.2), invFun := fun x ↦ (x.1, (φ' x.1).symm x.2), source := U' ×ˢ univ,
          target := U' ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }).source =
    (U ∩ U') ×ˢ univ
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
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst✝³] U
hφ : ContinuousOn (fun x ↦ ↑(φ x)) U
h2φ : ContinuousOn (fun x ↦ ↑(φ x).symm) U
hU' : IsOpen[inst✝³] U'
hφ' : ContinuousOn (fun x ↦ ↑(φ' x)) U'
h2φ' : ContinuousOn (fun x ↦ ↑(φ' x).symm) U'
⊢ (openPartialHomeomorph φ hU hφ h2φ ≫ₕ openPartialHomeomorph φ' hU' hφ' h2φ').target = (U ∩ U') ×ˢ univ

Tactic:
dsimp only [FiberwiseLinear.openPartialHomeomorph]

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
φ φ' : B → F ≃L[𝕜] F
U U' : Set B
hU : IsOpen[inst✝³] U
hφ : ContinuousOn (fun x ↦ ↑(φ x)) U
h2φ : ContinuousOn (fun x ↦ ↑(φ x).symm) U
hU' : IsOpen[inst✝³] U'
hφ' : ContinuousOn (fun x ↦ ↑(φ' x)) U'
h2φ' : ContinuousOn (fun x ↦ ↑(φ' x).symm) U'
⊢ ({ toFun := fun x ↦ (x.1, (φ x.1) x.2), invFun := fun x ↦ (x.1, (φ x.1).symm x.2), source := U ×ˢ univ,
          target := U ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ } ≫ₕ
        { toFun := fun x ↦ (x.1, (φ' x.1) x.2), invFun := fun x ↦ (x.1, (φ' x.1).symm x.2), source := U' ×ˢ univ,
          target := U' ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
          continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }).target =
    (U ∩ U') ×ˢ univ
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: case refine_2
𝕜 : 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)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ
hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p
heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source
he : e.source = (Prod.fst '' e.source) ×ˢ univ
p : B × F
hp : p ∈ e.source
⊢ (e.restr (s ⟨p, hp⟩)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ ⟨p, hp⟩) ⋯ ⋯ ⋯)

Tactic:
exact heφ ⟨p, hp⟩

Goal state after:
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:
by
  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.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : y ∈ (⇑f ⁻¹' e.baseSet) ×ˢ univ
⊢ TotalSpace.mk' F y.1 (e.symm (f y.1) y.2) ∈ Pullback.lift ⇑f ⁻¹' e.source

Tactic:
by
    rw [mem_prod, mem_preimage] at h
    simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]

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

Goal state before:
pp: case pos
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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸]
    (↑(if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
        else LinearEquiv.refl R F)).toFun

Tactic:
dif_pos hb

Goal state after:
case pos
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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸] (↑((linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯)).toFun
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case pos
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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸]
    (if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
      else LinearEquiv.refl R F).invFun

Tactic:
dif_pos hb

Goal state after:
case pos
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✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸] ((linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯).invFun
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j k : ι
x : B
hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k
⊢ Z.coordChange j k x ∘SL Z.coordChange i j x = Z.coordChange i k x

Tactic:
by
  ext v
  exact Z.coordChange_comp i j k x hx v

Goal state after:
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 t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasMFDerivAt[s] f x f' ↔ HasMFDerivAt[t] f x f'

Tactic:
have : T1Space M := I.t1Space M
  simp only [HasMFDerivWithinAt]
  refine and_congr ?_ ?_
  · exact continuousWithinAt_congr_set' _ h
  · apply hasFDerivWithinAt_congr_set' (extChartAt I x x)
    exact preimage_extChartAt_eventuallyEq_compl_singleton y h

Goal state after:
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 t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ mfderiv[s] f x = mfderiv[t] f x

Tactic:
by
  by_cases hx : MDiffAt[s] f x
  · simp only [mfderivWithin, hx, (mdifferentiableWithinAt_congr_set' y h).1 hx, ↓reduceIte]
    apply fderivWithin_congr_set' (extChartAt I x x)
    exact preimage_extChartAt_eventuallyEq_compl_singleton y h
  · simp [mfderivWithin, hx, ← mdifferentiableWithinAt_congr_set' y h]

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

Goal state before:
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
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ (↑(extChartAt I' (f₁ x)) ∘ f₁ ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) =
    (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

pp: case pos.hs
𝕜 : 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
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ ↑(extChartAt I' (f₁ x)) ∘
      f₁ ∘ ↑(extChartAt I x).symm =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm

Tactic:
· simp [hx]

Goal state after:
case pos.hs
𝕜 : 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
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ ↑(extChartAt I' (f₁ x)) ∘
      f₁ ∘ ↑(extChartAt I x).symm =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    ↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm
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 x' : M
h : x = x'
⊢ mfderiv% f x = mfderiv% f x'

Tactic:
subst h; rfl

Goal state after:
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
f' : M → M'
h : f = f'
⊢ mfderiv% f x = mfderiv% f' x

Tactic:
subst h; rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : ℕ∞ω
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 (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ (ModelWithCorners.extendCoordChange ↑i ↑j).source ∈ 𝓝[range ↑I] x

Tactic:
exact I.extendCoordChange_source_mem_nhdsWithin hx

Goal state after:
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'
x : M
g : M' → M''
y : M'
hg : MDiffAt g y
hf : MDiffAt f x
hy : f x = y
⊢ MDiffAt (g ∘ f) x

Tactic:
subst hy; exact hg.comp _ hf

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

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
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
⊢ mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm y =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
← mfderiv_comp_mfderivWithin

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
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
⊢ mfderiv[range ↑I] (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

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)

case hf
𝕜 : 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[range ↑I] ↑(extChartAt I x).symm y

case hxs
𝕜 : 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
⊢ UniqueMDiffAt[range ↑I] y