-- 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
⊢ let V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E));
  let W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E));
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (fun (x₀ : E) ↦
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
          (((fderivWithin 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
                    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) x₀ :
                  E →L[𝕜] 𝕜) :
                (a : E) → 𝕜)
              (V' x₀) :
            𝕜)
          (W' x₀))
      x =
    HSMul.hSMul.{u_1, u_3, u_3} (α := TangentSpace 𝓘(𝕜, 𝕜) (f x))
      (((mfderivWithin I 𝓘(𝕜, 𝕜) f s x :
              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))
      (W x)
have simp : 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)
Tactic: simp only [mpullback, mfderivWithin, hf, map_smul, ← mfderiv_extChart_inverse_comp_aux x W,
    mpullbackWithin]