Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiff[s]
h's : x ∈ closure[inst✝³] (interior s)
hx : x ∈ s
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) s x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨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) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0V :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0W :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J1U :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1V :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1W :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
JU : U =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U'
JV : V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V'
JW : W =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W'
this✝ :
  ∀ᶠ (y : M) in 𝓝[s] x,
    mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W') s y =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) y
this :
  ∀ᶠ (y : M) in 𝓝[s] x,
    mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V') s y =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) y
⊢ ∀ᶠ (y : M) 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

Tactic:
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

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiff[s]
h's : x ∈ closure[inst✝³] (interior s)
hx : x ∈ s
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) s x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨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) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0V :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0W :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J1U :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1V :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1W :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
JU : U =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U'
JV : V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V'
JW : W =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W'
this✝ :
  ∀ᶠ (y : M) in 𝓝[s] x,
    mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W') s y =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) y
this :
  ∀ᶠ (y : M) in 𝓝[s] x,
    mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V') s y =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) y
y : M
hy : ∀ᶠ (x_1 : M) in 𝓝[s] y, ↑(extChartAt I x) x_1 ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
hyU :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
hyW :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
h'y : y ∈ (chartAt H x).source
ys : y ∈ s
⊢ 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