awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
v : PointDerivation I x
g : C^∞⟮I', M'; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 f x : (a : PointDerivation I x) → PointDerivation I' ((f : (a : M) → M') x)) v :
            PointDerivation.{u_1, u_5, u_6, u_7} I' (M := M') ((f : (a : M) → M') x : M')) :
          (a : C^∞⟮I', M'; 𝕜⟯⟨(f : (a : M) → M') x⟩) → 𝕜)
        g :
      𝕜)
    ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (g.comp f) : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : (f : (a : M) → M') x = y
v : PointDerivation I x
g : C^∞⟮I', M'; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅ₕ h : (a : PointDerivation I x) → PointDerivation I' y) v : PointDerivation I' y) :
          (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
        g :
      𝕜)
    ((((𝒅 f x : (a : PointDerivation I x) → PointDerivation I' ((f : (a : M) → M') x)) v :
            PointDerivation.{u_1, u_5, u_6, u_7} I' (M := M') ((f : (a : M) → M') x : M')) :
          (a : C^∞⟮I', M'; 𝕜⟯⟨(f : (a : M) → M') x⟩) → 𝕜)
        g :
      𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.DerivationBundle
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
g : C^∞⟮I', M'; I'', M''⟯
f : C^∞⟮I, M; I', M'⟯
x : M
⊢ 𝒅 (g.comp f) x = 𝒅 g ((f : (a : M) → M') x) ∘ₗ 𝒅 f x

Tactic:
rfl

Premises used: fdifferential, Derivation.mk', ContMDiffMap, PointedContMDiffMap, hfdifferential, ContMDiffMap.comp, rfl
-- 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
v w : GroupLieAlgebra I G
h : ∀ (g : G), mulInvariantVectorField (v + w) g = (mulInvariantVectorField v + mulInvariantVectorField w) g
⊢ mulInvariantVectorField (v + w) = 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
v w : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (v + w) g = (mulInvariantVectorField v + mulInvariantVectorField w) g

Tactic:
simp [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_5
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : AddGroup G
c : 𝕜
v : AddGroupLieAlgebra I G
h : ∀ (g : G), addInvariantVectorField (c • v) g = (c • addInvariantVectorField v) g
⊢ addInvariantVectorField (c • v) = c • addInvariantVectorField v

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_5
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : AddGroup G
c : 𝕜
v : AddGroupLieAlgebra I G
g : G
⊢ addInvariantVectorField (c • v) g = (c • addInvariantVectorField v) g

Tactic:
simp [addInvariantVectorField]

Premises used: addInvariantVectorField
-- 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
c : 𝕜
v : GroupLieAlgebra I G
h : ∀ (g : G), mulInvariantVectorField (c • v) g = (c • mulInvariantVectorField v) g
⊢ mulInvariantVectorField (c • v) = c • mulInvariantVectorField v

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
c : 𝕜
v : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (c • v) g = (c • mulInvariantVectorField v) g

Tactic:
simp [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
v w : GroupLieAlgebra I G
⊢ ⁅v, w⁆ = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1

Tactic:
rfl

Premises used: rfl
-- 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 h : 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
g h : 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
g h : G
M : minSmoothness 𝕜 3 ≠ 0
h₁ : ∀ (x : G), ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) x = id x
⊢ Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) id

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 h : G
M : minSmoothness 𝕜 3 ≠ 0
x : G
⊢ ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) x = id x

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 h : G
M : minSmoothness 𝕜 3 ≠ 0
⊢ Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) id

Tactic:
have : (fun x ↦ g⁻¹ * x) ∘ (fun x ↦ g * x) = id := by ext x; 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
this : Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) id
rw :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (id h)) (mfderiv% id h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
rw₁ :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I h) (mfderiv% id h : TangentSpace I h →L[𝕜] TangentSpace I (id h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := TangentSpace I h →L[𝕜] TangentSpace I h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
⊢ Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (mfderiv% ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))

Tactic:
rw [this, id_eq, mfderiv_id]

Premises used: id_eq, mfderiv_id
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (mfderiv% ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
⊢ Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))

Tactic:
rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
    (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)] at A

Premises used: mfderiv_comp, 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
h₁ : ∀ (x : G), ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) x = id x
⊢ Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) id

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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
x : G
⊢ ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) x = id x

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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
⊢ Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) id

Tactic:
have : (fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x) = id := by ext x; 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
this : Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) id
rw :
  Eq (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I (id (g * h))) (mfderiv% id (g * h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
rw₁ :
  Eq (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I (g * h))
    (mfderiv% id (g * h) : TangentSpace I (g * h) →L[𝕜] TangentSpace I (id (g * h)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I (g * h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))) (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
⊢ Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (mfderiv% ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))

Tactic:
rw [this, id_eq, mfderiv_id]

Premises used: id_eq, mfderiv_id
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
⊢ Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (mfderiv% ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))

Tactic:
have A' : mfderiv% ((fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x)) (g * h) =
      ContinuousLinearMap.id _ _ := by
    have : (fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x) = id := by ext x; simp
    rw [this, id_eq, mfderiv_id]
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
A' :
  Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (mfderiv% ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
⊢ Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I h) ((mfderiv% fun (x : G) ↦ g * x) h)
      ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))

Tactic:
rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
    (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M), inv_mul_cancel_left g h] at A'

Premises used: mfderiv_comp, ContMDiffAt.mdifferentiableAt, inv_mul_cancel_left, 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
A' :
  Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I h) ((mfderiv% fun (x : G) ↦ g * x) h)
      ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
⊢ Eq (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I h)
    (ContinuousLinearMap.inverse ((mfderiv% fun (b : G) ↦ g * b) h)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h))

Tactic:
ContinuousLinearMap.inverse_eq A' A

Premises used: ContinuousLinearMap.inverse_eq
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
A :
  Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (g * h)) ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h))
      ((mfderiv% fun (x : G) ↦ g * x) h))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
A' :
  Eq (α :=
    TangentSpace I (g * h) →L[𝕜] TangentSpace I (M := G) (((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I h) ((mfderiv% fun (x : G) ↦ g * x) h)
      ((mfderiv% fun (x : G) ↦ g⁻¹ * x) (g * h)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
⊢ Eq (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I h)
    (ContinuousLinearMap.inverse ((mfderiv% fun (b : G) ↦ g * b) h)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h))

Tactic:
exact ContinuousLinearMap.inverse_eq A' A

Premises used: ContinuousLinearMap.inverse_eq
-- 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
⊢ 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
g : 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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : ∀ (h : G), mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) h = mulInvariantVectorField v h
⊢ mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) = mulInvariantVectorField v

Tactic:
ext h
-- 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₁ :
  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))
⊢ mpullback I I (fun (x : G) ↦ g * x) (mulInvariantVectorField v) h = mulInvariantVectorField v h

Tactic:
simp only [mpullback, inverse_mfderiv_mul_left, mulInvariantVectorField]

Premises used: VectorField.mpullback, mulInvariantVectorField, inverse_mfderiv_mul_left