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 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
suffices :
  LinearMap.restrict
      (((φ : 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)
      hy' =
    0
⊢ 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 ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
    (0 : R)

Tactic:
suffices (φ x ∘ₗ φ y).restrict hy' = 0 by
    simp [this, N.trace_eq_trace_restrict_of_le_idealizer I h x 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 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
h₁ :
  ∀ (n : ↥N),
    Eq.{u_4 + 1} (α := M)
      (↑((LinearMap.restrict
                (((φ : 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)
                hy' :
              (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M))
            n) :
        M)
      (↑((0 : (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M)) n) : M)
⊢ LinearMap.restrict
      (((φ : 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)
      hy' =
    0

Tactic:
ext (n : N)
-- 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
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
n : ↥N
this : ⁅y, (↑n : M)⁆ = 0
⊢ Eq.{u_4 + 1} (α := M)
    (↑((LinearMap.restrict
              (((φ : 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)
              hy' :
            (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M))
          n) :
      M)
    (↑((0 : (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M)) n) : M)

Tactic:
simp [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 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
n : ↥N
h₁ : ⁅y, (↑n : M)⁆ = 0
⊢ Eq.{u_4 + 1} (α := M)
    (↑((LinearMap.restrict
              (((φ : 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)
              hy' :
            (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M))
          n) :
      M)
    (↑((0 : (a : ↥(↑N : Submodule R M)) → ↥(↑N : Submodule R M)) n) : M)

Tactic:
suffices ⁅y, (n : M)⁆ = 0 by simp [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 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
n : ↥N
⊢ ⁅y, (↑n : M)⁆ = 0

Tactic:
Submodule.coe_eq_zero.mpr (LieModule.IsTrivial.trivial (⟨y, hy⟩ : I) n)

Premises used: Iff.mpr, Subtype.mk, Submodule.coe_eq_zero, LieModule.IsTrivial.trivial
-- 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
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : 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) :=
  ⋯
n : ↥N
⊢ ⁅y, (↑n : M)⁆ = 0

Tactic:
exact Submodule.coe_eq_zero.mpr (LieModule.IsTrivial.trivial (⟨y, hy⟩ : I) n)

Premises used: Iff.mpr, Subtype.mk, Submodule.coe_eq_zero, LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
    ((trace R L : (a : L →ₗ[R] L) → R) ((ad R L : (a : L) → End R L) x ∘ₗ (ad R L : (a : L) → End R L) y) : R)

Tactic:
LieModule.traceForm_apply_apply R L L x y

Premises used: LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_3} ↥H
x₀ x₁ : L
hx₀ : x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H
hx₁ : Membership.mem (γ := LieSubmodule R (↥H) L) (LieModule.posFittingComp R (↥H) L) x₁
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x₀ : L →ₗ[R] R) : (a : L) → R) x₁ : R) (0 : R)

Tactic:
LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting R H L
    (fun x y z ↦ LieModule.traceForm_apply_lie_apply' R L L x y z) hx₀ hx₁

Premises used: Membership.mem, Subtype, LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting, Subtype.val, LieModule.traceForm_apply_lie_apply'
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ (↑(killingCompl R L I) : Submodule R L) = LinearMap.BilinForm.orthogonal (killingForm R L) (↑I : Submodule R L)

Tactic:
rfl

Premises used: Submodule.orthogonalBilin, LinearMap.BilinForm.orthogonal, rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ killingCompl R L I ↔
    ∀ y ∈ I,
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R) (0 : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h :
  ∀ (x : L),
    Membership.mem (γ := Submodule R L) (LieSubalgebra.toSubmodule (toLieSubalgebra R L (killingCompl R L ⊤))) x ↔
      Membership.mem (γ := Submodule R L) (LinearMap.ker (killingForm R L)) x
⊢ Eq (α := Submodule R L) (LieSubalgebra.toSubmodule (toLieSubalgebra R L (killingCompl R L ⊤)))
    (LinearMap.ker (killingForm R L))

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ Membership.mem (γ := Submodule R L) (LieSubalgebra.toSubmodule (toLieSubalgebra R L (killingCompl R L ⊤))) x ↔
    Membership.mem (γ := Submodule R L) (LinearMap.ker (killingForm R L)) x

Tactic:
simp [LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LieModule.traceForm_comm R L L x]

Premises used: LieModule.traceForm_comm, LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ LinearMap.BilinForm.restrict (killingForm R L) (toLieSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥I) L

Tactic:
rfl

Premises used: LinearMap.restrictScalars, Set.Mem, LinearMap.compr₂, LinearMap.domRestrict₁₂, LinearMap.domRestrict, LinearMap.BilinForm.restrict, rfl, LieModule.traceForm
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
⊢ I ≤ LieSubmodule.idealizer I

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
inst_7 : IsLieAbelian.{u_3} ↥I
x : L
x₁ : ∀ (hx : x ∈ I), Membership.mem (γ := LieSubmodule R L L) (killingCompl R L ⊤) x
⊢ x ∈ I → Membership.mem (γ := LieSubmodule R L L) (killingCompl R L ⊤) x

Tactic:
(hx : x ∈ I)
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
inst_7 : IsLieAbelian.{u_3} ↥I
x : L
hx : x ∈ I
simp :
  ∀ (y : L),
    Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R) (0 : R)
⊢ Membership.mem (γ := LieSubmodule R L L) (killingCompl R L ⊤) x

Tactic:
simp only [mem_killingCompl, LieSubmodule.mem_top, forall_true_left]

Premises used: forall_true_left, LieIdeal.mem_killingCompl, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
inst_7 : IsLieAbelian.{u_3} ↥I
x : L
hx : x ∈ I
y : L
rw :
  Eq.{u_1 + 1} (α := R)
    ((trace R L : (a : L →ₗ[R] L) → R)
        ((LieModule.toEnd R L L : (a : L) → End R L) y ∘ₗ (LieModule.toEnd R L L : (a : L) → End R L) x) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R) (0 : R)

Tactic:
rw [LieModule.traceForm_apply_apply]

Premises used: LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
inst_7 : IsLieAbelian.{u_3} ↥I
x : L
hx : x ∈ I
y : L
⊢ I ≤ LieSubmodule.idealizer I

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : Free R L
inst_4 : Module.Finite R L
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
inst_7 : IsLieAbelian.{u_3} ↥I
x : L
hx : x ∈ I
y : L
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R L : (a : L →ₗ[R] L) → R)
        ((LieModule.toEnd R L L : (a : L) → End R L) y ∘ₗ (LieModule.toEnd R L L : (a : L) → End R L) x) :
      R)
    (0 : R)

Tactic:
exact LieSubmodule.traceForm_eq_zero_of_isTrivial I I (by simp) _ hx

Premises used: LieSubmodule.traceForm_eq_zero_of_isTrivial
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
x y : L
⊢ ∀ (χ : Weight K L M),
    MapsTo
      (⇑(((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) :
        (a : M) → M)
      (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M) (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M)

Tactic:
have hxy : ∀ χ : Weight K L M, MapsTo (toEnd K L M x ∘ₗ toEnd K L M y)
      (genWeightSpace M χ) (genWeightSpace M χ) :=
    fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
x y : L
hxy :
  ∀ (χ : Weight K L M),
    MapsTo
      (⇑(((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) :
        (a : M) → M)
      (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M) (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M)
⊢ DirectSum.IsInternal (S := Submodule K M) fun (i : Weight K L M) ↦
    (↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace' K L M)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top' K L M)
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
x y : L
hxy :
  ∀ (χ : Weight K L M),
    MapsTo
      (⇑(((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) :
        (a : M) → M)
      (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M) (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M)
hds :
  DirectSum.IsInternal (S := Submodule K M) fun (i : Weight K L M) ↦
    (↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)
simp_rw :
  Eq.{u_2 + 1} (α := K)
    (∑ i : Weight K L M,
      (trace K ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) :
          (a :
              ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) →ₗ[K]
                ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)) →
            K)
        (LinearMap.restrict
          (((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y)
          ⋯))
    (∑ x_1 : Weight K L M,
      (((traceForm.{u_2, u_3, u_4} K L ↥(genWeightSpace M (⇑x_1 : (a : L) → K)) : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) :
          (a : L) → K)
        y)
⊢ Eq.{u_2 + 1} (α := K) ((((traceForm K L M : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    (∑ χ : Weight K L M,
        finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K)) •
          HMul.hMul (α := K) (β := K) ((χ : (a : L) → K) x : K) ((χ : (a : L) → K) y : K) :
      K)

Tactic:
simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
    ← traceForm_genWeightSpace_eq K L M _ x y]

Premises used: LinearMap.trace_eq_sum_trace_restrict, LieModule.traceForm_genWeightSpace_eq, LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
x y : L
hxy :
  ∀ (χ : Weight K L M),
    MapsTo
      (⇑(((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) :
        (a : M) → M)
      (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M) (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M)
hds :
  DirectSum.IsInternal (S := Submodule K M) fun (i : Weight K L M) ↦
    (↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)
⊢ Eq.{u_2 + 1} (α := K)
    (∑ i : Weight K L M,
      (trace K ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) :
          (a :
              ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) →ₗ[K]
                ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)) →
            K)
        (LinearMap.restrict
          (((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y)
          ⋯))
    (∑ x_1 : Weight K L M,
      (((traceForm.{u_2, u_3, u_4} K L ↥(genWeightSpace M (⇑x_1 : (a : L) → K)) : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) :
          (a : L) → K)
        y)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
x y : L
hxy :
  ∀ (χ : Weight K L M),
    MapsTo
      (⇑(((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
            ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y) :
        (a : M) → M)
      (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M) (↑(genWeightSpace M (⇑χ : (a : L) → K)) : Set M)
have have₁ have₂ :
  ∀
    (hds :
      DirectSum.IsInternal (S := Submodule K M) fun (i : Weight K L M) ↦
        (↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)),
    Eq.{u_2 + 1} (α := K) ((((traceForm K L M : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      (∑ χ : Weight K L M,
          finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K)) •
            HMul.hMul (α := K) (β := K) ((χ : (a : L) → K) x : K) ((χ : (a : L) → K) y : K) :
        K)
have₃ :
  ∀
    (hds :
      DirectSum.IsInternal (S := Submodule K M) fun (i : Weight K L M) ↦
        (↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)),
    Eq.{u_2 + 1} (α := K)
      (∑ i : Weight K L M,
        (trace K ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) :
            (a :
                ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M) →ₗ[K]
                  ↥(↑(genWeightSpace M (⇑i : (a : L) → K)) : Submodule K M)) →
              K)
          (LinearMap.restrict
            (((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) x ∘ₗ
              ((toEnd K L M : LieHom.{u_2, u_3, u_4} K L (End K M)) : (a : L) → End K M) y)
            ⋯))
      (∑ x_1 : Weight K L M,
        (((traceForm.{u_2, u_3, u_4} K L ↥(genWeightSpace M (⇑x_1 : (a : L) → K)) : (a : L) → L →ₗ[K] K) x :
              L →ₗ[K] K) :
            (a : L) → K)
          y)
⊢ Eq.{u_2 + 1} (α := K) ((((traceForm K L M : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    (∑ χ : Weight K L M,
        finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K)) •
          HMul.hMul (α := K) (β := K) ((χ : (a : L) → K) x : K) ((χ : (a : L) → K) y : K) :
      K)

Tactic:
classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace' K L M)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top' K L M)
  simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
    ← traceForm_genWeightSpace_eq K L M _ x y]
  rfl

Premises used: LieModule.traceForm_genWeightSpace_eq, LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
K : Type u_2
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : Module K M
inst_6 : LieModule K L M
inst_7 : FiniteDimensional K M
inst_8 : LieRing.IsNilpotent L
inst_9 : LinearWeights K L M
inst_10 : IsTriangularizable K L M
H :
  ∀ (x y : L),
    Eq.{u_2 + 1} (α := K) ((((traceForm K L M : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((((∑ χ : Weight K L M,
                    HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K)))
                      ((Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)) :
                  (a : L) → L →ₗ[K] K)
                x :
              L →ₗ[K] K) :
            (a : L) → K)
          y :
        K)
⊢ Eq (α := LinearMap.BilinForm K L) (traceForm K L M)
    (∑ χ : Weight K L M,
      HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K)))
        ((Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)))

Tactic:
ext