awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
⊢ 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 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)
          sorry))
    (∑ 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: 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 (α := 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 χ)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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) ((((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)
have 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)
Tactic: rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ 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 χ)))
have 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 χ))
Tactic: rw [traceForm_eq_sum_finrank_nsmul,
      ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 (α := 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 χ)))
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
have 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
Tactic: refine Finset.sum_eq_zero fun χ hχ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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} χ
⊢ 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
have hχ₁ : Weight.toLinear K L M χ = 0
Tactic: replace hχ : (χ : L →ₗ[K] K) = 0 := by simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 (α := 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 χ)))
have 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
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χ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ 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 χ)))
have 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
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χ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ 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 χ)))
have 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
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χ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 (α := 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)
have 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)
Tactic: rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coe_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
have 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)
Tactic: refine Submodule.sum_mem _ fun χ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 (α := 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)
have 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 χ)))
Tactic: simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, Weight.toLinear_apply,
    ← Nat.cast_smul_eq_nsmul K]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (hypothesis)
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)
⊢ 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))
have 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)
Tactic: rw [map_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.UniversalEnveloping (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f_1 f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
h : Rel R L a b
⊢ Eq.{u₃ + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        a :
      A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        b :
      A)
have lie_compat : ∀ (x y : L),
  Eq.{u₃ + 1} (α := A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        (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))) :
      A)
    ((((TensorAlgebra.lift R : (a : L →ₗ[R] A) → TensorAlgebra R L →ₐ[R] A) (↑f : L →ₗ[R] A) :
            TensorAlgebra R L →ₐ[R] A) :
          (a : TensorAlgebra R L) → A)
        (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)) :
      A)
Tactic: induction h
Cleared hypotheses: h