awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : oneCochain R L M
x x_1 x_2 : L
h :
  HAdd.hAdd (α := M) (β := M) (⁅x, (f : (a : L) → M) x_2⁆ : M) (⁅x_1, (f : (a : L) → M) x_2⁆ : M) -
        HAdd.hAdd (α := M) (β := M) (⁅x_2, (f : (a : L) → M) x⁆ : M) (⁅x_2, (f : (a : L) → M) x_1⁆ : M) -
      HAdd.hAdd (α := M) (β := M) ((f : (a : L) → M) ⁅x, x_2⁆ : M) ((f : (a : L) → M) ⁅x_1, x_2⁆ : M) =
    HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) x_2⁆ : M) (⁅x_2, (f : (a : L) → M) x⁆ : M))
        ((f : (a : L) → M) ⁅x, x_2⁆ : M) +
      HSub.hSub (β := M)
        (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) x_2⁆ : M) (⁅x_2, (f : (a : L) → M) x_1⁆ : M))
        ((f : (a : L) → M) ⁅x_1, x_2⁆ : M)
⊢ Eq.{u_3 + 1} (α := M)
    (({
            toFun := fun (y : L) ↦
              HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x + x_1, (f : (a : L) → M) y⁆ : M)
                  (⁅y, (f : (a : L) → M) (x + x_1)⁆ : M))
                ((f : (a : L) → M) ⁅x + x_1, y⁆ : M),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : L) → M)
        x_2 :
      M)
    ((HAdd.hAdd (α := L →ₗ[R] M)
            {
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x⁆ : M))
                  ((f : (a : L) → M) ⁅x, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M }
            {
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x_1⁆ : M))
                  ((f : (a : L) → M) ⁅x_1, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M } :
          (a : L) → M)
        x_2 :
      M)

Tactic:
simp
-- 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
f : oneCochain R L M
x x_1 x_2 : L
⊢ HAdd.hAdd (α := M) (β := M) (⁅x, (f : (a : L) → M) x_2⁆ : M) (⁅x_1, (f : (a : L) → M) x_2⁆ : M) -
        HAdd.hAdd (α := M) (β := M) (⁅x_2, (f : (a : L) → M) x⁆ : M) (⁅x_2, (f : (a : L) → M) x_1⁆ : M) -
      HAdd.hAdd (α := M) (β := M) ((f : (a : L) → M) ⁅x, x_2⁆ : M) ((f : (a : L) → M) ⁅x_1, x_2⁆ : M) =
    HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) x_2⁆ : M) (⁅x_2, (f : (a : L) → M) x⁆ : M))
        ((f : (a : L) → M) ⁅x, x_2⁆ : M) +
      HSub.hSub (β := M)
        (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) x_2⁆ : M) (⁅x_2, (f : (a : L) → M) x_1⁆ : M))
        ((f : (a : L) → M) ⁅x_1, x_2⁆ : M)

Tactic:
abel
-- 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
f : oneCochain R L M
x : R
x_1 : L
h :
  ∀ (x_2 : L),
    Eq.{u_3 + 1} (α := M)
      (({
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x • x_1, (f : (a : L) → M) y⁆ : M)
                    (⁅y, (f : (a : L) → M) (x • x_1)⁆ : M))
                  ((f : (a : L) → M) ⁅x • x_1, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : L) → M)
          x_2 :
        M)
      ((HSMul.hSMul (α := R) (β := L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x : R)
              {
                toFun := fun (y : L) ↦
                  HSub.hSub (β := M)
                    (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x_1⁆ : M))
                    ((f : (a : L) → M) ⁅x_1, y⁆ : M),
                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M } :
            (a : L) → M)
          x_2 :
        M)
⊢ {
      toFun := fun (y : L) ↦
        HSub.hSub (β := M)
          (HSub.hSub (α := M) (β := M) (⁅x • x_1, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) (x • x_1)⁆ : M))
          ((f : (a : L) → M) ⁅x • x_1, y⁆ : M),
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x : R)
      {
        toFun := fun (y : L) ↦
          HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x_1⁆ : M))
            ((f : (a : L) → M) ⁅x_1, y⁆ : M),
        map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M }

Tactic:
ext
-- 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
f : oneCochain R L M
x : R
x_1 x_2 : L
⊢ Eq.{u_3 + 1} (α := M)
    (({
            toFun := fun (y : L) ↦
              HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x • x_1, (f : (a : L) → M) y⁆ : M)
                  (⁅y, (f : (a : L) → M) (x • x_1)⁆ : M))
                ((f : (a : L) → M) ⁅x • x_1, y⁆ : M),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : L) → M)
        x_2 :
      M)
    ((HSMul.hSMul (α := R) (β := L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x : R)
            {
              toFun := fun (y : L) ↦
                HSub.hSub (β := M)
                  (HSub.hSub (α := M) (β := M) (⁅x_1, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x_1⁆ : M))
                  ((f : (a : L) → M) ⁅x_1, y⁆ : M),
              map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] M } :
          (a : L) → M)
        x_2 :
      M)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- 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
f : oneCochain R L M
x : L
⊢ Eq.{u_3 + 1} (α := M)
    (((({
                  toFun := fun (x : L) ↦
                    {
                      toFun := fun (y : L) ↦
                        HSub.hSub (β := M)
                          (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x⁆ : M))
                          ((f : (a : L) → M) ⁅x, y⁆ : M),
                      map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ } :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        x :
      M)
    (0 : M)

Tactic:
simp
-- 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
x_2 x_3 : L
⊢ 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:
abel
-- 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 : R
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)
    (((((↑(HSMul.hSMul (α := R) (β := ↥(twoCochain R L M)) ((RingHom.id R : (a : R) → R) x : R)
                      (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)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- 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
f : oneCochain R L M
x y : L
⊢ (((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) f : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
          L →ₗ[R] M) :
        (a : L) → M)
      y =
    HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) y⁆ : M) (⁅y, (f : (a : L) → M) x⁆ : M))
      ((f : (a : L) → M) ⁅x, y⁆ : M)

Tactic:
rfl

Premises used: rfl
-- 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
inst_7 : IsTrivial L M
f : oneCochain R L M
x y : L
⊢ Eq.{u_3 + 1} (α := M)
    ((((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) f : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (-(f : (a : L) → M) ⁅x, y⁆ : M)

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- 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 y x_1 x_2 : L
⊢ HAdd.hAdd (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M)
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) +
        HAdd.hAdd (α := M) (β := M) ((((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_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M) -
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M))
              (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
                (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
              (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M)

Tactic:
abel
-- 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 y : L
x_1 : R
x_2 : L
⊢ HAdd.hAdd (α := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) (x_1 • x_2)⁆ : M)
      (HSMul.hSMul (α := ℤ) (β := M) (-1)
          (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) (x_1 • x_2)⁆ : M) +
        HAdd.hAdd (α := M) (⁅x_1 • x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M)
          (HSMul.hSMul (α := ℤ) (β := M) (-1)
              ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) (x_1 • x_2) : M) +
            HAdd.hAdd (α := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1 • x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M)
              (HSMul.hSMul (α := ℤ) (β := M) (-1)
                ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_1 • x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M)))) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x_1 : R)
      (HAdd.hAdd (α := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
        (HSMul.hSMul (α := ℤ) (β := M) (-1) (⁅y, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) +
          HAdd.hAdd (α := M) (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y⁆ : M)
            (HSMul.hSMul (α := ℤ) (β := M) (-1)
                ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) +
              HAdd.hAdd (α := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) y : M)
                (HSMul.hSMul (α := ℤ) (β := M) (-1)
                  ((((a : (a : L) → L →ₗ[R] M) ⁅y, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x : M)))))

Tactic:
simp
-- 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 x_3 : L
⊢ HAdd.hAdd (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
                (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
                (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_1⁆ : M)
              (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
            ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) +
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) -
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M) =
    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) x_3⁆ : M)
                (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
              (⁅x_3, (((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) x_3 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M) +
      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) x_3⁆ : M)
                (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
              (⁅x_3, (((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) x_3 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M)

Tactic:
abel
-- 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 : L
x_1 : R
x_2 x_3 : L
⊢ Eq.{u_3 + 1} (α := M)
    (({
            toFun := fun (z : L) ↦
              HAdd.hAdd (α := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) (x_1 • x_2) : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                (HSMul.hSMul (α := ℤ) (β := M) (-1)
                    (⁅x_1 • x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M) +
                  HAdd.hAdd (α := M) (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) (x_1 • x_2)⁆ : M)
                    (HSMul.hSMul (α := ℤ) (β := M) (-1)
                        ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_1 • x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M) +
                      HAdd.hAdd (α := M)
                        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) (x_1 • x_2) : M)
                        (HSMul.hSMul (α := ℤ) (β := M) (-1)
                          ((((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)
    ((HSMul.hSMul (α := R) (β := L →ₗ[R] M) ((RingHom.id R : (a : R) → R) x_1 : R)
            {
              toFun := fun (z : L) ↦
                HAdd.hAdd (α := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) z⁆ : M)
                  (HSMul.hSMul (α := ℤ) (β := M) (-1)
                      (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) z⁆ : M) +
                    HAdd.hAdd (α := M) (⁅z, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
                      (HSMul.hSMul (α := ℤ) (β := M) (-1)
                          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) z : M) +
                        HAdd.hAdd (α := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
                          (HSMul.hSMul (α := ℤ) (β := M) (-1)
                            ((((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)

Tactic:
simp
-- 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 x_3 : L
⊢ HAdd.hAdd (α := M) (β := M) (⁅x, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
                (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
                (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M)
              (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
            ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) +
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
          ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) -
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M)
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M) =
    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) x_3⁆ : M)
                (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
              (⁅x_3, (((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) x_3 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x_1, (((a : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
                (⁅x_2, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
              (⁅x_3, (((a : (a : L) → L →ₗ[R] M) x_1 : L →ₗ[R] M) : (a : L) → M) x_2⁆ : M))
            ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_2⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x_1, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_1 : M)

Tactic:
abel