-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_comp_of_left
    {g : M' → M''} {f : M → M'} {V : Π (x : M''), TangentSpace I'' x} {s : Set M} {t : Set M'}
    {x₀ : M} (hf : MDifferentiableWithinAt I I' f s x₀) (h : Set.MapsTo f s t)
    (hu : UniqueMDiffWithinAt I s x₀) (hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible) :
    mpullbackWithin I I'' (g ∘ f) V s x₀ =
      mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDifferentiableWithinAt I I' f s x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible
⊢ mpullbackWithin I I'' (g ∘ f) V s x₀ = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀

Tactic:
simp only [mpullbackWithin, comp_apply]

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDifferentiableWithinAt I I' f s x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible
⊢ (mfderivWithin I I'' (g ∘ f) s x₀).inverse (V ((g ∘ f) x₀)) =
    (mfderivWithin I I' f s x₀).inverse ((mfderivWithin I' I'' g t (f x₀)).inverse (V (g (f x₀))))

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDifferentiableWithinAt I I' f s x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible
⊢ (mfderivWithin I I'' (g ∘ f) s x₀).inverse (V ((g ∘ f) x₀)) =
    (mfderivWithin I I' f s x₀).inverse ((mfderivWithin I' I'' g t (f x₀)).inverse (V (g (f x₀))))

Tactic:
have hg : MDifferentiableWithinAt I' I'' g t (f x₀) :=
  mdifferentiableWithinAt_of_isInvertible_mfderivWithin hg'

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDifferentiableWithinAt I I' f s x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible
hg : MDifferentiableWithinAt I' I'' g t (f x₀)
⊢ (mfderivWithin I I'' (g ∘ f) s x₀).inverse (V ((g ∘ f) x₀)) =
    (mfderivWithin I I' f s x₀).inverse ((mfderivWithin I' I'' g t (f x₀)).inverse (V (g (f x₀))))

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
E' : Type u_6
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDifferentiableWithinAt I I' f s x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible
hg : MDifferentiableWithinAt I' I'' g t (f x₀)
⊢ (mfderivWithin I I'' (g ∘ f) s x₀).inverse (V ((g ∘ f) x₀)) =
    (mfderivWithin I I' f s x₀).inverse ((mfderivWithin I' I'' g t (f x₀)).inverse (V (g (f x₀))))

Tactic:
rw [mfderivWithin_comp _ hg hf h hu, Function.comp_apply,
  IsInvertible.inverse_comp_apply_of_left hg']

Result:
no goals