-- 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 :
  ∀ᶠ (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)
h :
  ∀ (y : M)
    (hy :
      ∀ᶠ (x_1 : M) in 𝓝[s] y,
        (↑(extChartAt I x) : M → E) x_1 ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)
    (hyU :
      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))
    (hyV :
      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))
    (h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source) (ys : y ∈ s),
    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) 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)

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem, J1U, J1V,
      nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyU hyV h'y ys

Premises used: Iff.mpr, chart_source_mem_nhds, nhdsWithin_le_nhds, self_mem_nhdsWithin, eventually_eventually_nhdsWithin