-- 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 : 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 :
      𝕜)
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 :
      𝕜)
h₆ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((evalAt h : (a : LeftInvariantDerivation I G) → PointDerivation I h) X : PointDerivation I h) :
          (a : C^∞⟮I, G; 𝕜⟯⟨h⟩) → 𝕜)
        (f.comp (𝑳 I g)) :
      𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : G) → 𝕜)
        h :
      𝕜)
h₇ h₈ :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (f.comp (𝑳 I g)) : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
          (a : 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 :
      𝕜)

Tactic:
rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]

Premises used: fdifferential_apply, hfdifferential_apply, L_apply, LeftInvariantDerivation.evalAt_mul, ContMDiffMap.comp_apply, LeftInvariantDerivation.evalAt_apply