-- 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, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆ : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1 : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
have h₁ : HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Y : (a : 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; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (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; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((Y : (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; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1)) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) -
      HSub.hSub (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
        ((Z : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Y : (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; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((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; 𝓘(𝕜, 𝕜), 𝕜⟯)
            ((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; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((X : (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; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Y : (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; 𝓘(𝕜, 𝕜), 𝕜⟯)
              ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f_1)) :
          C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯))
Tactic: simp only [commutator_apply, coe_add, map_sub, Pi.add_apply]