-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (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
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
f : M → 𝕜
hf : MDiffAt[s] f x
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (β := TangentSpace I x)
      (((fderivWithin 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
                ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          ((ContinuousLinearMap.inverse
                  (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
                    fderivWithin 𝕜
                      (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
                      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
                        range (↑𝓘(𝕜, E) : E → E))
                      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
                  else 0) :
                (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
                  TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
              (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) :
            TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :
        𝕜)
      ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
            (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
          ((ContinuousLinearMap.inverse
                (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
                  fderivWithin 𝕜
                    (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
                    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
                      range (↑𝓘(𝕜, E) : E → E))
                    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
                else 0) :
              (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
                TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))) :
        TangentSpace I x) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := TangentSpace 𝓘(𝕜, 𝕜) (f x)) (β := TangentSpace I x)
      (((if True then
                fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, 𝕜) x f)
                  ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
              else 0 :
              ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, 𝕜) (f x))) :
            (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, 𝕜) (f x))
          (V x) :
        TangentSpace 𝓘(𝕜, 𝕜) (f x))
      ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
              (ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x))
              (ContinuousLinearMap.inverse
                (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
                  fderivWithin 𝕜
                    (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
                    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
                      range (↑𝓘(𝕜, E) : E → E))
                    ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
                else 0)) :
            (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) → TangentSpace I x)
          (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) :
        TangentSpace I x)
have e_a : (ContinuousLinearMap.inverse
        (if MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) then
          fderivWithin 𝕜
            (writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M))
            ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)).symm : E → E) ⁻¹' range (↑I : H → E) ∩
              range (↑𝓘(𝕜, E) : E → E))
            ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
        else 0) :
      (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
        TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) =
  V x
Tactic: congr 2