awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
H₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I (M := G) ((𝑳 I h : (a : G) → G) 1 : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I h : (a : G) → G) 1⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
H₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅ₕ (f := 𝑳 I h) ⋯ : (a : PointDerivation I 1) → PointDerivation I h)
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) :
                (a : PointDerivation I ((𝑳 I h : (a : G) → G) 1)) →
                  PointDerivation I ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)))
              ((𝒅 (𝑳 I h) 1 : (a : PointDerivation I 1) → PointDerivation I ((𝑳 I h : (a : G) → G) 1))
                ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X)) :
            PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1)⟩) → 𝕜)
        f :
      𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (ContMDiffMap.comp f (𝑳 I g)) :
      𝕜)
have H₃ : Eq.{u_1 + 1} (α := 𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
  ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
        (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
      (ContMDiffMap.comp f (𝑳 I g)) :
    𝕜)
Tactic: rw [fdifferential_apply, ← hfdifferential_apply (smoothLeftMul_one I h), left_invariant]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g))
    ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)))
have h : ∀ (h : G),
  Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
Tactic: ext h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
have h₁ : Eq.{u_1 + 1} (α := 𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      ((𝑳 I g : (a : G) → G) h : G) :
    𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      h :
    𝕜)
Tactic: rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
h₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
        ((𝑳 I g : (a : G) → G) h : G) :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
have h₂ : Eq.{u_1 + 1} (α := 𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜) (g * h) : 𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      h :
    𝕜)
Tactic: rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
h₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
        ((𝑳 I g : (a : G) → G) h : G) :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜) (g * h) : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
have h₃ : Eq.{u_1 + 1} (α := 𝕜)
  ((((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
      f :
    𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      h :
    𝕜)
Tactic: rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
h₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
        ((𝑳 I g : (a : G) → G) h : G) :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜) (g * h) : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₃ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
have h₄ : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I h) → PointDerivation I (g * h))
            ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
          PointDerivation I (g * h)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
      f :
    𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      h :
    𝕜)
Tactic: rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (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
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
h₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
        ((𝑳 I g : (a : G) → G) h : G) :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜) (g * h) : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₃ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₄ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I h) → PointDerivation I (g * h))
              ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
            PointDerivation I (g * h)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g * h⟩) → 𝕜)
        f :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g) : (a : G) → 𝕜) h : 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
have h₅ : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅 (𝑳 I g) h : (a : PointDerivation I h) → PointDerivation I ((𝑳 I g : (a : G) → G) h))
            ((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X) :
          PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) h : G)) :
        (a : C^∞⟮I, G; 𝕜⟯⟨(𝑳 I g : (a : G) → G) h⟩) → 𝕜)
      f :
    𝕜)
  ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) : (a : G) → 𝕜)
      h :
    𝕜)
Tactic: rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g_1 h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
⊢ Eq (α := PointDerivation I g)
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
            (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆) :
      PointDerivation I g)
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
          (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆ :
      PointDerivation I g)
have H₁ : ∀ (f : C^∞⟮I, G; 𝕜⟯⟨g⟩),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
              ((Derivation.evalAt 1 :
                  (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
                ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
                  (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        f :
      𝕜)
    ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
                (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆ :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        f :
      𝕜)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g_1 h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f_1 f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
              ((Derivation.evalAt 1 :
                  (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
                ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
                  (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        f :
      𝕜)
    ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              ⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
                (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆ :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        f :
      𝕜)
have hX : Eq.{u_1 + 1} (α := 𝕜)
  ((((𝒅ₕ (f := 𝑳 I g) sorry : (a : PointDerivation I 1) → PointDerivation I g)
            ((Derivation.evalAt 1 :
                (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
              (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
          PointDerivation I g) :
        (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
    𝕜)
  ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
            (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          PointDerivation I g) :
        (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
    𝕜)
Tactic: have hX := Derivation.congr_fun (left_invariant' g X) (Y f)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X + Y, Z⁆ = ⁅X, Z⁆ + ⁅Y, Z⁆
have h₁ : ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
  Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X + Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Z⁆ + ⁅Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X + Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Z⁆ + ⁅Y, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
have h₁ : HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
    HAdd.hAdd (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
  HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) +
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X_1 Y_1 : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, Y + Z⁆ = ⁅X, Y⁆ + ⁅X, Z⁆
have h₁ : ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
  Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Y + Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    ((⁅X, Y⁆ + ⁅X, Z⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
Tactic: ext1