-- 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
x x_1 : oneCochain R L M
a :
  ∀ (x_2 x_3 : L),
    Eq.{u_3 + 1} (α := M)
      (((((↑(Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                        Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                        {
                          toFun := fun (x_4 : L) ↦
                            {
                              toFun := fun (y : L) ↦
                                HSub.hSub (β := M)
                                  (HSub.hSub (α := M) (β := M) (⁅x_4, (x + x_1 : (a : L) → M) y⁆ : M)
                                    (⁅y, (x + x_1 : (a : L) → M) x_4⁆ : M))
                                  ((x + x_1 : (a : L) → M) ⁅x_4, y⁆ : M),
                              map_add' := ⋯, map_smul' := ⋯ },
                          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)
      (((((↑(HAdd.hAdd (α := ↥(twoCochain R L M))
                        (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                          Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                          {
                            toFun := fun (x_4 : L) ↦
                              {
                                toFun := fun (y : L) ↦
                                  HSub.hSub (β := M)
                                    (HSub.hSub (α := M) (β := M) (⁅x_4, (x : (a : L) → M) y⁆ : M)
                                      (⁅y, (x : (a : L) → M) x_4⁆ : M))
                                    ((x : (a : L) → M) ⁅x_4, y⁆ : M),
                                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
                            map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }
                          ⋯)
                        (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
                          Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
                          {
                            toFun := fun (x : L) ↦
                              {
                                toFun := fun (y : L) ↦
                                  HSub.hSub (β := M)
                                    (HSub.hSub (α := M) (β := M) (⁅x, (x_1 : (a : L) → M) y⁆ : M)
                                      (⁅y, (x_1 : (a : L) → M) x⁆ : M))
                                    ((x_1 : (a : L) → M) ⁅x, y⁆ : M),
                                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
                            map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }
                          ⋯)) :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                x_2 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_3 :
        M)
⊢ Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
      Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
      {
        toFun := fun (x_2 : L) ↦
          {
            toFun := fun (y : L) ↦
              HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x_2, (x + x_1 : (a : L) → M) y⁆ : M)
                  (⁅y, (x + x_1 : (a : L) → M) x_2⁆ : M))
                ((x + x_1 : (a : L) → M) ⁅x_2, y⁆ : M),
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }
      ⋯ =
    HAdd.hAdd (α := ↥(twoCochain R L M))
      (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
        Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
        {
          toFun := fun (x_2 : L) ↦
            {
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x_2, (x : (a : L) → M) y⁆ : M) (⁅y, (x : (a : L) → M) x_2⁆ : M))
                  ((x : (a : L) → M) ⁅x_2, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
          map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }
        ⋯)
      (Subtype.mk (p := fun (x : L →ₗ[R] L →ₗ[R] M) ↦
        Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) x)
        {
          toFun := fun (x : L) ↦
            {
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x, (x_1 : (a : L) → M) y⁆ : M) (⁅y, (x_1 : (a : L) → M) x⁆ : M))
                  ((x_1 : (a : L) → M) ⁅x, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M },
          map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L →ₗ[R] M }
        ⋯)

Tactic:
ext