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
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
h₂ : χ x • d • χ y = d • (χ x * χ y)
⊢ Eq (α := LinearMap.BilinForm R L) (traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ)) 0

Tactic:
have := traceForm_eq_zero_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)
-- 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
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : Eq (α := LinearMap.BilinForm R L) (traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ)) 0
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace 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:
replace this := LinearMap.congr_fun (LinearMap.congr_fun this 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
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y
⊢ y = 0

Tactic:
simpa using hy
-- 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 : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y
⊢ y = 0

Tactic:
replace hy : y = 0 := by simpa using hy
-- 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 : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x
hy : y = 0
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
simp [hy]
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs (k + 1) ⊥) y
⊢ ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆

Tactic:
rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy

Premises used: LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
⊢ Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x

Tactic:
simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieIdeal.lcs_succ, LieSubmodule.mem_top, true_and
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx

Premises used: Submodule.span_induction
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
succ :
  ∀ (x : L)
    (h :
      Membership.mem (γ := Set L)
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x}
        x),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
succ₁ : Eq.{u_1 + 1} (α := R) (((traceForm R L M : (a : L) → L →ₗ[R] R) 0 : (a : L) → R) y : R) (0 : R)
succ₂ :
  ∀ (z w : L),
    Membership.mem (γ := Submodule R L)
        (Submodule.span R
          {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
        z →
      Membership.mem (γ := Submodule R L)
          (Submodule.span R
            {x : L |
              ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
          w →
        ∀
          (hz :
            Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R)
              (0 : R))
          (hw :
            Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) y : R)
              (0 : R)),
          Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (z + w) : L →ₗ[R] R) : (a : L) → R) y : R)
            (0 : R)
succ₃ :
  ∀ (t : R) (z : L),
    Membership.mem (γ := Submodule R L)
        (Submodule.span R
          {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
        z →
      ∀
        (hz :
          Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R)
            (0 : R)),
        Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (t • z) : L →ₗ[R] R) : (a : L) → R) y : R)
          (0 : 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 : R)

Tactic:
refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
z w : L
hw : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) w
succ :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) ⁅z, y⁆ : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅z, w⁆ : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]

Premises used: LinearMap.neg_apply, neg_eq_zero, map_neg, lie_skew, 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
z w : L
hw : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) w
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) ⁅z, y⁆ : R) (0 : R)

Tactic:
ih hw (hy _)
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
z w : L
hw : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) w
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) ⁅z, y⁆ : R) (0 : R)

Tactic:
exact ih hw (hy _)
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
⊢ Eq.{u_1 + 1} (α := R) (((traceForm R L M : (a : L) → L →ₗ[R] R) 0 : (a : L) → R) 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
z w : L
h :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    z
h_1 :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    w
hz : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
hw : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (z + w) : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
simp [hz, hw]
-- 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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
t : R
z : L
h :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    z
hz : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (t • z) : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
simp [hz]
-- 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 : L
k : ℕ
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y
zero :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
        (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
        Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R))
    {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs (k + 1) ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : 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 : R)

Tactic:
induction k generalizing x y with
  | zero =>
    replace hy : y = 0 := by simpa using hy
    simp [hy]
  | succ k ih =>
    rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
    simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx
    refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
    · rintro - ⟨z, w, hw, rfl⟩
      rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
      exact ih hw (hy _)
    · simp
    · simp [hz, hw]
    · simp [hz]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LinearMap.neg_apply, LieSubmodule.ucs_succ, neg_eq_zero, LieIdeal.lcs_succ, map_neg, lie_skew, LieModule.traceForm_apply_lie_apply, LieSubmodule.mem_top, LieSubmodule.mem_normalizer, rfl, true_and
-- 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 : L
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
hy : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) y
hx₁ : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 1) x
hy₁ : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 1 ⊥) y
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1

Premises used: LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs, OfNat.ofNat
-- 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 : L
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
hy : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) y
⊢ Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 1) x

Tactic:
simpa using 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
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
hy : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) y
⊢ Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 1 ⊥) y

Tactic:
simpa using hy
-- 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 : IsTrivial 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 : IsTrivial L M
x y : L
this :
  Eq.{u_4 + 1} (α := 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)
    0
⊢ 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 [traceForm_apply_apply, this]

Premises used: 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 : IsTrivial L M
x y : L
H :
  Eq.{u_4 + 1} (α := 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)
    0
⊢ 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:
suffices φ x ∘ₗ φ y = 0 by simp [traceForm_apply_apply, this]
-- 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 : IsTrivial L M
x y : L
H :
  ∀ (m : M),
    Eq (α := 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 :
            (a : M) → M)
          m :
        M)
      ((0 : (a : M) → M) m : M)
⊢ Eq.{u_4 + 1} (α := 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)
    0

Tactic:
ext m
-- 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 : IsTrivial L M
x y : L
m : M
⊢ Eq (α := 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 :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero