-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.Pullback (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
H'' : Type u_8
inst_11 : TopologicalSpace H''
E'' : Type u_9
inst_12 : NormedAddCommGroup E''
inst_13 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hf : MDiffAt[s] f x₀
h : MapsTo f s t
hu : UniqueMDiffWithinAt I s x₀
hg' : IsInvertible (M := TangentSpace I' (f x₀)) (M₂ := TangentSpace I'' (g (f x₀))) (mfderivWithin I' I'' g t (f x₀))
hg : MDiffAt[t] g (f x₀)
rw :
  Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse
              (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I' I'' g t (f x₀))
                (mfderivWithin I I' f s x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
rw₁ :
  Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse
              (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I' I'' g t (f x₀))
                (mfderivWithin I I' f s x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀))) (TangentSpace I x₀)) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I x₀)
        (V (g (f x₀))) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
⊢ Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((inverse (mfderivWithin I I'' (g ∘ f) s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_3} (RingHom.id 𝕜) (TangentSpace I'' ((g ∘ f) x₀))
              (TangentSpace I x₀)) :
          (a : TangentSpace I'' ((g ∘ f) x₀)) → TangentSpace I x₀)
        (V ((g ∘ f) x₀)) :
      TangentSpace I x₀)
    (((inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        (((inverse (mfderivWithin I' I'' g t (f x₀)) :
              ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
                (TangentSpace I' (f x₀))) :
            (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
          (V (g (f x₀)))) :
      TangentSpace I x₀)
have rw₂ : Eq.{u_3 + 1} (α := TangentSpace I x₀)
  (((inverse (mfderivWithin I I' f s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
      (((inverse (mfderivWithin I' I'' g t (f x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
              (TangentSpace I' (f x₀))) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
        (V (g (f x₀)))) :
    TangentSpace I x₀)
  (((inverse (mfderivWithin I I' f s x₀) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
        (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
      (((inverse (mfderivWithin I' I'' g t (f x₀)) :
            ContinuousLinearMap.{u_1, u_1, u_9, u_6} (RingHom.id 𝕜) (TangentSpace I'' (g (f x₀)))
              (TangentSpace I' (f x₀))) :
          (a : TangentSpace I'' (g (f x₀))) → TangentSpace I' (f x₀))
        (V (g (f x₀)))) :
    TangentSpace I x₀)
Tactic: rw [mfderivWithin_comp _ hg hf h hu, Function.comp_apply,
    IsInvertible.inverse_comp_apply_of_left hg']