awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E')) ((↑(extChartAt I' (f x)) : M' → E') (f x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst : s ⊆ f ⁻¹' u
this_1 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
hg₁ :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
      (writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x))
hf₁ :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst₁ : s ⊆ f ⁻¹' u
this₁ :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)

Tactic:
rw [← this] at hg
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
      (writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst : s ⊆ f ⁻¹' u
this_1 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
apply :
  MapsTo (writtenInExtChartAt I I' x f)
    ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
    ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
⊢ HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
apply HasFDerivWithinAt.comp ((extChartAt I x) x) hg.2 hf.2 _

Premises used: extChartAt, HasFDerivWithinAt.comp, And.right, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
      (writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst : s ⊆ f ⁻¹' u
this_1 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
y : E
hy : y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)
⊢ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∧
    y ∈ range (↑I : H → E)

Tactic:
simp only [mfld_simps] at hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
      (writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst : s ⊆ f ⁻¹' u
this_1 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
y : E
hy :
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∧
    y ∈ range (↑I : H → E)
⊢ f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)) ∈ u

Tactic:
have : f (((chartAt H x).symm : H → M) (I.symm y)) ∈ u := hst hy.1.1
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g'
      ((↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E'))
      (writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
hst : s ⊆ f ⁻¹' u
this_1 :
  (↑(extChartAt I x).symm : E → M) ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
this_2 : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
y : E
hy :
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∧
    y ∈ range (↑I : H → E)
this : f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) y)) ∈ u
⊢ writtenInExtChartAt I I' x f y ∈ (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' u ∩ range (↑I' : H' → E')

Tactic:
simp only [hy, this, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g u (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
hst : s ⊆ f ⁻¹' u
⊢ HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
have A :
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f)
      (ContinuousLinearMap.comp g' f' : E →L[𝕜] E'') ((extChartAt I x).symm ⁻¹' s ∩ range I)
      ((extChartAt I x) x) := by
    have :
      (extChartAt I x).symm ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
        𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
      extChartAt_preimage_mem_nhdsWithin
        (hf.1.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _))
    unfold HasMFDerivWithinAt at *
    rw [← hasFDerivWithinAt_inter' this, ← extChartAt_preimage_inter_eq] at hf ⊢
    have : writtenInExtChartAt I I' x f ((extChartAt I x) x) = (extChartAt I' (f x)) (f x) := by
      simp only [mfld_simps]
    rw [← this] at hg
    apply HasFDerivWithinAt.comp ((extChartAt I x) x) hg.2 hf.2 _
    intro y hy
    simp only [mfld_simps] at hy
    have : f (((chartAt H x).symm : H → M) (I.symm y)) ∈ u := hst hy.1.1
    simp only [hy, this, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g u (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
hst : s ⊆ f ⁻¹' u
A :
  HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
apply :
  writtenInExtChartAt I I'' x (g ∘ f) ((↑(extChartAt I x) : M → E) x) =
    (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I'' x (g ∘ f)) (g' ∘SL f')
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
apply A.congr_of_eventuallyEq (writtenInExtChartAt_comp hf.1)

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, And.left, writtenInExtChartAt_comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g u (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
hst : s ⊆ f ⁻¹' u
A :
  HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g' ∘SL f')
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ writtenInExtChartAt I I'' x (g ∘ f) ((↑(extChartAt I x) : M → E) x) =
    (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivAt I' I'' g (f x) g'
hf : HasMFDerivAt I I' f x f'
rw :
  ∀ (hg : HasMFDerivWithinAt I' I'' g univ (f x) g') (hf : HasMFDerivWithinAt I I' f univ x f'),
    HasMFDerivWithinAt I I'' (g ∘ f) univ x (g' ∘SL f')
⊢ HasMFDerivAt I I'' (g ∘ f) x (g' ∘SL f')

Tactic:
rw [← hasMFDerivWithinAt_univ] at *

Premises used: hasMFDerivWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g univ (f x) g'
hf : HasMFDerivWithinAt I I' f univ x f'
⊢ HasMFDerivWithinAt I I'' (g ∘ f) univ x (g' ∘SL f')

Tactic:
HasMFDerivWithinAt.comp x (hg.mono (subset_univ _)) hf subset_preimage_univ

Premises used: Set.subset_univ, Set.subset_preimage_univ, HasMFDerivWithinAt.mono, HasMFDerivWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g univ (f x) g'
hf : HasMFDerivWithinAt I I' f univ x f'
⊢ HasMFDerivWithinAt I I'' (g ∘ f) univ x (g' ∘SL f')

Tactic:
exact HasMFDerivWithinAt.comp x (hg.mono (subset_univ _)) hf subset_preimage_univ

Premises used: Set.subset_univ, Set.subset_preimage_univ, HasMFDerivWithinAt.mono, HasMFDerivWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivAt I' I'' g (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I' I'' g univ (f x) g'

Tactic:
rw [← hasMFDerivWithinAt_univ] at *

Premises used: hasMFDerivWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivAt I' I'' g (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
hg₁ : HasMFDerivWithinAt I' I'' g univ (f x) g'
⊢ HasMFDerivWithinAt I I' f s x f'

Tactic:
rw [← hasMFDerivWithinAt_univ] at *

Premises used: hasMFDerivWithinAt_univ