-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
s : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s : (a : L) → E.L)
x y z : L
hjac :
  Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L)
      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) y)) =
    -HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
          E.L)
hja :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : E.L)
hj :
  Eq.{u_5 + 1} (α := E.L) ((s : (a : L) → E.L) ⁅z, ⁅y, x⁆⁆ : E.L)
    (-(s : (a : L) → E.L) (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆) : E.L)
⊢ HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (-Bracket.bracket (L := E.L) ((s : (a : L) → E.L) (-⁅z, y⁆) : E.L) ((s : (a : L) → E.L) x) : E.L) -
              HSub.hSub (α := E.L) (β := E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                    (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                  E.L)
                (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) (-⁅z, x⁆)) : E.L) +
            HSub.hSub (β := E.L)
              (-HSub.hSub (α := E.L) (β := E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                    E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                      (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                    E.L))
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
          HSub.hSub (α := E.L)
            (-Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, -⁅z, y⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, -⁅z, x⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (-Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) (-⁅z, x⁆)) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            (-(s : (a : L) → E.L) (⁅x, -⁅z, y⁆⁆ - ⁅y, -⁅z, x⁆⁆) : E.L)) -
      HSub.hSub (α := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) (-⁅z, y⁆) : E.L) ((s : (a : L) → E.L) x) : E.L)
        (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)
          (-(s : (a : L) → E.L) (⁅y, -⁅z, x⁆⁆ - ⁅x, -⁅z, y⁆⁆) : E.L)) =
    0
have h : HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅z, y⁆ : E.L) ((s : (a : L) → E.L) x) : E.L) -
            HAdd.hAdd (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅z, x⁆) : E.L) +
          HSub.hSub (β := E.L)
            (HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L) ((s : (a : L) → E.L) z)) :
                E.L)
              (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) x : E.L)
                  (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) z)) :
                E.L))
            (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L) -
        HSub.hSub (α := E.L)
          (-Bracket.bracket (L := E.L) ((s : (a : L) → E.L) z : E.L) ((s : (a : L) → E.L) ⁅x, y⁆) : E.L)
          (HAdd.hAdd (α := E.L) (β := E.L) (-(s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L)) +
      HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) y : E.L) ((s : (a : L) → E.L) ⁅z, x⁆) : E.L)
        ((s : (a : L) → E.L) ⁅y, ⁅z, x⁆⁆ : E.L) -
    HSub.hSub (α := E.L) (β := E.L)
      (-Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅z, y⁆ : E.L) ((s : (a : L) → E.L) x) : E.L)
      ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L) =
  0
Tactic: simp only [map_neg, neg_lie, neg_neg, neg_sub, lie_neg, sub_neg_eq_add,
      sub_add_cancel_right, map_add, neg_add_rev]