-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (goal)
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
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)
have a : HAdd.hAdd (α := M) (β := M) (⁅x_2, (x : (a : L) → M) x_3⁆ : M) (⁅x_2, (x_1 : (a : L) → M) x_3⁆ : M) -
      HAdd.hAdd (α := M) (β := M) (⁅x_3, (x : (a : L) → M) x_2⁆ : M) (⁅x_3, (x_1 : (a : L) → M) x_2⁆ : M) -
    HAdd.hAdd (α := M) (β := M) ((x : (a : L) → M) ⁅x_2, x_3⁆ : M) ((x_1 : (a : L) → M) ⁅x_2, x_3⁆ : M) =
  HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x_2, (x : (a : L) → M) x_3⁆ : M) (⁅x_3, (x : (a : L) → M) x_2⁆ : M))
      ((x : (a : L) → M) ⁅x_2, x_3⁆ : M) +
    HSub.hSub (β := M)
      (HSub.hSub (α := M) (β := M) (⁅x_2, (x_1 : (a : L) → M) x_3⁆ : M) (⁅x_3, (x_1 : (a : L) → M) x_2⁆ : M))
      ((x_1 : (a : L) → M) ⁅x_2, x_3⁆ : M)
Tactic: simp