-- 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 x_1 x_2 : L
h :
  ∀ (x_3 : L),
    Eq.{u_3 + 1} (α := M)
      (({
              toFun := fun (z : L) ↦
                HSub.hSub (β := M)
                  (HAdd.hAdd (β := M)
                    (HSub.hSub (β := M)
                      (HAdd.hAdd (β := M)
                        (HSub.hSub (α := M) (β := M)
                          (⁅x, (((a : (a : L) → L →ₗ[R] M) (x_1 + x_2) : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                          (⁅x_1 + x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                        (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2)⁆ : M))
                      ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1 + x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                    ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2) : M))
                  ((((a : (a : L) → L →ₗ[R] M) ⁅x_1 + x_2, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : L) → M)
          x_3 :
        M)
      ((HAdd.hAdd (α := L →ₗ[R] M)
              {
                toFun := fun (z : L) ↦
                  HSub.hSub (β := M)
                    (HAdd.hAdd (β := M)
                      (HSub.hSub (β := M)
                        (HAdd.hAdd (β := M)
                          (HSub.hSub (α := M) (β := M)
                            (⁅x, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                            (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                          (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M))
                        ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                      ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
                    ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M }
              {
                toFun := fun (z : L) ↦
                  HSub.hSub (β := M)
                    (HAdd.hAdd (β := M)
                      (HSub.hSub (β := M)
                        (HAdd.hAdd (β := M)
                          (HSub.hSub (α := M) (β := M)
                            (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                            (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                          (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
                        ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
                      ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
                    ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M } :
            (a : L) → M)
          x_3 :
        M)
⊢ {
      toFun := fun (z : L) ↦
        HSub.hSub (β := M)
          (HAdd.hAdd (β := M)
            (HSub.hSub (β := M)
              (HAdd.hAdd (β := M)
                (HSub.hSub (α := M) (β := M)
                  (⁅x, (((a : (a : L) → L →ₗ[R] M) (x_1 + x_2) : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                  (⁅x_1 + x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2)⁆ : M))
              ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1 + x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) (x_1 + x_2) : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x_1 + x_2, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := L →ₗ[R] M)
      {
        toFun := fun (z : L) ↦
          HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (β := M)
                (HAdd.hAdd (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                    (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                  (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M))
                ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
              ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M }
      {
        toFun := fun (z : L) ↦
          HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (β := M)
                (HAdd.hAdd (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                    (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M))
                  (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
                ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
              ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, z⁆ : L →ₗ[R] M) : (a : L) → M) x : M),
        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M }

Tactic:
ext