awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TraceForm
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
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
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
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) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R) =
    0
H₆ H₇ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 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:
rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]

Premises used: LinearMap.zero_apply, sub_self, LieHom.lie_apply, Module.Dual.lie_apply, LinearMap.sub_apply, LieModule.traceForm_apply_lie_apply'
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : IsReduced R
inst_8 : IsNilpotent L M
H :
  ∀ (x y : L),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
      ((((0 : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
⊢ Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0

Tactic:
ext x y
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : IsReduced R
inst_8 : IsNilpotent L M
x y : L
H :
  _root_.IsNilpotent.{u_1} (R := 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 ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
    ((((0 : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)

Tactic:
simp only [traceForm_apply_apply, LinearMap.zero_apply, ← isNilpotent_iff_eq_zero]

Premises used: LinearMap.zero_apply, isNilpotent_iff_eq_zero, LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : IsReduced R
inst_8 : IsNilpotent L M
x y : L
H :
  _root_.IsNilpotent.{u_4} (R := M →ₗ[R] M)
    (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
      ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
⊢ _root_.IsNilpotent.{u_1} (R := 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 ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)

Tactic:
apply LinearMap.isNilpotent_trace_of_isNilpotent

Premises used: LinearMap.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : IsReduced R
inst_8 : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent.{u_4} (R := M →ₗ[R] M)
    (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
      ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)

Tactic:
isNilpotent_toEnd_of_isNilpotent₂ R L M x y

Premises used: LieModule.isNilpotent_toEnd_of_isNilpotent₂
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : IsReduced R
inst_8 : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent.{u_4} (R := M →ₗ[R] M)
    (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
      ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)

Tactic:
exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y

Premises used: LieModule.isNilpotent_toEnd_of_isNilpotent₂
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : Module.Finite R M
A : Type u_5
inst_9 : CommRing A
inst_10 : Algebra R A
a :
  ∀ (x x_1 : L),
    Eq.{u_5 + 1} (α := A)
      ((((TensorProduct.AlgebraTensorModule.curry
                    ((((TensorProduct.AlgebraTensorModule.curry (traceForm A (A ⊗[R] L) (A ⊗[R] M)) :
                              A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                            (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                          1 :
                        (a : L) → A ⊗[R] L →ₗ[A] A)
                      x) :
                  A →ₗ[A] L →ₗ[R] A) :
                (a : A) → L →ₗ[R] A)
              1 :
            (a : L) → A)
          x_1 :
        A)
      ((((TensorProduct.AlgebraTensorModule.curry
                    ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.baseChange A (traceForm R L M)) :
                              A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                            (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                          1 :
                        (a : L) → A ⊗[R] L →ₗ[A] A)
                      x) :
                  A →ₗ[A] L →ₗ[R] A) :
                (a : A) → L →ₗ[R] A)
              1 :
            (a : L) → A)
          x_1 :
        A)
⊢ Eq (α := LinearMap.BilinForm A (A ⊗[R] L)) (traceForm A (A ⊗[R] L) (A ⊗[R] M))
    (LinearMap.BilinForm.baseChange A (traceForm R L M))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : Module.Finite R M
A : Type u_5
inst_9 : CommRing A
inst_10 : Algebra R A
x x_1 : L
⊢ Eq.{u_5 + 1} (α := A)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry (traceForm A (A ⊗[R] L) (A ⊗[R] M)) :
                            A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                          (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                        1 :
                      (a : L) → A ⊗[R] L →ₗ[A] A)
                    x) :
                A →ₗ[A] L →ₗ[R] A) :
              (a : A) → L →ₗ[R] A)
            1 :
          (a : L) → A)
        x_1 :
      A)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.baseChange A (traceForm R L M)) :
                            A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                          (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                        1 :
                      (a : L) → A ⊗[R] L →ₗ[A] A)
                    x) :
                A →ₗ[A] L →ₗ[R] A) :
              (a : A) → L →ₗ[R] A)
            1 :
          (a : L) → A)
        x_1 :
      A)

Tactic:
simp [traceForm_apply_apply, ← LinearMap.baseChange_comp, Algebra.algebraMap_eq_smul_one]

Premises used: LinearMap.baseChange_comp, Algebra.algebraMap_eq_smul_one, LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
rw :
  Membership.mem (γ := Submodule R L)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1))) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x

Tactic:
rw [← LieAlgebra.coe_derivedSeries_one_eq]

Premises used: LieAlgebra.coe_derivedSeries_one_eq
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
⊢ Membership.mem (γ := Submodule R L)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1))) x

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
⊢ Membership.mem (γ := Submodule R L)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1))) x

Tactic:
exact hx
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x

Tactic:
replace hx : x ∈ Submodule.span R {⁅u, v⁆ | (u : L) (v : L)} := by
    rw [← LieAlgebra.coe_derivedSeries_one_eq]; exact hx
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x u : L
hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u
mem :
  ∀ (a b : L),
    Eq.{u_1 + 1} (α := 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) ⁅a, b⁆ : End R M)
            y) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := 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) u : End R M) y) :
      R)
    (0 : R)

Tactic:
obtain ⟨a, b, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b : L
mem :
  ∀ (c : L)
    (hbc :
      Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
        (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)),
    Eq.{u_1 + 1} (α := 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) ⁅a, b⁆ : End R M)
            y) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := 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) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)

Tactic:
obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
    (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)
rw :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆
rw₁ :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆
rw₂ rw₃ :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y
⊢ Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c

Tactic:
rw [hbc, Module.End.instLieRingModule_eq, lie_skew]

Premises used: lie_skew, Module.End.instLieRingModule_eq
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
    (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)
⊢ Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c

Tactic:
replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
⊢ 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) 0 * y) : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x u v : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) u
hy_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) v
hu :
  Eq.{u_1 + 1} (α := 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) u : End R M) y) :
      R)
    (0 : R)
hv :
  Eq.{u_1 + 1} (α := 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) v : End R M) y) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := 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) (u + v) : End R M)
          y) :
      R)
    (0 : R)

Tactic:
simp [add_mul, hu, hv]

Premises used: add_mul
-- Module: Mathlib.Algebra.Lie.TraceForm
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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
t : R
u : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) u
hu :
  Eq.{u_1 + 1} (α := 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) u : End R M) y) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := 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) (t • u) : End R M)
          y) :
      R)
    (0 : R)

Tactic:
simp [hu]
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
set :
  let d := finrank.{u_1, u_4} R ↥(genWeightSpace M χ);
  (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    d • (χ x * χ y)
⊢ (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    finrank.{u_1, u_4} R ↥(genWeightSpace M χ) • (χ x * χ y)

Tactic:
set d := finrank R (genWeightSpace M χ)

Premises used: Membership.mem, Subtype, LieModule.genWeightSpace, Module.finrank
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
⊢ χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0

Tactic:
simp [mul_comm (χ x)]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
⊢ χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0

Tactic:
have h₁ : χ y • d • χ x - χ y • χ x • (d : R) = 0 := by simp [mul_comm (χ x)]
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
⊢ χ x • d • χ y = d • (χ x * χ y)

Tactic:
simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)

Premises used: mul_left_comm, Nat.cast, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.Algebra.Lie.TraceForm
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
⊢ χ x • d • χ y = d • (χ x * χ y)

Tactic:
have h₂ : χ x • d • χ y = d • (χ x * χ y) := by
    simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)