awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H :
  Eq.{u_2 + 1} (α := K)
    (∑ x_1 ∈ Finset.attach Finset.univ,
        finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑(↑x_1 : Weight K L M) : (a : L) → K)) •
          HMul.hMul (α := K) (β := K) (((↑x_1 : Weight K L M) : (a : L) → K) x : K)
            (((↑x_1 : Weight K L M) : (a : L) → K) y : K) :
      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.{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)

Tactic:
rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]

Premises used: Finset.sum_attach, LieModule.traceForm_eq_sum_finrank_nsmul_mul
-- 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
⊢ Eq.{u_2 + 1} (α := K)
    (∑ x_1 ∈ Finset.attach Finset.univ,
        finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑(↑x_1 : Weight K L M) : (a : L) → K)) •
          HMul.hMul (α := K) (β := K) (((↑x_1 : Weight K L M) : (a : L) → K) x : K)
            (((↑x_1 : Weight K L M) : (a : L) → K) y : K) :
      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)

Tactic:
simp [-LinearMap.coe_smul]

Premises used: LinearMap.coe_smul
-- 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
this :
  Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0
rw :
  HAdd.hAdd (α := L →ₗ[K] L →ₗ[K] K)
      (∑ x : Weight K L M with x.IsNonZero,
        HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑x : (a : L) → K)))
          ((Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x)))
      (∑ x : Weight K L M with ¬x.IsNonZero,
        HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑x : (a : L) → K)))
          ((Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x))) =
    ∑ χ : Weight K L M with χ.IsNonZero,
      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 χ))
⊢ Eq (α := LinearMap.BilinForm K L) (traceForm K L M)
    (∑ χ : Weight K L M with χ.IsNonZero,
      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:
rw [traceForm_eq_sum_finrank_nsmul,
      ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]

Premises used: LieModule.Weight.IsNonZero, LieModule.traceForm_eq_sum_finrank_nsmul, Finset.sum_filter_add_sum_filter_not
-- 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
this :
  Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0
⊢ HAdd.hAdd (α := L →ₗ[K] L →ₗ[K] K)
      (∑ x : Weight K L M with x.IsNonZero,
        HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑x : (a : L) → K)))
          ((Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x)))
      (∑ x : Weight K L M with ¬x.IsNonZero,
        HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑x : (a : L) → K)))
          ((Weight.toLinear K L M x).smulRight (Weight.toLinear K L M x))) =
    ∑ χ : Weight K L M with χ.IsNonZero,
      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:
simp [this]
-- 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
suffices :
  Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0
⊢ Eq (α := LinearMap.BilinForm K L) (traceForm K L M)
    (∑ χ : Weight K L M with χ.IsNonZero,
      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:
suffices ∑ χ ∈ {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) •
      (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) = 0 by
    rw [traceForm_eq_sum_finrank_nsmul,
      ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]
    simp [this]
-- 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
⊢ Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0

Tactic:
Finset.sum_eq_zero fun χ hχ ↦ ?_

Premises used: Finset.sum_eq_zero
-- 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
refine :
  ∀ (χ : Weight K L M) (hχ : Membership.mem (γ := Finset (Weight K L M)) {χ : Weight K L M | χ.IsZero} χ),
    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 χ)) =
      0
⊢ Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0

Tactic:
refine Finset.sum_eq_zero fun χ hχ ↦ ?_

Premises used: Finset.sum_eq_zero
-- 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
χ : Weight K L M
hχ : Membership.mem (γ := Finset (Weight K L M)) {χ : Weight K L M | χ.IsZero} χ
⊢ Weight.toLinear K L M χ = 0

Tactic:
simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ

Premises used: LieModule.Weight.coe_toLinear_eq_zero_iff
-- 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
χ : Weight K L M
hχ : Membership.mem (γ := Finset (Weight K L M)) {χ : Weight K L M | χ.IsZero} χ
⊢ Weight.toLinear K L M χ = 0

Tactic:
replace hχ : (χ : L →ₗ[K] K) = 0 := by simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ
-- 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
χ : Weight K L M
hχ : Weight.toLinear K L M χ = 0
⊢ 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 χ)) =
    0

Tactic:
simp [hχ]
-- 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
suffices suffices₁ suffices₂ :
  Eq (α := L →ₗ[K] L →ₗ[K] K)
    (∑ χ : Weight K L M with χ.IsZero,
      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 χ)))
    0
suffices₃ :
  ∀ (χ : Weight K L M) (hχ : Membership.mem (γ := Finset (Weight K L M)) {χ : Weight K L M | χ.IsZero} χ),
    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 χ)) =
      0
suffices₄ :
  ∀ (χ : Weight K L M) (hχ : Weight.toLinear K L M χ = 0),
    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 χ)) =
      0
⊢ Eq (α := LinearMap.BilinForm K L) (traceForm K L M)
    (∑ χ : Weight K L M with χ.IsNonZero,
      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:
classical
  suffices ∑ χ ∈ {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) •
      (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) = 0 by
    rw [traceForm_eq_sum_finrank_nsmul,
      ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]
    simp [this]
  refine Finset.sum_eq_zero fun χ hχ ↦ ?_
  replace hχ : (χ : L →ₗ[K] K) = 0 := by simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ
  simp [hχ]

Premises used: Finset.sum_eq_zero
-- 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 : L
rw :
  Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (∑ c : Weight K L M,
      (HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑c : (a : L) → K)))
            ((Weight.toLinear K L M c).smulRight (Weight.toLinear K L M c)) :
          (a : L) → L →ₗ[K] K)
        x)
⊢ Membership.mem (α := L →ₗ[K] K) (γ := Submodule K (L →ₗ[K] K))
    (span K (range (ι := Weight K L M) (Weight.toLinear K L M))) ((traceForm K L M : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K)

Tactic:
rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coe_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, LinearMap.coe_sum, LieModule.traceForm_eq_sum_finrank_nsmul
-- 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 : L
⊢ Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (∑ c : Weight K L M,
      (HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑c : (a : L) → K)))
            ((Weight.toLinear K L M c).smulRight (Weight.toLinear K L M c)) :
          (a : L) → L →ₗ[K] K)
        x)

Tactic:
Submodule.sum_mem _ fun χ _ ↦ ?_

Premises used: Set.Mem, Submodule.sum_mem
-- 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 : L
refine :
  ∀ (χ : Weight K L M),
    Membership.mem (γ := Finset (Weight K L M)) Finset.univ χ →
      Membership.mem (α := L →ₗ[K] K) (γ := Submodule K (L →ₗ[K] K))
        (span K (range (ι := Weight K L M) (Weight.toLinear 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)
⊢ Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (∑ c : Weight K L M,
      (HSMul.hSMul (β := L →ₗ[K] L →ₗ[K] K) (finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑c : (a : L) → K)))
            ((Weight.toLinear K L M c).smulRight (Weight.toLinear K L M c)) :
          (a : L) → L →ₗ[K] K)
        x)

Tactic:
refine Submodule.sum_mem _ fun χ _ ↦ ?_

Premises used: Submodule.sum_mem
-- 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 : L
χ : Weight K L M
h : Membership.mem (γ := Finset (Weight K L M)) Finset.univ χ
simp_rw :
  Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (HSMul.hSMul (α := K) (↑(finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K))) : K)
      (HSMul.hSMul (α := K) ((χ : (a : L) → K) x : K) (Weight.toLinear K L M χ)))
⊢ Membership.mem (α := L →ₗ[K] K) (γ := Submodule K (L →ₗ[K] K))
    (span K (range (ι := Weight K L M) (Weight.toLinear 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)

Tactic:
simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, Weight.toLinear_apply,
    ← Nat.cast_smul_eq_nsmul K]

Premises used: LinearMap.smul_apply, Nat.cast_smul_eq_nsmul, LinearMap.coe_smulRight, LieModule.Weight.toLinear_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 : L
χ : Weight K L M
h : Membership.mem (γ := Finset (Weight K L M)) Finset.univ χ
⊢ Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (HSMul.hSMul (α := K) (↑(finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K))) : K)
      (HSMul.hSMul (α := K) ((χ : (a : L) → K) x : K) (Weight.toLinear K L M χ)))

Tactic:
Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ

Premises used: Set.mem_range_self, Set.Mem, Submodule.subset_span, Submodule.smul_mem
-- 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 : L
χ : Weight K L M
h : Membership.mem (γ := Finset (Weight K L M)) Finset.univ χ
⊢ Membership.mem (γ := Submodule K (L →ₗ[K] K)) (span K (range (ι := Weight K L M) (Weight.toLinear K L M)))
    (HSMul.hSMul (α := K) (↑(finrank.{u_2, u_4} K ↥(genWeightSpace M (⇑χ : (a : L) → K))) : K)
      (HSMul.hSMul (α := K) ((χ : (a : L) → K) x : K) (Weight.toLinear K L M χ)))

Tactic:
exact Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ

Premises used: Set.mem_range_self, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
this :
  Eq (α := UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
      UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
      UniversalEnvelopingAlgebra R L)
⊢ (mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
      (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) =
    HMul.hMul (α := UniversalEnvelopingAlgebra R L) (β := UniversalEnvelopingAlgebra R L)
      ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x) :
        UniversalEnvelopingAlgebra R L)
      ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y) :
        UniversalEnvelopingAlgebra R L)

Tactic:
rw [map_mul] at this

Premises used: map_mul
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
this :
  (mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
      (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) =
    HMul.hMul (α := UniversalEnvelopingAlgebra R L) (β := UniversalEnvelopingAlgebra R L)
      ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x) :
        UniversalEnvelopingAlgebra R L)
      ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y) :
        UniversalEnvelopingAlgebra R L)
⊢ Eq (α := UniversalEnvelopingAlgebra R L)
    (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) ⁅x, y⁆)
    (Bracket.bracket (L := UniversalEnvelopingAlgebra R L)
      (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) x)
      (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) y))

Tactic:
simp [LieRing.of_associative_ring_bracket, ← this]

Premises used: LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
suffices :
  Eq (α := UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HAdd.hAdd (α := TensorAlgebra R L) ((ιₜ : (a : L) → TensorAlgebra R L) ⁅x, y⁆ : TensorAlgebra R L)
          (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)
            ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L))) :
      UniversalEnvelopingAlgebra R L)
    ((mkAlgHom R L : (a : TensorAlgebra R L) → UniversalEnvelopingAlgebra R L)
        (HMul.hMul (α := TensorAlgebra R L) (β := TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) x : TensorAlgebra R L)
          ((ιₜ : (a : L) → TensorAlgebra R L) y : TensorAlgebra R L)) :
      UniversalEnvelopingAlgebra R L)
⊢ Eq (α := UniversalEnvelopingAlgebra R L)
    (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) ⁅x, y⁆)
    (Bracket.bracket (L := UniversalEnvelopingAlgebra R L)
      (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) x)
      (AddHom.toFun (LinearMap.toAddHom (AlgHom.toLinearMap (mkAlgHom R L) ∘ₗ ιₜ)) y))

Tactic:
suffices mkAlgHom R L (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) = mkAlgHom R L (ιₜ x * ιₜ y) by
        rw [map_mul] at this; simp [LieRing.of_associative_ring_bracket, ← this]