awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val val_1 : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (Sum.inr val_1) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val) (Sum.inr val_1)

Tactic:
simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
      Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
      Sum.elim_inl, if_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
      Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr, Sum.inl_injective.eq_iff,
      Sum.inr_injective.eq_iff, reduceCtorEq]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
j₃ : l
⊢ Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inl j₃))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
⊢ Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inr val))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
i₃ : l
⊢ Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inl i₃) PUnit.unit)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
⊢ Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inr val) PUnit.unit)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Lie.Classical
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
⊢ Invertible (PB l R)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Classical
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
apply : ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)
⊢ ↥(typeB l R) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)

Tactic:
apply (skewAdjointMatricesLieSubalgebraEquiv (JB l R) (PB l R) (by infer_instance)).trans

Premises used: skewAdjointMatricesLieSubalgebraEquiv, LieEquiv.trans, LieAlgebra.Orthogonal.PB, LieAlgebra.Orthogonal.JB
-- Module: Mathlib.Algebra.Lie.Classical
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
symm : ↥(so' (Unit ⊕ l) l R) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
⊢ ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R)) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)

Tactic:
symm
-- Module: Mathlib.Algebra.Lie.Classical
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
Unit :
  ↥(skewAdjointMatricesLieSubalgebra
        ((reindexAlgEquiv R R (Equiv.sumAssoc PUnit.{1} l l) :
            (a : Matrix ((_root_.Unit ⊕ l) ⊕ l) ((_root_.Unit ⊕ l) ⊕ l) R) →
              Matrix (PUnit.{1} ⊕ l ⊕ l) (PUnit.{1} ⊕ l ⊕ l) R)
          (indefiniteDiagonal (_root_.Unit ⊕ l) l R))) ≃ₗ⁅R⁆
    ↥(skewAdjointMatricesLieSubalgebra ((PB l R)ᵀ * JB l R * PB l R))
⊢ ↥(so' (_root_.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

Premises used: skewAdjointMatricesLieSubalgebraEquivTranspose, LieAlgebra.Orthogonal.indefiniteDiagonal, Sum, Unit, Matrix.reindexAlgEquiv, PUnit, LieEquiv.trans, Equiv.sumAssoc, Matrix.transpose_reindex
-- Module: Mathlib.Algebra.Lie.Classical
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
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))
⊢ ↥(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 LieEquiv.ofEq

Premises used: LieEquiv.ofEq
-- Module: Mathlib.Algebra.Lie.Classical
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
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))
⊢ (↑(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:
ext A
-- Module: Mathlib.Algebra.Lie.Classical
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
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
⊢ 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:
rw [jb_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    LieSubalgebra.mem_coe, mem_skewAdjointMatricesLieSubalgebra_unit_smul]

Premises used: LieAlgebra.Orthogonal.jb_transform, mem_skewAdjointMatricesLieSubalgebra_unit_smul, Units.smul_def, val_unitOfInvertible, LieSubalgebra.mem_coe, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Classical
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
⊢ 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:
simp [indefiniteDiagonal_assoc, S]

Premises used: LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, LieAlgebra.Orthogonal.S
-- 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
a b : L →ₗ[R] L →ₗ[R] M
ha :
  Membership.mem (γ := Set (L →ₗ[R] L →ₗ[R] M))
    {c : L →ₗ[R] L →ₗ[R] M |
      ∀ (x : L), Eq.{u_3 + 1} (α := M) ((((c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)}
    a
hb :
  Membership.mem (γ := Set (L →ₗ[R] L →ₗ[R] M))
    {c : L →ₗ[R] L →ₗ[R] M |
      ∀ (x : L), Eq.{u_3 + 1} (α := M) ((((c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)}
    b
x : L
⊢ Eq.{u_3 + 1} (α := M) ((((a + b : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)

Tactic:
simp [ha x, hb x]
-- 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
⊢ Membership.mem (γ := Set (L →ₗ[R] L →ₗ[R] M))
    {c : L →ₗ[R] L →ₗ[R] M |
      ∀ (x : L), Eq.{u_3 + 1} (α := M) ((((c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)}
    0

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
t : R
c : L →ₗ[R] L →ₗ[R] M
hc :
  Membership.mem (γ := Set (L →ₗ[R] L →ₗ[R] M))
    {c : L →ₗ[R] L →ₗ[R] M |
      ∀ (x : L), Eq.{u_3 + 1} (α := M) ((((c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)}
    c
x : L
⊢ Eq.{u_3 + 1} (α := M) ((((t • c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)

Tactic:
simp [hc x]
-- 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
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)
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)
⊢ x = 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
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_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:
congrFun (congrArg DFunLike.coe (congrFun h _)) _

Premises used: congrArg, congrFun, 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
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_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:
exact congrFun (congrArg DFunLike.coe (congrFun h _)) _

Premises used: congrArg, congrFun, 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
c : L →ₗ[R] L →ₗ[R] M
⊢ Membership.mem (γ := Submodule R (L →ₗ[R] L →ₗ[R] M)) (twoCochain R L M) c ↔
    ∀ (x : L), Eq.{u_3 + 1} (α := M) ((((c : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
a : ↥(twoCochain R L M)
x : L
⊢ Eq.{u_3 + 1} (α := M) ((((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) x : M) (0 : M)

Tactic:
a.2 x

Premises used: Subtype.property
-- 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
a : ↥(twoCochain R L M)
x y : L
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
⊢ 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)

Tactic:
rw [neg_eq_iff_add_eq_zero, add_comm]

Premises used: neg_eq_iff_add_eq_zero, add_comm
-- 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
a : ↥(twoCochain R L M)
x y : L
⊢ 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:
simpa [map_add, twoCochain_alt a x, twoCochain_alt a y] using twoCochain_alt a (x + y)

Premises used: LieModule.Cohomology.twoCochain_alt, map_add, HAdd.hAdd
-- 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
a : ↥(twoCochain R L M)
x : L
⊢ Eq (α := L →ₗ[R] M) (((↑a : L →ₗ[R] L →ₗ[R] M) : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M)
    ((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] 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
a b : ↥(twoCochain R L M)
x y : L
⊢ (((a + b : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y =
    HAdd.hAdd (α := M) (β := M) ((((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y : M)
      ((((b : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y : M)

Tactic:
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
r : R
a : ↥(twoCochain R L M)
x y : L
⊢ (((r • a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y =
    HSMul.hSMul (β := M) r ((((a : (a : L) → L →ₗ[R] M) x : L →ₗ[R] M) : (a : L) → M) y : M)

Tactic:
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
f : oneCochain R L M
x x_1 x_2 : L
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)
⊢ 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)

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_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:
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 : L
x_1 : R
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) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x_1 : R)
      (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 [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 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)
      ((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)
⊢ {
      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 }

Tactic:
ext