awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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)
have 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
Tactic: simp only [LinearMap.comp_apply, d₂₃_apply, LinearMap.zero_apply, this,
    d₁₂_apply_coe_apply_apply R L M, lie_sub, lie_lie]
-- 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
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)
have 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)
Tactic: rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- 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
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)
⊢ (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)
have 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)
Tactic: rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- 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
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)
⊢ (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)
have 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)
Tactic: rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- 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
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)
⊢ (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)
have 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)
Tactic: rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- 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
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)
⊢ (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)
have 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)
Tactic: rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (hypothesis)
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)
⊢ 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)
                  (HAdd.hAdd (α := M) (β := M) (⁅⁅y, x⁆, (a : (a : L) → M) z⁆ : M) (⁅x, ⁅y, (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)
              (HAdd.hAdd (α := M) (β := M) (⁅⁅z, x⁆, (a : (a : L) → M) y⁆ : M) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M) -
                HAdd.hAdd (α := M) (β := M) (⁅⁅z, y⁆, (a : (a : L) → M) x⁆ : M) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M))
              (⁅z, (a : (a : L) → M) ⁅x, y⁆⁆ : M) -
          HSub.hSub (β := M)
            (HSub.hSub (β := M)
              (HSub.hSub (α := M) (⁅x, ⁅y, (a : (a : L) → M) z⁆⁆ : M)
                (HAdd.hAdd (α := M) (β := M) (⁅⁅y, x⁆, (a : (a : L) → M) z⁆ : M) (⁅x, ⁅y, (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) (⁅x, ⁅z, (a : (a : L) → M) y⁆⁆ : M)
              (HAdd.hAdd (α := M) (β := M) (⁅⁅z, x⁆, (a : (a : L) → M) y⁆ : M) (⁅x, ⁅z, (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) (⁅y, ⁅z, (a : (a : L) → M) x⁆⁆ : M)
            (HAdd.hAdd (α := M) (β := M) (⁅⁅z, y⁆, (a : (a : L) → M) x⁆ : M) (⁅y, ⁅z, (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
have 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)
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]
-- 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
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a ↔
    ∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have mp : Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a →
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
Tactic: constructor
-- 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
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
mp :
  Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a →
    ∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a ↔
    ∀ (x y z : L),
      (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
        HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
          ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have mpr : (∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)) →
  Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a
Tactic: constructor
-- 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
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h : Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a
x y z : L
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have mp : ∀
  (h :
    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))
  (x y z : L),
  (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
Tactic: rw [mem_twoCocycle_iff] at h
Cleared hypotheses: h, x, y, z
-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (hypothesis)
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
a : ↥(twoCochain R L M)
h :
  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)
x y z : L
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have this : Eq.{u_3 + 1} (α := 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) :
                    (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 : M)
Tactic: have : (d₂₃ R L M) a x y z = 0 := (congrArg (fun b ↦ b x y z = 0) h).mpr rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (hypothesis)
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
a : ↥(twoCochain R L M)
h :
  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)
x y z : L
this :
  Eq.{u_3 + 1} (α := 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) :
                      (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 : M)
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have this₁ : HSub.hSub (β := M)
    (HAdd.hAdd (α := M) (β := 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) =
  0
Tactic: simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Cochain (hypothesis)
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
a : ↥(twoCochain R L M)
h :
  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)
x y z : L
this :
  HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := 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) =
    0
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have this₁ : HAdd.hAdd (α := M) (β := 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
Tactic: rw [sub_eq_zero] at this
Cleared hypotheses: this
-- 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
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  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)
x y z : L
this :
  HAdd.hAdd (α := M) (β := 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
⊢ (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
      ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
have mp : -HAdd.hAdd (α := M) (β := 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) =
  HAdd.hAdd (α := M) (β := 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)
Tactic: rw [← twoCochain_skew a _ x, ← twoCochain_skew a _ y, ← this]
-- 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
inst_7 : IsTrivial L M
a : ↥(twoCochain R L M)
h :
  ∀ (x y z : L),
    (((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) ⁅y, z⁆ =
      HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) ⁅x, y⁆ : L →ₗ[R] M) : (a : L) → M) z : M)
        ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) ⁅x, z⁆ : M)
⊢ Membership.mem (γ := Submodule R ↥(twoCochain R L M)) (twoCocycle R L M) a
have mpr : ∀ (x y z : L),
  Eq.{u_3 + 1} (α := 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) :
                      (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 : 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: ext x y z