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 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[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) ⁻¹' ((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)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x

Tactic:
have C : CMDiffAt[s] m' (T% ((mpullback I 𝓘(𝕜, E) (extChartAt I x)
      ((mlieBracketWithin 𝓘(𝕜, E) U' V'
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)))))) x :=
    ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq B (n := m' + 1)
      contMDiffAt_extChartAt
      (isInvertible_mfderiv_extChartAt (mem_extChartAt_source x)) le_rfl pre_mem 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 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[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) ⁻¹' ((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)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x