Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case e_6
𝕜 : 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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)

Tactic:
apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq

Goal state after:
case e_6.hV
𝕜 : 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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁
      (range ↑I) =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)

case hxV
𝕜 : 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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I) (↑(extChartAt I x) x) =
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) (↑(extChartAt I x) x)

case e_6.hW
𝕜 : 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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁
      (range ↑I) =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)

case hxW
𝕜 : 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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I) (↑(extChartAt I x) x) =
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I) (↑(extChartAt I x) x)