-- 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
inst_6 : IsManifold I (minSmoothness 𝕜 3) M
inst_7 : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiffOn I s
h's : x ∈ closure[inst_4] (interior s)
hx : x ∈ s
hU :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (minSmoothness 𝕜 2) (fun (x : M) ↦ ⟨x, U x⟩) s x
hV :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (minSmoothness 𝕜 2) (fun (x : M) ↦ ⟨x, V x⟩) s x
hW :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (minSmoothness 𝕜 2) (fun (x : M) ↦ ⟨x, W x⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
pre_mem : (↑(extChartAt I x) : M → E) ⁻¹' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) U (range (↑I : H → E))
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x :=
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
J0V :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, V' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
J0W :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, W' x⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
J1U :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, U' x⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
J1V :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, V' x⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
J1W :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (minSmoothness 𝕜 2) (fun (x : E) ↦ ⟨x, W' x⟩)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y)
JU : U =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) U'
JV : V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) V'
JW : W =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) W'
this_1 :
  ∀ᶠ (y : M) in 𝓝[s] x,
    Eq (α := TangentSpace I y)
      (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) V')
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) W') s y)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) y)
this_2 :
  ∀ᶠ (y : M) in 𝓝[s] x,
    Eq (α := TangentSpace I y)
      (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) U')
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) V') s y)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) y)
this :
  ∀ᶠ (y : M) in 𝓝[s] x,
    Eq (α := TangentSpace I y)
      (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) U')
        (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) W') s y)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E) U' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) y)
rw :
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mlieBracketWithin 𝓘(𝕜, E) U'
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
      x =
    HAdd.hAdd (α := TangentSpace I x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E)
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) W'
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
        x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E) V'
          (mlieBracketWithin 𝓘(𝕜, E) U' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
        x)
rw₁ :
  (MDiffAt[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s] fun (x_1 : E) ↦
      ⟨x_1, mlieBracketWithin 𝓘(𝕜, E) U' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x_1⟩)
    ((↑(extChartAt I x) : M → E) x)
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
      (mlieBracketWithin 𝓘(𝕜, E) U'
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
      x =
    HAdd.hAdd (α := TangentSpace I x)
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E)
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) W'
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
        x)
      (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) V')
        (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) U')
          (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) W') s)
        s x)

Tactic:
rw [Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem EventuallyEq.rfl this hx,
    ← mpullback_mlieBracketWithin (J0V.mdifferentiableWithinAt
      (two_pos.trans_le le_minSmoothness).ne') _ hs contMDiffAt_extChartAt hx le_rfl pre_mem]

Premises used: le_rfl, VectorField.mpullback_mlieBracketWithin, le_minSmoothness, two_pos, LT.lt.ne', LT.lt.trans_le, contMDiffAt_extChartAt, ContMDiffWithinAt.mdifferentiableWithinAt, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem, Filter.EventuallyEq.rfl