awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(typeB l R) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)
have apply : ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)
Tactic: apply (skewAdjointMatricesLieSubalgebraEquiv (JB l R) (PB l R) (by infer_instance)).trans
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)
have symm : ↥(so' (Unit ⊕ l) l R) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(so' (Unit ⊕ l) l R) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
have Unit : ↥(skewAdjointMatricesLieSubalgebra
      ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
          (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
        (indefiniteDiagonal (Unit ⊕ l) l R))) ≃ₗ⁅R⁆
  ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
Tactic: apply
    (skewAdjointMatricesLieSubalgebraEquivTranspose (indefiniteDiagonal (Sum Unit l) l R)
        (Matrix.reindexAlgEquiv _ _ (Equiv.sumAssoc PUnit l l))
        (Matrix.transpose_reindex _ _)).trans
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
            (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
          (indefiniteDiagonal (Unit ⊕ l) l R))) ≃ₗ⁅R⁆
    ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
have h : (↑(skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
            (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
          (indefiniteDiagonal (Unit ⊕ l) l R))) :
    Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)) =
  (↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) :
    Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R))
Tactic: apply LieEquiv.ofEq
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ (↑(skewAdjointMatricesLieSubalgebra
          ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
              (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
            (indefiniteDiagonal (Unit ⊕ l) l R))) :
      Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)) =
    (↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) :
      Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R))
have h : ∀ (A : Matrix.{u_4, u_4, u₂} (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R),
  A ∈
      (↑(skewAdjointMatricesLieSubalgebra
            ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
                (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
              (indefiniteDiagonal (Unit ⊕ l) l R))) :
        Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)) ↔
    A ∈
      (↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) :
        Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R))
Tactic: ext A
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
A : Matrix.{u_4, u_4, u₂} (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R
⊢ A ∈
      (↑(skewAdjointMatricesLieSubalgebra
            ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
                (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
              (indefiniteDiagonal (Unit ⊕ l) l R))) :
        Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)) ↔
    A ∈
      (↑(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) :
        Set (Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R))
have h : Membership.mem (γ := LieSubalgebra R (Matrix.{u_4, u_4, u₂} (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R))
    (skewAdjointMatricesLieSubalgebra
      ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
          (a : Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) → Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
        (indefiniteDiagonal (Unit ⊕ l) l R)))
    A ↔
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_4, u_4, u₂} (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R))
    (skewAdjointMatricesLieSubalgebra (fromBlocks 1 0 0 (S l R))) A
Tactic: rw [jb_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    LieSubalgebra.mem_coe, mem_skewAdjointMatricesLieSubalgebra_unit_smul]
-- 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
x x_1 : ↥(twoCochain R L M)
h :
  Eq (α := (a : L) → L →ₗ[R] M)
    ((fun (a : ↥(twoCochain R L M)) (x : L) ↦ (((↑a : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M)) x)
    ((fun (a : ↥(twoCochain R L M)) (x : L) ↦ (((↑a : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M)) x_1)
⊢ x = x_1
have a : ∀ (x_2 x_3 : L),
  Eq.{u_3 + 1} (α := M) (((((↑x : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3 : M)
    (((((↑x_1 : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x_2 : L →ₗ[R] M) : (a : L) → M) x_3 : M)
Tactic: ext
-- 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
a : ↥(twoCochain R L M)
x y : L
⊢ Eq.{u_3 + 1} (α := M) (-(((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y : M)
    ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x : M)
have rw : HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) y : L →ₗ[R] M) : (a : L) → M) x : M)
    ((((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y : M) =
  0
Tactic: rw [neg_eq_iff_add_eq_zero, add_comm]
-- 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
f : oneCochain R L M
x x_1 x_2 : L
⊢ HSub.hSub (β := M)
      (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) (x_1 + x_2)⁆ : M) (⁅x_1 + x_2, (f : (a : L) → M) x⁆ : M))
      ((f : (a : L) → M) ⁅x, x_1 + x_2⁆ : M) =
    HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) x_1⁆ : M) (⁅x_1, (f : (a : L) → M) x⁆ : M))
        ((f : (a : L) → M) ⁅x, x_1⁆ : 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)
have simp : HAdd.hAdd (α := M) (β := M) (⁅x, (f : (a : L) → M) x_1⁆ : M) (⁅x, (f : (a : L) → M) x_2⁆ : M) -
      HAdd.hAdd (α := M) (β := M) (⁅x_1, (f : (a : L) → M) x⁆ : M) (⁅x_2, (f : (a : L) → M) x⁆ : M) -
    HAdd.hAdd (α := M) (β := M) ((f : (a : L) → M) ⁅x, x_1⁆ : M) ((f : (a : L) → M) ⁅x, x_2⁆ : M) =
  HSub.hSub (β := M) (HSub.hSub (α := M) (β := M) (⁅x, (f : (a : L) → M) x_1⁆ : M) (⁅x_1, (f : (a : L) → M) x⁆ : M))
      ((f : (a : L) → M) ⁅x, x_1⁆ : 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)
Tactic: simp
-- 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
f : oneCochain R L M
x x_1 : L
⊢ {
      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' := ⋯ } =
    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 }
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : L →ₗ[R] M } :
          (a : L) → M)
        x_2 :
      M)
Tactic: ext
-- 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
f : oneCochain R L M
x 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)
    ((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)
have 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)
Tactic: simp
-- 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
f : oneCochain R L M
x : R
x_1 : L
⊢ {
      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 }
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : L →ₗ[R] M } :
          (a : L) → M)
        x_2 :
      M)
Tactic: ext
-- 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 : ↥(twoCochain R L M)
⊢ d₂₃_aux R L M (x + x_1) = d₂₃_aux R L M x + d₂₃_aux R L M x_1
have 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)
Tactic: ext
-- 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 : R
x_1 : ↥(twoCochain R L 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)
have 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)
Tactic: ext
-- 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 : R
x_1 : ↥(twoCochain R L M)
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)
have 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)
Tactic: simp [d₂₃_aux]
-- 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
⊢ Eq (α := oneCochain R L M →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M) (d₂₃ R L M ∘ₗ d₁₂ R L M) 0
have 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)
Tactic: ext a 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
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)
have 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)
Tactic: have (a : oneCochain R L M) (x : L) : d₁₂ R L M a x = (d₁₂ R L M a).val x := rfl