awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (goal)
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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, 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
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (k • ContMDiffMap.comp g f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
have rw₁ : HSMul.hSMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
  HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: rw [ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (goal)
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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, 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
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
rw :
  (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (k • ContMDiffMap.comp g f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
rw₁ :
  HSMul.hSMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (k • g) f) =
    HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
have rw₂ : HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
  HMul.hMul (β := 𝕜) k ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: rw [ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (goal)
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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, 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 g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ ({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f), map_add' := ⋯,
          map_smul' := ⋯ } :
        (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
      (g * g') =
    HSMul.hSMul (β := 𝕜) g
        (({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f),
                map_add' := ⋯, map_smul' := ⋯ : C^∞⟮I', M'; 𝕜⟯⟨y⟩ →ₗ[𝕜] 𝕜 } :
              (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
            g' :
          𝕜) +
      HSMul.hSMul (β := 𝕜) g'
        (({ toFun := fun (g : C^∞⟮I', M'; 𝕜⟯⟨y⟩) ↦ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f),
                map_add' := ⋯, map_smul' := ⋯ : C^∞⟮I', M'; 𝕜⟯⟨y⟩ →ₗ[𝕜] 𝕜 } :
              (a : C^∞⟮I', M'; 𝕜⟯⟨y⟩) → 𝕜)
            g :
          𝕜)
have dsimp : (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g * g') f) =
  HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
    HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.DerivationBundle (goal)
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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f_1 : C^∞⟮I, 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 g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ (v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp (g * g') f) =
    HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
      HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
have rw : HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : M') → 𝕜) y : 𝕜) ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g' : (a : M') → 𝕜) y : 𝕜)
      ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜) =
  HSMul.hSMul (β := 𝕜) g ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g' f) : 𝕜) +
    HSMul.hSMul (β := 𝕜) g' ((v : (a : C^∞⟮I, M; 𝕜⟯⟨x⟩) → 𝕜) (ContMDiffMap.comp g f) : 𝕜)
Tactic: rw [ContMDiffMap.mul_comp, Derivation.leibniz,
          PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply,
          PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply, 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
v w : GroupLieAlgebra I G
⊢ mulInvariantVectorField (v + w) = mulInvariantVectorField v + mulInvariantVectorField w
have h : ∀ (g : G), mulInvariantVectorField (v + w) g = (mulInvariantVectorField v + mulInvariantVectorField w) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : AddGroup G
c : 𝕜
v : AddGroupLieAlgebra I G
⊢ addInvariantVectorField (c • v) = c • addInvariantVectorField v
have h : ∀ (g : G), addInvariantVectorField (c • v) g = (c • addInvariantVectorField v) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
c : 𝕜
v : GroupLieAlgebra I G
⊢ mulInvariantVectorField (c • v) = c • mulInvariantVectorField v
have h : ∀ (g : G), mulInvariantVectorField (c • v) g = (c • mulInvariantVectorField v) g
Tactic: ext g
-- 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 h : G
⊢ 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))
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 h : G
M : minSmoothness 𝕜 3 ≠ 0
⊢ Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) id
have h₁ : ∀ (x : G), ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) x = id x
Tactic: ext x
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
⊢ 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))
have this : 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
-- 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 h : G
M : minSmoothness 𝕜 3 ≠ 0
this : Eq.{u_4 + 1} (α := G → G) ((fun (x : G) ↦ g⁻¹ * x) ∘ fun (x : G) ↦ g * x) id
⊢ 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))
have rw : Eq (α := TangentSpace I h →L[𝕜] TangentSpace I (id h)) (mfderiv% id h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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))
⊢ 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))
have 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))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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))
⊢ 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))
have rw₂ : Eq.{u_3 + 1} (α := TangentSpace I h →L[𝕜] TangentSpace I h) (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I h))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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 (g * h) →L[𝕜] TangentSpace I h)
    (ContinuousLinearMap.inverse ((mfderiv% fun (b : G) ↦ g * b) h)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h))
have 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))
Tactic: rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
    (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)] at A
Cleared hypotheses: A
-- 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 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
have h₁ : ∀ (x : G), ((fun (x : G) ↦ g * x) ∘ fun (x : G) ↦ g⁻¹ * x) x = id x
Tactic: ext x
-- 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 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)))
have this : 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
-- 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 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
⊢ 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)))
have rw : Eq (α := TangentSpace I (g * h) →L[𝕜] TangentSpace I (id (g * h))) (mfderiv% id (g * h))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h)))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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)))
⊢ 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)))
have 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)))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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)))
⊢ 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)))
have 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)))
Tactic: rw [this, id_eq, mfderiv_id]
-- 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 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 h)
    (ContinuousLinearMap.inverse ((mfderiv% fun (b : G) ↦ g * b) h)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h))
have 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)))
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]
-- 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 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 h)
    (ContinuousLinearMap.inverse ((mfderiv% fun (b : G) ↦ g * b) h)) ((mfderiv% fun (b : G) ↦ g⁻¹ * b) (g * h))
have 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)))
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'
Cleared hypotheses: A'