awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
h₁ : ∀ (x : G), h * x = ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x) x
⊢ Eq.{u_4 + 1} (α := (x : G) → G) (fun (x : G) ↦ h * x) ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x)

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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₁ : h * x = g⁻¹ * (g * h * x)
⊢ h * x = ((fun (b : G) ↦ g⁻¹ * b) ∘ fun (x : G) ↦ g * h * x) x

Tactic:
simp only [comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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 = g⁻¹ * (g * h * x)

Tactic:
group
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)

Tactic:
have D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ (fun x ↦ g * h * x) := by
    ext x; simp only [comp_apply]; group
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
h₃ : (MDiffAt fun (x : G) ↦ g * h * x) 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))

Tactic:
rw [D, mfderiv_comp (I' := I)]

Premises used: mfderiv_comp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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₁ : g * h = 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)
    (((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:
congr 2
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
⊢ g * h = g * h * 1

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
⊢ (MDiffAt fun (b : G) ↦ g⁻¹ * b) (g * h * 1)

Tactic:
contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

Premises used: ContMDiffAt.mdifferentiableAt, contMDiff_mul_left, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
⊢ (MDiffAt fun (b : G) ↦ g⁻¹ * b) (g * h * 1)

Tactic:
exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

Premises used: ContMDiffAt.mdifferentiableAt, contMDiff_mul_left, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
⊢ (MDiffAt fun (x : G) ↦ g * h * x) 1

Tactic:
contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

Premises used: ContMDiffAt.mdifferentiableAt, contMDiff_mul_left, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
⊢ (MDiffAt fun (x : G) ↦ g * h * x) 1

Tactic:
exact contMDiff_mul_left.contMDiffAt.mdifferentiableAt M

Premises used: ContMDiffAt.mdifferentiableAt, contMDiff_mul_left, ContMDiff.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
⊢ 1 = g⁻¹ * g

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
⊢ 1 = g⁻¹ * g

Tactic:
have A : 1 = g⁻¹ * g := by simp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
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)
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun (x : G) ↦ g⁻¹ * x) V g

Tactic:
simp only [mulInvariantVectorField, mpullback, inverse_mfderiv_mul_left]

Premises used: VectorField.mpullback, mulInvariantVectorField, inverse_mfderiv_mul_left
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
h : Eq.{u_4 + 1} (α := G → G) (fun (x : G) ↦ g * x) fun (b : G) ↦ g⁻¹⁻¹ * b
⊢ 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:
congr
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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.{u_4 + 1} (α := G → G) (fun (x : G) ↦ g * x) fun (b : G) ↦ g⁻¹⁻¹ * b

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
⊢ LT.lt (α := WithTop ℕ∞) 0 3

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
⊢ minSmoothness 𝕜 3 ≠ 0

Tactic:
have M : minSmoothness 𝕜 3 ≠ 0 := lt_of_lt_of_le (by simp) le_minSmoothness |>.ne'
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
rw : minSmoothness 𝕜 (HAdd.hAdd (α := WithTop ℕ∞) 2 1) = minSmoothness 𝕜 3
⊢ minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3

Tactic:
rw [← minSmoothness_add]

Premises used: minSmoothness_add
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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 𝕜 (HAdd.hAdd (α := WithTop ℕ∞) 2 1) = minSmoothness 𝕜 3

Tactic:
norm_num
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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

Tactic:
have A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3 := by
    rw [← minSmoothness_add]
    norm_num
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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.tangent (minSmoothness 𝕜 2) fg

Tactic:
have sfg : CMDiff (minSmoothness 𝕜 2) fg := contMDiff_zeroSection _ _
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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.tangent (minSmoothness 𝕜 2) fv

Tactic:
have sfv : CMDiff (minSmoothness 𝕜 2) fv := contMDiff_const
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁

Tactic:
have S₁ : CMDiff (minSmoothness 𝕜 2) F₁ := sfg.prodMk sfv
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂

Tactic:
have S₂ : CMDiff (minSmoothness 𝕜 2) F₂ := contMDiff_equivTangentBundleProd_symm
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
apply : ContMDiff (I.prod I) I (M' := G) (minSmoothness 𝕜 2 + 1) fun (p : G × G) ↦ p.1 * p.2
⊢ ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃

Tactic:
apply ContMDiff.contMDiff_tangentMap _ (m := minSmoothness 𝕜 2) le_rfl

Premises used: le_rfl, ContMDiff.contMDiff_tangentMap
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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
rw : ContMDiff (I.prod I) I (M' := G) (minSmoothness 𝕜 3) 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

Tactic:
rw [A]
-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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 𝕜 3) fun (p : G × G) ↦ p.1 * p.2

Tactic:
contMDiff_mul I (minSmoothness 𝕜 3)

Premises used: contMDiff_mul, minSmoothness, OfNat.ofNat