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
g : G
v : GroupLieAlgebra I G
⊢ mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) = mulInvariantVectorField v
have M : minSmoothness 𝕜 3 ≠ 0
Tactic: have M : minSmoothness 𝕜 3 ≠ 0 := lt_of_lt_of_le (by simp) le_minSmoothness |>.ne'
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
⊢ mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) = mulInvariantVectorField v
have h : ∀ (h : G), mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) h = mulInvariantVectorField v h
Tactic: ext h
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
⊢ mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) h = mulInvariantVectorField v h
have h₁ : Eq (α := TangentSpace I h)
  ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
        (a : TangentSpace I (g * h)) → TangentSpace I h)
      (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
        TangentSpace I (g * h * 1)) :
    TangentSpace I h)
  (((mfderiv% fun (x : G) ↦ h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (h * 1)) v : TangentSpace I (h * 1))
Tactic: simp only [mpullback, inverse_mfderiv_mul_left, 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
⊢ Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
have h₁ : ∀ (x : G), h * x = ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x) x
Tactic: ext x
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h x : G
⊢ h * x = ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x) x
have h₁ : h * x = g⁻¹ * (g * h * x)
Tactic: simp only [comp_apply]
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
⊢ Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((mfderiv% fun (x : G) ↦ h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (h * 1)) v : TangentSpace I (h * 1))
have D : Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
Tactic: have D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ (fun x ↦ g * h * x) := by
    ext x; simp only [comp_apply]; group
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
⊢ Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((mfderiv% fun (x : G) ↦ h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (h * 1)) v : TangentSpace I (h * 1))
have h₁ : Eq (α := TangentSpace I h)
  ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
        (a : TangentSpace I (g * h)) → TangentSpace I h)
      (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
        TangentSpace I (g * h * 1)) :
    TangentSpace I h)
  (((ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h * 1)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h * 1))
            ((mfderiv% fun (x : G) ↦ g * h * x) 1) :
          TangentSpace.{u_3, u_1, u_2, u_4} I (M := G) 1 →L[𝕜] TangentSpace I (g⁻¹ * (g * h * 1))) :
        (a : TangentSpace I 1) → TangentSpace I (h * 1))
      v :
    TangentSpace I (h * 1))
Tactic: rw [D, mfderiv_comp (I' := I)]
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
h₁ :
  Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h * 1)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h * 1))
              ((mfderiv% fun (x : G) ↦ g * h * x) 1) :
            TangentSpace.{u_3, u_1, u_2, u_4} I (M := G) 1 →L[𝕜] TangentSpace I (g⁻¹ * (g * h * 1))) :
          (a : TangentSpace I 1) → TangentSpace I (h * 1))
        v :
      TangentSpace I (h * 1))
⊢ Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((mfderiv% fun (x : G) ↦ h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (h * 1)) v : TangentSpace I (h * 1))
have h₂ : (MDiffAt fun (b : G) ↦ g⁻¹ * b) (g * h * 1)
Tactic: rw [D, mfderiv_comp (I' := I)]
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
h₁ :
  Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h * 1)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h * 1))
              ((mfderiv% fun (x : G) ↦ g * h * x) 1) :
            TangentSpace.{u_3, u_1, u_2, u_4} I (M := G) 1 →L[𝕜] TangentSpace I (g⁻¹ * (g * h * 1))) :
          (a : TangentSpace I 1) → TangentSpace I (h * 1))
        v :
      TangentSpace I (h * 1))
h₂ : (MDiffAt fun (b : G) ↦ g⁻¹ * b) (g * h * 1)
⊢ Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((mfderiv% fun (x : G) ↦ h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (h * 1)) v : TangentSpace I (h * 1))
have h₃ : (MDiffAt fun (x : G) ↦ g * h * x) 1
Tactic: rw [D, mfderiv_comp (I' := I)]
-- 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)
⊢ Eq (α := TangentSpace I h)
    ((((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (g⁻¹ * (g * h))) :
          (a : TangentSpace I (g * h)) → TangentSpace I h)
        (((mfderiv% fun (x : G) ↦ g * h * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * h * 1)) v :
          TangentSpace I (g * h * 1)) :
      TangentSpace I h)
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h * 1)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h * 1))
              ((mfderiv% fun (x : G) ↦ g * h * x) 1) :
            TangentSpace.{u_3, u_1, u_2, u_4} I (M := G) 1 →L[𝕜] TangentSpace I (g⁻¹ * (g * h * 1))) :
          (a : TangentSpace I 1) → TangentSpace I (h * 1))
        v :
      TangentSpace I (h * 1))
have h₁ : g * h = g * h * 1
Tactic: congr 2
-- 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
g : G
V : (g : G) → TangentSpace I g
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun (x : G) ↦ g⁻¹ * x) V g
have A : 1 = g⁻¹ * g
Tactic: have A : 1 = g⁻¹ * g := by simp
-- 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
g : G
V : (g : G) → TangentSpace I g
A : 1 = g⁻¹ * g
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun (x : G) ↦ g⁻¹ * x) V g
have simp : Eq (α := TangentSpace I g)
  (((mfderiv% fun (x : G) ↦ g * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * 1)) (V 1) : TangentSpace I (g * 1))
  ((((mfderiv% fun (b : G) ↦ g⁻¹⁻¹ * b) (g⁻¹ * g) : TangentSpace I (g⁻¹ * g) →L[𝕜] TangentSpace I (g⁻¹⁻¹ * (g⁻¹ * g))) :
        (a : TangentSpace I (g⁻¹ * g)) → TangentSpace I g)
      (V (g⁻¹ * g)) :
    TangentSpace I g)
Tactic: simp only [mulInvariantVectorField, mpullback, inverse_mfderiv_mul_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
g : G
V : (g : G) → TangentSpace I g
A : 1 = g⁻¹ * g
⊢ Eq (α := TangentSpace I g)
    (((mfderiv% fun (x : G) ↦ g * x) 1 : (a : TangentSpace I 1) → TangentSpace I (g * 1)) (V 1) :
      TangentSpace I (g * 1))
    ((((mfderiv% fun (b : G) ↦ g⁻¹⁻¹ * b) (g⁻¹ * g) :
            TangentSpace I (g⁻¹ * g) →L[𝕜] TangentSpace I (g⁻¹⁻¹ * (g⁻¹ * g))) :
          (a : TangentSpace I (g⁻¹ * g)) → TangentSpace I g)
        (V (g⁻¹ * g)) :
      TangentSpace I g)
have h : Eq.{u_4 + 1} (α := G → G) (fun (x : G) ↦ g * x) fun (b : G) ↦ g⁻¹⁻¹ * b
Tactic: congr
-- 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
⊢ 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 M : minSmoothness 𝕜 3 ≠ 0
Tactic: have M : minSmoothness 𝕜 3 ≠ 0 := lt_of_lt_of_le (by simp) le_minSmoothness |>.ne'
-- 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
⊢ minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
have rw : minSmoothness 𝕜 (HAdd.hAdd (α := WithTop ℕ∞) 2 1) = minSmoothness 𝕜 3
Tactic: rw [← minSmoothness_add]
-- 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
⊢ 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 A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
Tactic: have A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3 := by
    rw [← minSmoothness_add]
    norm_num
-- 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⟩
⊢ 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 sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
Tactic: have sfg : CMDiff (minSmoothness 𝕜 2) fg := contMDiff_zeroSection _ _
-- 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⟩
⊢ 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 sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
Tactic: have sfv : CMDiff (minSmoothness 𝕜 2) fv := contMDiff_const
-- 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)
⊢ 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 (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
Tactic: have S₁ : CMDiff (minSmoothness 𝕜 2) F₁ := sfg.prodMk sfv
-- 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))
⊢ 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.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
Tactic: have S₂ : CMDiff (minSmoothness 𝕜 2) F₂ := contMDiff_equivTangentBundleProd_symm
-- 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
⊢ ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
have apply : ContMDiff (I.prod I) I (M' := G) (minSmoothness 𝕜 2 + 1) fun (p : G × G) ↦ p.1 * p.2
Tactic: apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl
-- 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
⊢ ContMDiff (I.prod I) I (M' := G) (minSmoothness 𝕜 2 + 1) fun (p : G × G) ↦ p.1 * p.2
have rw : ContMDiff (I.prod I) I (M' := G) (minSmoothness 𝕜 3) fun (p : G × G) ↦ p.1 * p.2
Tactic: rw [A]