-- 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 𝕜 2) M
inst_7 : CompleteSpace E
n : ℕ∞ω
inst_8 : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) n
    (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)) n
    (fun (x : M) ↦ ⟨x, V x⟩) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
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))
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
    Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) m'
    (fun (x₀ : E) ↦
      ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) x)
C :
  ContMDiffWithinAt I (I.prod 𝓘(𝕜, E)) (M' := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I)) m'
    (fun (x_1 : M) ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) x_1⟩)
    s x
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 :
      ∀ᶠ (x_1 : M) in 𝓝[s] y,
        U x_1 =
          mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) U (range (↑I : H → E))) x_1)
    (hyV :
      ∀ᶠ (x_1 : M) in 𝓝[s] y,
        V x_1 =
          mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))) x_1)
    (h'yU :
      ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
        Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (m' + 1)
        (fun (x_1 : E) ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) U (range (↑I : H → E)) x_1⟩)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y))
    (h'yV :
      ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
        Bundle.TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) (m' + 1)
        (fun (x_1 : E) ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_1⟩)
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) ((↑(extChartAt I x) : M → E) y))
    (hy_chart : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source) (hys : y ∈ s),
    ⟨y, mlieBracketWithin I U V s y⟩ =
      ⟨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⟩
⊢ (𝓝[s] x).EventuallyEq (β := Bundle.TotalSpace.{u_4, u_3, u_3} (B := M) E (TangentSpace I))
    (fun (x₀ : M) ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) fun (x_1 : M) ↦
    ⟨x_1,
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)) x_1⟩

Tactic:
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem,
    eventually_eventually_nhdsWithin.2 (eventuallyEq_mpullback_mpullbackWithin_extChartAt U),
    eventually_eventually_nhdsWithin.2 (eventuallyEq_mpullback_mpullbackWithin_extChartAt V),
    eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm (hU.of_le hm'n) hs hx
      (by gcongr) (by simp [h'm']),
    eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm (hV.of_le hm'n) hs hx
      (by gcongr) (by simp [h'm']),
    nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin]
    with y hy hyU hyV h'yU h'yV hy_chart hys

Premises used: Iff.mpr, chart_source_mem_nhds, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, nhdsWithin_le_nhds, self_mem_nhdsWithin, ContMDiffWithinAt.of_le, eventually_eventually_nhdsWithin, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm