-- 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 : 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
⊢ (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x + y)).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) z).1,
      HAdd.hAdd (α := M) (β := M)
          ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x + 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 + 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) z).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) (x + y)).2) =
    HAdd.hAdd (α := 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,
        HAdd.hAdd (α := M) (β := M)
            ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] 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) 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) z).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2)
      (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) (β := M)
            ((((↑(↑c : ↥(twoCochain R L M)) : L →ₗ[R] L →ₗ[R] 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
                (((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) z).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)
have simp : HAdd.hAdd (α := M) (β := M)
        ((((↑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)
        ((((↑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) +
      HAdd.hAdd (α := M)
        (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)
        (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) -
    HAdd.hAdd (α := M)
      (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
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2) =
  HAdd.hAdd (α := M) (β := M)
        ((((↑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) 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) z).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x).2 +
    (HAdd.hAdd (α := M) (β := M)
        ((((↑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
            (((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) z).1
        (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2)
Tactic: simp only [of_symm_add, Prod.fst_add, add_lie, twoCochain_val_apply, map_add,
      LinearMap.add_apply, Prod.snd_add, lie_add, Prod.mk_add_mk, Prod.mk.injEq, true_and]