-- 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 :
  ∀ᶠ (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)
⊢ ∀ᶠ (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)

Tactic:
have : ∀ᶠ y in 𝓝[s] x, mlieBracketWithin I
        (mpullback I 𝓘(𝕜, E) (extChartAt I x) U') (mpullback I 𝓘(𝕜, E) (extChartAt I x) W') s y
      = mpullback I 𝓘(𝕜, E) (extChartAt I x) (mlieBracketWithin 𝓘(𝕜, E) U' W'
        ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)) y := by
    filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem, J1U, J1W,
      nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyU hyW h'y ys
    symm
    exact mpullback_mlieBracketWithin (n := minSmoothness 𝕜 2)
      (hyU.mdifferentiableWithinAt (two_pos.trans_le le_minSmoothness).ne')
      (hyW.mdifferentiableWithinAt (two_pos.trans_le le_minSmoothness).ne') hs
      (contMDiffAt_extChartAt' h'y) ys le_rfl hy