-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
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)
⊢ 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)

Tactic:
simp only [mpullback, mfderivWithin, hf, map_smul, ← mfderiv_extChart_inverse_comp_aux x W,
    mpullbackWithin]

Premises used: VectorField.mpullbackWithin, mfderivWithin, VectorField.mpullback, _private.0.VectorField.mfderiv_extChart_inverse_comp_aux, map_smul