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
⊢ (MDiffAt[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] fun x_1 ↦
      ⟨x_1, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x_1⟩)
    (↑(extChartAt I x) x)

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
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
      (mlieBracketWithin 𝓘(𝕜, E) U'
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
      x =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E)
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) W'
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
        x +
      mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V')
        (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W')
          s)
        s x

Tactic:
· apply ContMDiffWithinAt.mdifferentiableWithinAt _ one_ne_zero
    apply J0U.mlieBracketWithin_vectorField J0V (m := 1)
    · exact hs.uniqueMDiffOn_target_inter x
    · exact ⟨mem_extChartAt_target x, by simp [hx]⟩
    · exact le_rfl

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
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
      (mlieBracketWithin 𝓘(𝕜, E) U'
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
      x =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E)
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) W'
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
        x +
      mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V')
        (mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W')
          s)
        s x