awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  Membership.mem (γ := Set (L ⊗[R] M))
    {t : L ⊗[R] M |
      ∃ (m : ↥I) (n : ↥N),
        ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
    (x ⊗ₜ[R] n)
⊢ Membership.mem (γ := Set (L ⊗[R] M))
      {t : L ⊗[R] M |
        ∃ (m : ↥I) (n : ↥N),
          ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
      (x ⊗ₜ[R] n) ∧
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
      ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆
have h₁ : ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M) (x ⊗ₜ[R] n) =
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ Membership.mem (γ := Set (L ⊗[R] M))
    {t : L ⊗[R] M |
      ∃ (m : ↥I) (n : ↥N),
        ((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) m ⊗ₜ[R] ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) n = t}
    (x ⊗ₜ[R] n)
have h : Eq (α := L ⊗[R] M)
  (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
      ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
    L ⊗[R] M)
  (x ⊗ₜ[R] n : L ⊗[R] M)
Tactic: use ⟨x, hx⟩, ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M) =
    m
⊢ ∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m
have e_s : ∃ (x_1 : ↥I) (n_1 : ↥N),
  ⁅(↑x_1 : L), (↑n_1 : M)⁆ =
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M) =
    m
⊢ ∃ (x_1 : ↥I) (n_1 : ↥N),
    ⁅(↑x_1 : L), (↑n_1 : M)⁆ =
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
        (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
            ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
          L ⊗[R] M)
have h₁ : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆ =
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
    (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
        ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
      L ⊗[R] M)
Tactic: use ⟨x, hx⟩, ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆ : R)
have calc_1 : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
        ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
    R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (β := End R M)
        (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
          HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) :
    R)
Tactic: calc traceForm R L M ⁅x, y⁆ z
      = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
    _ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
    _ = traceForm R L M x ⁅y, z⁆ := ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
calc_1 :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (β := End R M)
          (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
            HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆ : R)
have calc_2 : (trace R M : (a : M →ₗ[R] M) → R)
    (HMul.hMul (β := End R M)
      (HMul.hMul (α := End R M) (β := End R M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
        HMul.hMul (α := End R M) (β := End R M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
      (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) =
  HSub.hSub (α := R) (β := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
          (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
          (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
      R)
Tactic: calc traceForm R L M ⁅x, y⁆ z
      = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
    _ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
    _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
    _ = traceForm R L M x ⁅y, z⁆ := ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
have rw : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [← lie_skew x y, map_neg, LinearMap.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [← lie_skew x y, map_neg, LinearMap.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [← lie_skew x y, map_neg, LinearMap.neg_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
have rw : Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
Tactic: rw [traceForm_apply_lie_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
have rw : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
Tactic: rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
Tactic: rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
Tactic: rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
have rw₃ : Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
  (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
Tactic: rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
⊢ Eq (α := LinearMap.BilinForm R L) ⁅x, traceForm R L M⁆ 0
have H : ∀ (y z : L),
  Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: ext y z
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H : Eq.{u_1 + 1} (α := R)
  ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
          ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
        (a : L) → R)
      z :
    R)
  ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₁ : HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
H₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₂ : HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
H₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₂ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₃ : HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  (0 : (a : L) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]