-- 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
inst_7 : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun (x : M) ↦ ⟨x, W x⟩) x
hs : UniqueMDiffWithinAt I s x
set :
  let V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E));
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 V'
        (HSMul.hSMul (β := (x : E) → TangentSpace 𝓘(𝕜, E) x) (f ∘ (↑(extChartAt I x).symm : E → M))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
      x =
    HSMul.hSMul (α := 𝕜)
        ((fromTangentSpace (f x) : (a : 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) +
      HSMul.hSMul (β := TangentSpace I x) (f x)
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
          (lieBracketWithin 𝕜 V' (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
            ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
          x)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
        (HSMul.hSMul (β := (x : E) → TangentSpace 𝓘(𝕜, E) x) (f ∘ (↑(extChartAt I x).symm : E → M))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
      x =
    HSMul.hSMul (α := 𝕜)
        ((fromTangentSpace (f x) : (a : 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) +
      HSMul.hSMul (β := TangentSpace I x) (f x)
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
          (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
            ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
          x)

Tactic:
set V' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I)

Premises used: extChartAt, VectorField.mpullbackWithin, PartialEquiv.symm, ModelWithCorners.toFun', modelWithCornersSelf, Set.range, PartialEquiv.toFun