awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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
H₁ :
  ∀ (f : C^∞⟮I, G; 𝕜⟯⟨g * 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 :
        𝕜)
      ((((𝒅ₕ (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 :
        𝕜)
⊢ Eq (α := PointDerivation I (g * h))
    ((evalAt (g * h) : (a : LeftInvariantDerivation I G) → PointDerivation I (g * h)) X : PointDerivation I (g * h))
    ((𝒅ₕ (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))

Tactic:
ext f
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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 g) ((𝑳 I h : (a : G) → G) 1) ∘ₗ 𝒅 (𝑳 I h) 1 :
                  PointDerivation.{u_1, u_2, u_3, u_4} I (M := G) 1 →ₗ[𝕜]
                    PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
                (a : PointDerivation I 1) → PointDerivation I (((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I (M := G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) 1 : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨((𝑳 I g).comp (𝑳 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)) :
      𝕜)
⊢ 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 :
      𝕜)
    ((((𝒅ₕ (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 :
      𝕜)

Tactic:
rw [← left_invariant, hfdifferential_apply, hfdifferential_apply, L_mul, fdifferential_comp,
    fdifferential_apply]

Premises used: LeftInvariantDerivation.left_invariant, fdifferential_apply, L_mul, fdifferential_comp, hfdifferential_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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 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)) :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((((𝒅 (𝑳 I g) ((𝑳 I h : (a : G) → G) 1) ∘ₗ 𝒅 (𝑳 I h) 1 :
                  PointDerivation.{u_1, u_2, u_3, u_4} I (M := G) 1 →ₗ[𝕜]
                    PointDerivation I (M := G) ((𝑳 I g : (a : G) → G) ((𝑳 I h : (a : G) → G) 1 : G) : G)) :
                (a : PointDerivation I 1) → PointDerivation I (((𝑳 I g).comp (𝑳 I h) : (a : G) → G) 1))
              ((evalAt 1 : (a : LeftInvariantDerivation I G) → PointDerivation I 1) X) :
            PointDerivation I (M := G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) 1 : G)) :
          (a : C^∞⟮I, G; 𝕜⟯⟨((𝑳 I g).comp (𝑳 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)) :
      𝕜)

Tactic:
simp only [ContMDiffMap.comp_apply, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, ContMDiffMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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)) :
      𝕜)
H₃ 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)) :
      𝕜)
⊢ 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)) :
      𝕜)

Tactic:
rw [fdifferential_apply, ← hfdifferential_apply (smoothLeftMul_one I h), left_invariant]

Premises used: LeftInvariantDerivation.left_invariant, fdifferential_apply, smoothLeftMul_one, hfdifferential_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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 :
  ∀ (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 :
        𝕜)
⊢ 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)))

Tactic:
ext h
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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
H₁ :
  ∀ (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 :
        𝕜)
⊢ 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)

Tactic:
ext f
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
            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)
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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⟩
hX :
  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; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
            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; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)
⊢ 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)
                (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        ((X : (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)
              (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)

Tactic:
have hY := Derivation.congr_fun (left_invariant' g Y) (X f)
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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⟩
hX :
  Eq.{u_1 + 1} (α := 𝕜)
    (((((↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              (ContMDiffMap.comp ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g)) :
            C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        1 :
      𝕜)
    ((((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; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)
hY :
  Eq.{u_1 + 1} (α := 𝕜)
    (((((↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              (ContMDiffMap.comp ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) (𝑳 I g)) :
            C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        1 :
      𝕜)
    ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((((↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (ContMDiffMap.comp f (𝑳 I g))) :
            C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        1 :
      𝕜)
    ((((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:
rw [comp_L] at hX hY

Premises used: LeftInvariantDerivation.comp_L
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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⟩
hX :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (ContMDiffMap.comp f (𝑳 I g))) :
            C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        1 :
      𝕜)
    ((((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; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)
hY :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (ContMDiffMap.comp f (𝑳 I g))) :
            C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        1 :
      𝕜)
    ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
            PointDerivation I g) :
          (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
        ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      𝕜)
⊢ HSub.hSub (α := 𝕜) (β := 𝕜)
      ((((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; 𝓘(𝕜, 𝕜), 𝕜⟯) :
        𝕜)
      ((((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
                (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
              PointDerivation I g) :
            (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
          ((X : (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; 𝓘(𝕜, 𝕜), 𝕜⟯),
              (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆ :
          PointDerivation I g) :
        (a : C^∞⟮I, G; 𝕜⟯⟨g⟩) → 𝕜)
      f

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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
X Y : LeftInvariantDerivation I G
⊢ Eq (α := (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (⇑⁅X, Y⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (⇑⁅(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
          (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)⁆ :
      (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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
X Y : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ (⁅X, Y⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f =
    HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
          ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
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
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; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ ⁅X + Y, Z⁆ = ⁅X, Z⁆ + ⁅Y, Z⁆

Tactic:
ext1