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
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:
exact contMDiff_mul I (minSmoothness 𝕜 3)

Premises used: contMDiff_mul, minSmoothness, OfNat.ofNat
-- 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).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)
-- 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
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁)

Tactic:
S
-- 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
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)
h₁ :
  ∀ (g : G),
    g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I) →
      mulInvariantVectorField v g = (((F₃ ∘ F₂) ∘ F₁) g).snd (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⟩

Tactic:
convert! S with g
-- 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
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
g : G
⊢ g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I)

Tactic:
simp [F₁, F₂, F₃, fg, fv]
-- 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
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
g : G
e_4 : g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +instances [mulInvariantVectorField]

Premises used: mulInvariantVectorField
-- 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
g : G
⊢ ContMDiffAt 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⟩) g

Tactic:
(contMDiff_mulInvariantVectorField v).contMDiffAt

Premises used: contMDiff_mulInvariantVectorField, 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
v : GroupLieAlgebra I G
⊢ LT.lt (α := WithTop ℕ∞) 0 2

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
g : G
⊢ LT.lt (α := WithTop ℕ∞) 0 2

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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
h :
  ∀ (g : G),
    mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
      mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)

Tactic:
ext g
-- 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
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
h₃ : minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g

Tactic:
rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
    mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]

Premises used: VectorField.mpullback_mlieBracket, mpullback_mulInvariantVectorField, mulInvariantVectorField_eq_mpullback
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (M' := G) (minSmoothness 𝕜 3) (fun (x : G) ↦ g⁻¹ * x) g

Tactic:
contMDiffAt_mul_left

Premises used: contMDiffAt_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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (M' := G) (minSmoothness 𝕜 3) (fun (x : G) ↦ g⁻¹ * x) g

Tactic:
exact contMDiffAt_mul_left

Premises used: contMDiffAt_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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LE.le (α := ℕ) 2 3
⊢ LE.le (α := WithTop ℕ∞) 2 3

Tactic:
norm_cast
-- 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
inst_8 : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3

Tactic:
exact minSmoothness_monotone (by norm_cast)

Premises used: minSmoothness_monotone
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
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)
⊢ ⁅u + v, w⁆ = ⁅u, w⁆ + ⁅v, w⁆

Tactic:
simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]

Premises used: GroupLieAlgebra.bracket_def, mulInvariantVectorField_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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hV : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1
hV₁ : (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 w) 1)
      (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1)

Tactic:
rw [mlieBracket_add_left]

Premises used: VectorField.mlieBracket_add_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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField u x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
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)
⊢ ⁅u, v + w⁆ = ⁅u, v⁆ + ⁅u, w⁆

Tactic:
simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]

Premises used: GroupLieAlgebra.bracket_def, mulInvariantVectorField_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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
hW : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField v x⟩) 1
hW₁ : (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w 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)

Tactic:
rw [mlieBracket_add_right]

Premises used: VectorField.mlieBracket_add_right
-- 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
inst_8 : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun (x : G) ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
mdifferentiableAt_mulInvariantVectorField _

Premises used: mdifferentiableAt_mulInvariantVectorField