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

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 : ↥(twoCochain R L M)
h :
  ∀ (x_2 x_3 x_4 : L),
    Eq.{u_3 + 1} (α := M)
      ((((((d₂₃_aux R L M (x + x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_3 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_4 :
        M)
      ((((((d₂₃_aux R L M x + d₂₃_aux R L M x_1 : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                x_3 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_4 :
        M)
⊢ d₂₃_aux R L M (x + x_1) = d₂₃_aux R L M x + d₂₃_aux R L M x_1

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
x x_1 : ↥(twoCochain R L M)
x_2 x_3 x_4 : L
⊢ HAdd.hAdd (α := M) (β := M) (⁅x_2, (((x : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) -
              HAdd.hAdd (α := M) (β := M) (⁅x_3, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) +
            HAdd.hAdd (α := M) (β := M) (⁅x_4, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
              (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
          HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M)
            ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M) +
        HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
          ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) -
      HAdd.hAdd (α := M) (β := M) ((((x : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
        ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) =
    HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x_2, (((x : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M))
              (⁅x_4, (((x : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M))
          ((((x : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((x : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) +
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M)
                (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M))
              (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M))
          ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) 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
x : R
x_1 : ↥(twoCochain R L M)
h :
  ∀ (x_2 x_3 x_4 : L),
    Eq.{u_3 + 1} (α := M)
      ((((((d₂₃_aux R L M (x • x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_3 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_4 :
        M)
      ((((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (d₂₃_aux R L M x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M)
                      x_2 :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                x_3 :
              L →ₗ[R] M) :
            (a : L) → M)
          x_4 :
        M)
⊢ d₂₃_aux R L M (x • x_1) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (d₂₃_aux R L M x_1)

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
x : R
x_1 : ↥(twoCochain R L M)
x_2 x_3 x_4 : L
h :
  HSMul.hSMul (β := M) x (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) -
              HSMul.hSMul (β := M) x (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) +
            HSMul.hSMul (β := M) x (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) -
          HSMul.hSMul (β := M) x ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M) +
        HSMul.hSMul (β := M) x ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) -
      HSMul.hSMul (β := M) x ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M) =
    x •
      HSub.hSub (β := M)
        (HAdd.hAdd (β := M)
          (HSub.hSub (β := M)
            (HAdd.hAdd (β := M)
              (HSub.hSub (α := M) (β := M)
                (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
                (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M))
              (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M))
            ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M))
          ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M))
        ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)
⊢ Eq.{u_3 + 1} (α := M)
    ((((((d₂₃_aux R L M (x • x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M) x_2 : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_3 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_4 :
      M)
    ((((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (d₂₃_aux R L M x_1) : (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x_2 :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x_3 :
            L →ₗ[R] M) :
          (a : L) → M)
        x_4 :
      M)

Tactic:
simp [d₂₃_aux]

Premises used: _private.0.LieModule.Cohomology.d₂₃_aux
-- 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 : ↥(twoCochain R L M)
x_2 x_3 x_4 : L
⊢ HSMul.hSMul (β := M) x (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) +
      (HSMul.hSMul (α := ℤ) (-1)
          (HSMul.hSMul (β := M) x (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)) +
        (HSMul.hSMul (β := M) x (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M) +
          (HSMul.hSMul (α := ℤ) (-1)
              (HSMul.hSMul (β := M) x ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M)) +
            (HSMul.hSMul (β := M) x ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M) +
              HSMul.hSMul (α := ℤ) (-1)
                (HSMul.hSMul (β := M) x
                  ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_2 : M)))))) =
    x •
      HAdd.hAdd (α := M) (⁅x_2, (((x_1 : (a : L) → L →ₗ[R] M) x_3 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M)
        (HSMul.hSMul (α := ℤ) (β := M) (-1)
            (⁅x_3, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_4⁆ : M) +
          HAdd.hAdd (α := M) (⁅x_4, (((x_1 : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3⁆ : M)
            (HSMul.hSMul (α := ℤ) (β := M) (-1)
                ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_3⁆ : L →ₗ[R] M) : (a : L) → M) x_4 : M) +
              HAdd.hAdd (α := M) ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_2, x_4⁆ : L →ₗ[R] M) : (a : L) → M) x_3 : M)
                (HSMul.hSMul (α := ℤ) (β := M) (-1)
                  ((((x_1 : (a : L) → L →ₗ[R] M) ⁅x_3, x_4⁆ : 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
a : ↥(twoCochain R L M)
x y z : L
⊢ (((((((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                    (a : L) → L →ₗ[R] L →ₗ[R] M)
                  x :
                L →ₗ[R] L →ₗ[R] M) :
              (a : L) → L →ₗ[R] M)
            y :
          L →ₗ[R] M) :
        (a : L) → M)
      z =
    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) z⁆ : M)
              (⁅y, (((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) y⁆ : M))
          ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M))
        ((((a : (a : L) → L →ₗ[R] M) ⁅x, z⁆ : L →ₗ[R] M) : (a : L) → M) y : M))
      ((((a : (a : L) → L →ₗ[R] M) ⁅y, z⁆ : L →ₗ[R] M) : (a : L) → M) x : 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
h :
  ∀ (a : oneCochain R L M) (x y z : L),
    Eq.{u_3 + 1} (α := M)
      ((((((((d₂₃ R L M ∘ₗ d₁₂ R L M : (a : oneCochain R L M) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a :
                          L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                        (a : L) → L →ₗ[R] L →ₗ[R] M)
                      x :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                y :
              L →ₗ[R] M) :
            (a : L) → M)
          z :
        M)
      ((((((((0 : (a : oneCochain R L M) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                        (a : L) → L →ₗ[R] L →ₗ[R] M)
                      x :
                    L →ₗ[R] L →ₗ[R] M) :
                  (a : L) → L →ₗ[R] M)
                y :
              L →ₗ[R] M) :
            (a : L) → M)
          z :
        M)
⊢ Eq (α := oneCochain R L M →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M) (d₂₃ R L M ∘ₗ d₁₂ R L M) 0

Tactic:
ext a x y z
-- 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 : oneCochain R L M
x y z : L
⊢ ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)

Tactic:
have (a : oneCochain R L M) (x : L) : d₁₂ R L M a x = (d₁₂ R L M a).val x := 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
a : oneCochain R L M
x y z : L
this :
  ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
h :
  HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M))
                (⁅x, (a : (a : L) → M) ⁅y, z⁆⁆ : M) -
              HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
                (⁅y, (a : (a : L) → M) ⁅x, z⁆⁆ : M) +
            HSub.hSub (β := M)
              (HSub.hSub (α := M) (β := M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
              (⁅z, (a : (a : L) → M) ⁅x, y⁆⁆ : M) -
          HSub.hSub (β := M)
            (HSub.hSub (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M))
              (⁅z, (a : (a : L) → M) ⁅x, y⁆⁆ : M))
            ((a : (a : L) → M) (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆) : M) +
        HSub.hSub (β := M)
          (HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M))
            (⁅y, (a : (a : L) → M) ⁅x, z⁆⁆ : M))
          ((a : (a : L) → M) (⁅x, ⁅z, y⁆⁆ - ⁅z, ⁅x, y⁆⁆) : M) -
      HSub.hSub (β := M)
        (HSub.hSub (β := M)
          (HSub.hSub (α := M) (β := M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
          (⁅x, (a : (a : L) → M) ⁅y, z⁆⁆ : M))
        ((a : (a : L) → M) (⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) : M) =
    0
⊢ Eq.{u_3 + 1} (α := M)
    ((((((((d₂₃ R L M ∘ₗ d₁₂ R L M : (a : oneCochain R L M) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a :
                        L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)
    ((((((((0 : (a : oneCochain R L M) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M) :
                      (a : L) → L →ₗ[R] L →ₗ[R] M)
                    x :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              y :
            L →ₗ[R] M) :
          (a : L) → M)
        z :
      M)

Tactic:
simp only [LinearMap.comp_apply, d₂₃_apply, LinearMap.zero_apply, this,
    d₁₂_apply_coe_apply_apply R L M, lie_sub, lie_lie]

Premises used: LinearMap.zero_apply, LieModule.Cohomology.d₂₃_apply, LinearMap.comp_apply, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, lie_sub, lie_lie
-- 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 : oneCochain R L M
x y z : L
this :
  ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
rw :
  (a : (a : L) → M) (⁅⁅y, z⁆, x⁆ + ⁅z, ⁅y, x⁆⁆) =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
rw₁ :
  (a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆ + ⁅z, ⁅y, x⁆⁆) =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
rw₂ :
  (a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆ + ⁅z, ⁅y, x⁆⁆) =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, -⁅y, z⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
rw₃ :
  (a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆ + ⁅z, ⁅y, x⁆⁆) =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆) : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
rw₄ rw₅ :
  HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆) : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M) =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) (-⁅x, ⁅y, z⁆⁆) : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
⊢ (a : (a : L) → M) ⁅y, ⁅z, x⁆⁆ =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)

Tactic:
rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]

Premises used: leibniz_lie, lie_neg, map_add, lie_skew, congr_arg, DFunLike.coe
-- 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 : oneCochain R L M
x y z : L
this :
  ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
⊢ (a : (a : L) → M) ⁅y, ⁅z, x⁆⁆ =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)

Tactic:
have : a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆ := by
    rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- 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 : oneCochain R L M
x y z : L
this_1 :
  ∀ (a : oneCochain R L M) (x : L),
    Eq (α := L →ₗ[R] M)
      ((((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a : ↥(twoCochain R L M)) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
      (((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) a) : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x :
        L →ₗ[R] M)
this :
  (a : (a : L) → M) ⁅y, ⁅z, x⁆⁆ =
    HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)
⊢ HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M))
                (-⁅x, (a : (a : L) → M) ⁅z, y⁆⁆ : M) -
              HSub.hSub (β := M)
                (HSub.hSub (α := M) (β := M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
                (-⁅y, (a : (a : L) → M) ⁅z, x⁆⁆ : M) +
            HSub.hSub (β := M)
              (HSub.hSub (α := M) (β := M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
              (-⁅z, (a : (a : L) → M) ⁅y, x⁆⁆ : M) -
          (HSub.hSub (β := M)
              (HSub.hSub (α := M) (β := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M) (⁅y, ⁅x, (a : (a : L) → M) z⁆⁆ : M))
              (-⁅z, (a : (a : L) → M) ⁅y, x⁆⁆ : M) -
            HSub.hSub (α := M) (-(a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M)
              (-HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M))) +
        (HSub.hSub (β := M)
            (HSub.hSub (α := M) (β := M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M) (⁅z, ⁅x, (a : (a : L) → M) y⁆⁆ : M))
            (-⁅y, (a : (a : L) → M) ⁅z, x⁆⁆ : M) -
          HSub.hSub (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) (-(a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)) -
      (HSub.hSub (β := M)
          (HSub.hSub (α := M) (β := M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M) (⁅z, ⁅y, (a : (a : L) → M) x⁆⁆ : M))
          (-⁅x, (a : (a : L) → M) ⁅z, y⁆⁆ : M) -
        HSub.hSub (β := M)
          (HAdd.hAdd (α := M) (β := M) ((a : (a : L) → M) ⁅x, ⁅z, y⁆⁆ : M) ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M))
          ((a : (a : L) → M) ⁅z, ⁅y, x⁆⁆ : M)) =
    0

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)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a ↔
    Eq (α := L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
      ((d₂₃ R L M : (a : ↥(twoCochain R L M)) → L →ₗ[R] L →ₗ[R] L →ₗ[R] M) a : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)
      (0 : L →ₗ[R] L →ₗ[R] L →ₗ[R] M)

Tactic:
simp [twoCocycle]

Premises used: LieModule.Cohomology.twoCocycle