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
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f V s) (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f W s) (range ↑I))
      (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀) =
    (mfderiv[s] (↑(extChartAt I' (f x₀)) ∘ f) x₀ ∘SL
          mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I'))
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I'))
        (↑(extChartAt I' (f x₀)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x₀)) (f x₀)))

Tactic:
have : mfderiv[range I] (extChartAt I x₀).symm (extChartAt I x₀ x₀) =
      mfderiv[(extChartAt I x₀).symm ⁻¹' s ∩ range I] (extChartAt I x₀).symm (extChartAt I x₀ x₀) :=
    (MDifferentiableWithinAt.mfderivWithin_mono
      (mdifferentiableWithinAt_extChartAt_symm (mem_extChartAt_target x₀))
      (UniqueDiffWithinAt.uniqueMDiffWithinAt (hu x₀ hx₀)) inter_subset_right).symm

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
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this✝ : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
this :
  mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) =
    mfderiv[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f V s) (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f W s) (range ↑I))
      (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀) =
    (mfderiv[s] (↑(extChartAt I' (f x₀)) ∘ f) x₀ ∘SL
          mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I'))
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I'))
        (↑(extChartAt I' (f x₀)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x₀)) (f x₀)))