-- Module: Mathlib.Algebra.Lie.Cochain
Goal:
R : Type u_1
inst : CommRing R
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
a : ↥(twoCochain R L M)
x : R
x_1 : L
h :
  ∀ (x_2 x_3 : L),
    Eq.{u_3 + 1} (α := M)
      (((({
                    toFun := fun (y : L) ↦
                      {
                        toFun := fun (z : L) ↦
                          HSub.hSub (β := M)
                            (HAdd.hAdd (β := M)
                              (HSub.hSub (β := M)
                                (HAdd.hAdd (β := M)
                                  (HSub.hSub (α := M) (β := M)
                                    (⁅x • x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                                    (⁅y, (((a : (a : L) → L →ₗ[R] M) (x • x_1) : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                                  (⁅z, (((a : (a : L) → L →ₗ[R] M) (x • x_1) : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
                                ((((a : (a : L) → L →ₗ[R] M) ⁅x • x_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                              ((((a : (a : L) → L →ₗ[R] M) ⁅x • x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                            ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) (x • x_1) : M),
                        map_add' := ⋯, map_smul' := ⋯ },
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (a : L) → L →ₗ[R] M)
                x_2 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_3 :
        M)
      ((((HSMul.hSMul (α := R) (β := L →ₗ[R] L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x : R)
                    {
                      toFun := fun (y : L) ↦
                        {
                          toFun := fun (z : L) ↦
                            HSub.hSub (β := M)
                              (HAdd.hAdd (β := M)
                                (HSub.hSub (β := M)
                                  (HAdd.hAdd (β := M)
                                    (HSub.hSub (α := M) (β := M)
                                      (⁅x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                                      (⁅y, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                                    (⁅z, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
                                  ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                                ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                              ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M),
                          map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
                      map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M } :
                  (a : L) → L →ₗ[R] M)
                x_2 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_3 :
        M)
⊢ {
      toFun := fun (y : L) ↦
        {
          toFun := fun (z : L) ↦
            HSub.hSub (β := M)
              (HAdd.hAdd (β := M)
                (HSub.hSub (β := M)
                  (HAdd.hAdd (β := M)
                    (HSub.hSub (α := M) (β := M)
                      (⁅x • x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                      (⁅y, (((a : (a : L) → L →ₗ[R] M) (x • x_1) : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                    (⁅z, (((a : (a : L) → L →ₗ[R] M) (x • x_1) : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
                  ((((a : (a : L) → L →ₗ[R] M) ⁅x • x_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                ((((a : (a : L) → L →ₗ[R] M) ⁅x • x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
              ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) (x • x_1) : M),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := L →ₗ[R] L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x : R)
      {
        toFun := fun (y : L) ↦
          {
            toFun := fun (z : L) ↦
              HSub.hSub (β := M)
                (HAdd.hAdd (β := M)
                  (HSub.hSub (β := M)
                    (HAdd.hAdd (β := M)
                      (HSub.hSub (α := M) (β := M)
                        (⁅x_1, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                        (⁅y, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                      (⁅z, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
                    ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                  ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
                ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M),
            map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }

Tactic:
ext