-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (hypothesis)
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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
hc :
  Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) (↑c : ↥(twoCochain R L M)) :
      L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
    (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
this :
  0 =
    HSub.hSub (β := M)
      (HAdd.hAdd (β := M)
        (HSub.hSub (β := M)
          (HAdd.hAdd (β := M)
            (HSub.hSub (α := M) (β := M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                      (a : L) → M)
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
                M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                  ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                      (a : L) → M)
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
                M))
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
                ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
              M))
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                  (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M))
        ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
              (a : L) → M)
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
          M))
      ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
              (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
            (a : L) → M)
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
        M)
⊢ HAdd.hAdd (α := M)
        ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
              (a : L) → M)
            (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
          M)
        (HAdd.hAdd (α := M) (β := M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
              M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2) :
              M) -
          Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)) -
      HSub.hSub (α := M)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2))
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)) =
    HAdd.hAdd (α := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                  (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
            M)
          (HSub.hSub (α := M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2))
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2))) -
        (HAdd.hAdd (α := M) (β := M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
                ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
              M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
                (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2) :
              M) -
          Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)) +
      (HAdd.hAdd (α := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                (a : L) → M)
              (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
            M)
          (HAdd.hAdd (α := M) (β := M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                  ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                      (a : L) → M)
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
                M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                  (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).2) :
                M) -
            Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)) -
        HSub.hSub (α := M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2))
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)))
have this₁ : (((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
      (a : L) → M)
    (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) =
  -HAdd.hAdd (β := M)
      (HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (α := M) (β := M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
              M)
            (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
                ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                      (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                    (a : L) → M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
              M))
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1
              ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                    (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1 :
                  (a : L) → M)
                (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
            M))
        ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
              (a : L) → M)
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1 :
          M))
      (-(((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
              (a : L) → M)
            (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).1
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1) :
        M)
Tactic: rw [← twoCochain_skew _ _ ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
      ← twoCochain_skew _ _ ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆, eq_sub_iff_add_eq,
      zero_add, neg_eq_iff_eq_neg] at this
Cleared hypotheses: this