-- Module: Mathlib.Algebra.Lie.Extension
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
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) x : E.L) ((s : (a : L) → E.L) ⁅y, z⁆) : 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) ⁅x, z⁆) : E.L) +
            HSub.hSub (α := E.L) (β := E.L)
              (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)) :
                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) ⁅x, y⁆ : E.L) ((s : (a : L) → E.L) z) : E.L)
            (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅y, z⁆⁆ : E.L)
              ((s : (a : L) → E.L) ⁅y, ⁅x, z⁆⁆ : E.L)) +
        HSub.hSub (α := E.L)
          (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅x, z⁆ : E.L) ((s : (a : L) → E.L) y) : E.L)
          (HSub.hSub (α := E.L) (β := E.L) ((s : (a : L) → E.L) ⁅x, ⁅z, y⁆⁆ : E.L)
            ((s : (a : L) → E.L) ⁅z, ⁅x, y⁆⁆ : E.L)) -
      HSub.hSub (α := E.L) (Bracket.bracket (L := E.L) ((s : (a : L) → E.L) ⁅y, z⁆ : 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) ⁅z, ⁅y, x⁆⁆ : E.L)) =
    0
⊢ Eq.{u_4 + 1} (α := M)
    ((((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
                          (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                            Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                            ((E.twoCocycleAux hs).compr₂ (↑E.toKer.symm.toLinearEquiv : ↥E.proj.ker →ₗ[R] M)) ⋯) :
                        L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    ((((((0 : (a : L) → L →ₗ[R] L →ₗ[R] M) x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M)
        z :
      M)

Tactic:
suffices ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ -
        (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) + (⁅s z, ⁅s x, s y⁆⁆ - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - s ⁅z, ⁅x, y⁆⁆)) -
        (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - s ⁅z, ⁅y, x⁆⁆)) = 0 by
      set h := E.proj_surjective.hasRightInverse
      have aux (u : L) (v : E.proj.ker) : ⁅h.choose u, v⁆ = ⁅s u, v⁆ := by
        rw [← E.lie_apply_proj_of_leftInverse_eq hs, h.choose_spec _]
      simpa [← map_sub, ← map_add, ← twoCochain_val_apply, Subtype.ext_iff, twoCocycleAux, aux]