-- 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_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; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((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 : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                (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 (α := 𝕜) (β := 𝕜)
      ((((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
                (((↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                    (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
                  (ContMDiffMap.comp f (𝑳 I g))) :
              C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
            (a : G) → 𝕜)
          1 :
        𝕜)
      (((((↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
                  (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)
            ⁅(↑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 H₁ : ∀
  (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 (α := 𝕜) (β := 𝕜)
      ((((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 :
        𝕜)
      ((((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)
            ⁅(↑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: rw [coe_derivation] at hX hY ⊢
Cleared hypotheses: hX, hY