-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (hypothesis)
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'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
A' : x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)
h'f : MDiffAt[s] f x₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
    (ContinuousLinearMap.inverse
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E))
        ((↑(extChartAt I x₀) : M → E) x₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
⊢ lieBracketWithin 𝕜
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f V s) (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f W s) (range (↑I : H → E)))
      ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀) =
    ((ContinuousLinearMap.inverse
            (ContinuousLinearMap.comp (M₂ := TangentSpace I x₀)
              (mfderivWithin I 𝓘(𝕜, E') ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) s x₀)
              (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E))
                ((↑(extChartAt I x₀) : M → E) x₀))) :
          ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜)
            (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (f x₀)) : M' → E') (f x₀)))
            (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))) :
        (a : TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (f x₀)) : M' → E') (f x₀))) →
          TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀))
      (lieBracketWithin 𝕜
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E')))
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E')))
        ((↑(extChartAt I' (f x₀)).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))
        ((↑(extChartAt I' (f x₀)) : M' → E') (f x₀)))
have this₁ : Eq (α :=
  TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x₀) : M → E) x₀) →L[𝕜]
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)))
  (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀))
  (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M)
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀))
Tactic: have : mfderiv[range I] (extChartAt I x₀).symm (extChartAt I x₀ x₀) =
      mfderiv[(extChartAt I x₀).symm ⁻¹' s ∩ range I] (extChartAt I x₀).symm (extChartAt I x₀ x₀) :=
    (MDifferentiableWithinAt.mfderivWithin_mono
      (mdifferentiableWithinAt_extChartAt_symm (mem_extChartAt_target x₀))
      (UniqueDiffWithinAt.uniqueMDiffWithinAt (hu x₀ hx₀)) inter_subset_right).symm