[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
X Y : LeftInvariantDerivation I G
h : ↑X = ↑Y
⊢ X = Y
[PROOFSTEP]
cases X
[GOAL]
case mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
Y : LeftInvariantDerivation I G
toDerivation✝ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝) = ↑(Derivation.evalAt g) toDerivation✝
h : ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = ↑Y
⊢ { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = Y
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : SmoothMul I G
g h✝ : G
toDerivation✝¹ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝¹ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝¹) = ↑(Derivation.evalAt g) toDerivation✝¹
toDerivation✝ : Derivation 𝕜 C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ :
  ∀ (g : G), ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) toDerivation✝) = ↑(Derivation.evalAt g) toDerivation✝
h :
  ↑{ toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
⊢ { toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) 0) = ↑(Derivation.evalAt g) 0
[PROOFSTEP]
simp only [_root_.map_zero]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (↑X + ↑Y)) = ↑(Derivation.evalAt g) (↑X + ↑Y)
[PROOFSTEP]
simp only [map_add, Derivation.coe_add, left_invariant', Pi.add_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (-↑X)) = ↑(Derivation.evalAt g) (-↑X)
[PROOFSTEP]
rw [map_neg (Derivation.evalAt (𝕜 := 𝕜) (1 : G)), map_neg (𝒅ₕ (smoothLeftMul_one I g)), left_invariant',
  map_neg (Derivation.evalAt (𝕜 := 𝕜) g)]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (↑X - ↑Y)) = ↑(Derivation.evalAt g) (↑X - ↑Y)
[PROOFSTEP]
rw [map_sub (Derivation.evalAt (𝕜 := 𝕜) (1 : G)), map_sub (𝒅ₕ (smoothLeftMul_one I g)),
  map_sub (Derivation.evalAt (𝕜 := 𝕜) g), left_invariant', left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℕ
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : ℤ
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul_of_tower _ r, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
X : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) (r • ↑X)) = ↑(Derivation.evalAt g) (r • ↑X)
[PROOFSTEP]
simp_rw [LinearMap.map_smul, left_invariant']
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑(evalAt (g * h)) X = ↑(𝒅ₕ (_ : ↑(𝑳 I g) h = g * h)) (↑(evalAt h) X)
[PROOFSTEP]
ext f
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(evalAt (g * h)) X) f = ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) h = g * h)) (↑(evalAt h) X)) f
[PROOFSTEP]
rw [← left_invariant, apply_hfdifferential, apply_hfdifferential, L_mul, fdifferential_comp, apply_fdifferential]
  -- Porting note: more agressive here
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(LinearMap.comp (𝒅 (𝑳 I g) (↑(𝑳 I h) 1)) (𝒅 (𝑳 I h) 1)) (↑(evalAt 1) X)) f =
    ↑(↑(evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
erw [LinearMap.comp_apply]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ↑(↑(𝒅 (𝑳 I g) (↑(𝑳 I h) 1)) (↑(𝒅 (𝑳 I h) 1) (↑(evalAt 1) X))) f = ↑(↑(evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
rw [apply_fdifferential, ← apply_hfdifferential, left_invariant]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ContMDiffMap.comp (↑X f) (𝑳 I g) = ↑X (ContMDiffMap.comp f (𝑳 I g))
[PROOFSTEP]
ext h
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h✝ : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ↑(ContMDiffMap.comp (↑X f) (𝑳 I g)) h = ↑(↑X (ContMDiffMap.comp f (𝑳 I g))) h
[PROOFSTEP]
rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, apply_hfdifferential, apply_fdifferential,
  evalAt_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ ↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆) = ↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆
[PROOFSTEP]
ext f
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
have hX := Derivation.congr_fun (left_invariant' g X) (Y f)
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑X)) (↑Y f) = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
have hY := Derivation.congr_fun (left_invariant' g Y) (X f)
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑X)) (↑Y f) = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ↑Y)) (↑X f) = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑(𝒅ₕ (_ : ↑(𝑳 I g) 1 = g)) (↑(Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [apply_hfdifferential, apply_fdifferential, Derivation.evalAt_apply] at hX hY ⊢
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (ContMDiffMap.comp (↑Y f) (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (ContMDiffMap.comp (↑X f) (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [comp_L] at hX hY 
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [Derivation.commutator_apply, SmoothMap.coe_sub, Pi.sub_apply, coe_derivation]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑X (↑↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - ↑(↑↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [coe_derivation] at hX hY ⊢
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 - ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 =
    ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rw [hX, hY]
[GOAL]
case H
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g✝ h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^⊤⟮I, G; 𝕜⟯⟨g⟩
hX : ↑(↑X (↑Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑X) (↑Y f)
hY : ↑(↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ↑(↑(Derivation.evalAt g) ↑Y) (↑X f)
⊢ ↑(↑(Derivation.evalAt g) ↑X) (↑Y f) - ↑(↑(Derivation.evalAt g) ↑Y) (↑X f) = ↑(↑(Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X + Y, Z⁆ = ⁅X, Z⁆ + ⁅Y, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X + Y, Z⁆ f✝ = ↑(⁅X, Z⁆ + ⁅Y, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Z f✝) + ↑Y (↑Z f✝) - (↑Z (↑X f✝) + ↑Z (↑Y f✝)) = ↑X (↑Z f✝) - ↑Z (↑X f✝) + (↑Y (↑Z f✝) - ↑Z (↑Y f✝))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, Y + Z⁆ = ⁅X, Y⁆ + ⁅X, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, Y + Z⁆ f✝ = ↑(⁅X, Y⁆ + ⁅X, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Y f✝) + ↑X (↑Z f✝) - (↑Y (↑X f✝) + ↑Z (↑X f✝)) = ↑X (↑Y f✝) - ↑Y (↑X f✝) + (↑X (↑Z f✝) - ↑Z (↑X f✝))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
⊢ ⁅X, X⁆ = 0
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, X⁆ f✝ = ↑0 f✝
[PROOFSTEP]
simp only [commutator_apply, sub_self]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ 0 = ↑0 f✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, ⁅Y, Z⁆⁆ = ⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅X, ⁅Y, Z⁆⁆ f✝ = ↑(⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, coe_add, coe_sub, map_sub, Pi.add_apply]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑X (↑Y (↑Z f✝)) - ↑X (↑Z (↑Y f✝)) - (↑Y (↑Z (↑X f✝)) - ↑Z (↑Y (↑X f✝))) =
    ↑X (↑Y (↑Z f✝)) - ↑Y (↑X (↑Z f✝)) - (↑Z (↑X (↑Y f✝)) - ↑Z (↑Y (↑X f✝))) +
      (↑Y (↑X (↑Z f✝)) - ↑Y (↑Z (↑X f✝)) - (↑X (↑Z (↑Y f✝)) - ↑Z (↑X (↑Y f✝))))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
⊢ ⁅Y, r • Z⁆ = r • ⁅Y, Z⁆
[PROOFSTEP]
ext1
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
inst✝³ : Monoid G
inst✝² : SmoothMul I G
g h : G
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
r✝ : 𝕜
X Y✝ : LeftInvariantDerivation I G
f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
f✝ : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ↑⁅Y, r • Z⁆ f✝ = ↑(r • ⁅Y, Z⁆) f✝
[PROOFSTEP]
simp only [commutator_apply, map_smul, smul_sub, coe_smul, Pi.smul_apply]
