-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
    mlieBracketWithin I V W s x = 0

Proof state:
𝕜 : 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) x).inverse 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) (↑(extChartAt I x) x) = 0

Tactic:
simp only [mpullbackWithin_apply]

Result:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Tactic:
have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp

Result:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I) (↑(extChartAt I x) x) = 0

Tactic:
simp only [mpullbackWithin_apply]

Result:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Tactic:
have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp

Result:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Proof state:
case 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ mlieBracketWithin I V W s x = 0

Tactic:
simp only [mlieBracketWithin, mpullback_apply, comp_apply]

Result:
𝕜 : 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) x).inverse
      (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)) =
    0