-- 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 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h :
  (↑c' : ↥(twoCochain R L M)) =
    HAdd.hAdd (β := ↥(twoCochain R L M)) (↑c : ↥(twoCochain R L M))
      ((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) x : ↥(twoCochain R L M))
x_1 y : ofTwoCocycle c
simp :
  HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M)
          ((((↑c : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M)
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).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) x_1).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) y).1
          (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2)
      ((x : (a : L) → M)
          (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1
            (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).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).1 :
                (a : L) → M)
              (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 :
            M)
          (HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M)
              (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1
                  ((x : (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) y).1
                  ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1) :
                M))
            ((x : (a : L) → M)
                (Bracket.bracket (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1
                  (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
              M)) +
        HSub.hSub (α := M) (β := M)
          (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).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) x_1).1
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1) :
            M) -
      HSub.hSub (α := M) (β := 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) x_1).2 :
          M)
        (Bracket.bracket.{u_3, u_4} (L := L) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1
            ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1) :
          M)
⊢ Eq (α := L × M)
    ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) ⁅x_1, y⁆).1,
      HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) ⁅x_1, y⁆).2 : M)
        ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) ⁅x_1, y⁆).1 : M))
    (((ofProd c').symm : (a : ofTwoCocycle c') → L × M)
      (Bracket.bracket (L := ofTwoCocycle c')
        ((ofProd c' : (a : L × M) → ofTwoCocycle c')
            ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1,
              HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).2 : M)
                ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) x_1).1 : M)) :
          ofTwoCocycle c')
        ((ofProd c' : (a : L × M) → ofTwoCocycle c')
          ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1,
            HSub.hSub (α := M) (β := M) ((((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).2 : M)
              ((x : (a : L) → M) (((ofProd c).symm : (a : ofTwoCocycle c) → L × M) y).1 : M)))))

Tactic:
simp [bracket_ofTwoCocycle, h]

Premises used: LieAlgebra.bracket_ofTwoCocycle