awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun (g : G) ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun (x : G) ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun (g : G) ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) :=
  (⇑(Equiv.symm (equivTangentBundleProd I G I G)) :
    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) → TangentBundle I G :=
  tangentMap (I.prod I) I fun (p : G × G) ↦ p.1 * p.2
⊢ ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (g : G) ↦ ⟨g, mulInvariantVectorField v g⟩
have S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
Tactic: have S₃ : CMDiff (minSmoothness 𝕜 2) F₃ := by
    apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl
    rw [A]
    exact contMDiff_mul I (minSmoothness 𝕜 3)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun (g : G) ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun (x : G) ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun (g : G) ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) :=
  (⇑(Equiv.symm (equivTangentBundleProd I G I G)) :
    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) → TangentBundle I G :=
  tangentMap (I.prod I) I fun (p : G × G) ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
⊢ ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (g : G) ↦ ⟨g, mulInvariantVectorField v g⟩
have h : ∀ (g : G), g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I)
Tactic: convert! S with g
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun (g : G) ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun (x : G) ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun (g : G) ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) :=
  (⇑(Equiv.symm (equivTangentBundleProd I G I G)) :
    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) → TangentBundle I G :=
  tangentMap (I.prod I) I fun (p : G × G) ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
h : ∀ (g : G), g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I)
⊢ ContMDiff I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    fun (g : G) ↦ ⟨g, mulInvariantVectorField v g⟩
have h₁ : ∀ (g : G),
  g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I) →
    mulInvariantVectorField v g = (((F₃ ∘ F₂) ∘ F₁) g).snd (E := TangentSpace I)
Tactic: convert! S with g
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)
have h : ∀ (g : G),
  mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
have h : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)
Tactic: rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
    mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
h : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
have h₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)
Tactic: rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
    mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
h : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)
h₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
have h₂ : ContMDiffAt I I (M' := G) (minSmoothness 𝕜 3) (fun (x : G) ↦ g⁻¹ * x) g
Tactic: rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
    mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
h : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)
h₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)
h₂ : ContMDiffAt I I (M' := G) (minSmoothness 𝕜 3) (fun (x : G) ↦ g⁻¹ * x) g
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
have h₃ : minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3
Tactic: rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
    mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ LE.le (α := WithTop ℕ∞) 2 3
have norm_cast : LE.le (α := ℕ) 2 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ⁅u + v, w⁆ = ⁅u, w⁆ + ⁅v, w⁆
have simp : mlieBracket I (mulInvariantVectorField u + mulInvariantVectorField v) (mulInvariantVectorField w) 1 =
  HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
    (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
Tactic: simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u + mulInvariantVectorField v) (mulInvariantVectorField w) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
      (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
have hV : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
Tactic: rw [mlieBracket_add_left]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hV : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField u + mulInvariantVectorField v) (mulInvariantVectorField w) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
      (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
have hV₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
Tactic: rw [mlieBracket_add_left]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ⁅u, v + w⁆ = ⁅u, v⁆ + ⁅u, w⁆
have simp : mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v + mulInvariantVectorField w) 1 =
  HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1)
    (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
Tactic: simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v + mulInvariantVectorField w) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1)
      (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
have hW : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
Tactic: rw [mlieBracket_add_right]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hW : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v + mulInvariantVectorField w) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1)
      (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1)
have hW₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Tactic: rw [mlieBracket_add_right]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ⁅u, ⁅v, w⁆⁆ = ⁅⁅u, v⁆, w⁆ + ⁅v, ⁅u, w⁆⁆
have simp : mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
  HAdd.hAdd (α := GroupLieAlgebra I G)
    (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
      1)
    (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
      1)
Tactic: simp only [GroupLieAlgebra.bracket_def, mulInvariantVector_mlieBracket]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G)
      (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1)
      (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1)
have hU : ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
  (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
Tactic: apply leibniz_identity_mlieBracket_apply
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hU :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G)
      (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1)
      (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1)
have hV : ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
  (fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
Tactic: apply leibniz_identity_mlieBracket_apply
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hU :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
hV :
  ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
    (fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
⊢ mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    HAdd.hAdd (α := GroupLieAlgebra I G)
      (mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1)
      (mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1)
have hW : ContMDiffAt I (I.prod 𝓘(𝕜, E)) (M' := TotalSpace.{u_4, u_3, u_3} (B := G) E (TangentSpace I)) (minSmoothness 𝕜 2)
  (fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Tactic: apply leibniz_identity_mlieBracket_apply
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆
have simp : mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
  HSMul.hSMul (β := AddGroupLieAlgebra I G) c (mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0)
Tactic: simp only [AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G_1 : Type u_4
inst_4 : TopologicalSpace G_1
inst_5 : ChartedSpace H G_1
inst_6 : Group G_1
inst_7 : LieGroup I (minSmoothness 𝕜 3) G_1
inst_8 : CompleteSpace E
G : Type u_5
inst_9 : TopologicalSpace G
inst_10 : ChartedSpace H G
inst_11 : AddGroup G
inst_12 : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
    HSMul.hSMul (β := AddGroupLieAlgebra I G) c
      (mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0)
have rw : (MDiffAt fun (x : G) ↦ ⟨x, addInvariantVectorField w x⟩) 0
Tactic: rw [mlieBracket_const_smul_right]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆
have simp : mlieBracket I (mulInvariantVectorField v) (c • mulInvariantVectorField w) 1 =
  HSMul.hSMul (β := GroupLieAlgebra I G) c (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
Tactic: simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
inst_8 : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField v) (c • mulInvariantVectorField w) 1 =
    HSMul.hSMul (β := GroupLieAlgebra I G) c (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)
have rw : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Tactic: rw [mlieBracket_const_smul_right]