-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivWithinAt.comp (hg : HasMFDerivWithinAt I' I'' g u (f x) g')
    (hf : HasMFDerivWithinAt I I' f s x f') (hst : s ⊆ f ⁻¹' u) :
    HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f')

Proof state:
𝕜 : 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
s : Set M
g : M' → M''
u : Set M'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g' (↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑(extChartAt I x) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) (↑(extChartAt I x) x)
hst : s ⊆ f ⁻¹' u
this✝¹ :
  ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' (f x)).source) ∈
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
this✝ : writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)
y : E
hy :
  (↑(chartAt H x).symm (↑I.symm y) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm y)) ∈ (chartAt H' (f x)).source) ∧ y ∈ range ↑I
this : f (↑(chartAt H x).symm (↑I.symm y)) ∈ u
⊢ writtenInExtChartAt I I' x f y ∈ ↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I'

Tactic:
simp only [hy, this, mfld_simps]

Result:
no goals

Proof state:
𝕜 : 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
s : Set M
g : M' → M''
u : Set M'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g' (↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑(extChartAt I x) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) (↑(extChartAt I x) x)
hst : s ⊆ f ⁻¹' u
this✝ :
  ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' (f x)).source) ∈
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
this : writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I
⊢ writtenInExtChartAt I I' x f y ∈ ↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I'

Tactic:
simp only [mfld_simps] at hy

Result:
𝕜 : 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
s : Set M
g : M' → M''
u : Set M'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g' (↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑(extChartAt I x) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) (↑(extChartAt I x) x)
hst : s ⊆ f ⁻¹' u
this✝ :
  ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' (f x)).source) ∈
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
this : writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)
y : E
hy :
  (↑(chartAt H x).symm (↑I.symm y) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm y)) ∈ (chartAt H' (f x)).source) ∧ y ∈ range ↑I
⊢ writtenInExtChartAt I I' x f y ∈ ↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I'