awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux :
  ∀ {β : Weight K (↥H) L} (hβ : β.IsNonZero) {y g : L}
    (hy : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β : (a : ↥H) → K)) y)
    (hg : g ∈ rootSpace H (⇑β : (a : ↥H) → K)) (hg_ne_zero : g ≠ 0), ∃ (c : K), y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
x_pos : L
hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) x_pos
x_neg : L
hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) x_neg
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (x_pos + x_neg)
hx :
  HAdd.hAdd (β := L) (x_pos + x_neg)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ HAdd.hAdd (β := L) (x_pos + x_neg)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
have h : ∀ (c₁ : K)
  (hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) (c₁ • e))
  (hx_αneg :
    Membership.mem (γ := Submodule K L)
      (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L)
      (c₁ • e + x_neg))
  (hx :
    HAdd.hAdd (β := L) (c₁ • e + x_neg)
        (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
      genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α),
  HAdd.hAdd (β := L) (c₁ • e + x_neg)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
Tactic: obtain ⟨c₁, rfl⟩ := aux hα hx_pos heα ht.e_ne_zero
Cleared hypotheses: x_pos, hx_pos, hx_αneg, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux :
  ∀ {β : Weight K (↥H) L} (hβ : β.IsNonZero) {y g : L}
    (hy : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β : (a : ↥H) → K)) y)
    (hg : g ∈ rootSpace H (⇑β : (a : ↥H) → K)) (hg_ne_zero : g ≠ 0), ∃ (c : K), y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
x_neg : L
hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) x_neg
c₁ : K
hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) (c₁ • e)
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (c₁ • e + x_neg)
hx :
  HAdd.hAdd (β := L) (c₁ • e + x_neg)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ HAdd.hAdd (β := L) (c₁ • e + x_neg)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
have h : ∀ (c₂ : K)
  (hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (c₂ • f))
  (hx_αneg :
    Membership.mem (γ := Submodule K L)
      (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L)
      (c₁ • e + c₂ • f))
  (hx :
    HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
        (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
      genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α),
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
Tactic: obtain ⟨c₂, rfl⟩ := aux (Weight.IsNonZero.neg hα) hx_neg hfα ht.f_ne_zero
Cleared hypotheses: x_neg, hx_neg, hx_αneg, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux :
  ∀ {β : Weight K (↥H) L} (hβ : β.IsNonZero) {y g : L}
    (hy : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β : (a : ↥H) → K)) y)
    (hg : g ∈ rootSpace H (⇑β : (a : ↥H) → K)) (hg_ne_zero : g ≠ 0), ∃ (c : K), y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
c₁ : K
hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) (c₁ • e)
c₂ : K
hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (c₂ • f)
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L)
    (c₁ • e + c₂ • f)
hx :
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
have h : ∀ (c₃ : K)
  (hy_coroot :
    c₃ • coroot α ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule))
  (hx :
    HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
        (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
      genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α),
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
    sl2SubmoduleOfRoot hα
Tactic: obtain ⟨c₃, rfl⟩ : ∃ c₃ : K, c₃ • coroot α = y := by
      simpa [← mem_span_singleton, ← coe_corootSpace_eq_span_singleton α]
Cleared hypotheses: y, hy_coroot, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux :
  ∀ {β : Weight K (↥H) L} (hβ : β.IsNonZero) {y g : L}
    (hy : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β : (a : ↥H) → K)) y)
    (hg : g ∈ rootSpace H (⇑β : (a : ↥H) → K)) (hg_ne_zero : g ≠ 0), ∃ (c : K), y = c • g
c₁ : K
hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) (c₁ • e)
c₂ : K
hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (c₂ • f)
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L)
    (c₁ • e + c₂ • f)
c₃ : K
hy_coroot :
  c₃ • coroot α ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
hx :
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
    sl2SubalgebraOfRoot hα
have h : ∃ (c₁_1 : K) (c₂_1 : K) (c₃_1 : K),
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) =
    c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
Tactic: rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux :
  ∀ {β : Weight K (↥H) L} (hβ : β.IsNonZero) {y g : L}
    (hy : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑β : (a : ↥H) → K)) y)
    (hg : g ∈ rootSpace H (⇑β : (a : ↥H) → K)) (hg_ne_zero : g ≠ 0), ∃ (c : K), y = c • g
c₁ : K
hx_pos : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (⇑α : (a : ↥H) → K)) : Submodule K L) (c₁ • e)
c₂ : K
hx_neg : Membership.mem (γ := Submodule K L) (↑(genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) (c₂ • f)
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L)
    (c₁ • e + c₂ • f)
c₃ : K
hy_coroot :
  c₃ • coroot α ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
hx :
  HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ ∃ (c₁_1 : K) (c₂_1 : K) (c₃_1 : K),
    HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
        (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) =
      c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
have h : HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
    (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) =
  c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
Tactic: use c₁, c₂, c₃
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ sl2SubmoduleOfRoot hα ≠ ⊥
have rw : genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α ≠ ⊥
Tactic: rw [sl2SubmoduleOfRoot_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
⊢ LinearMap.BilinForm.restrict (killingForm K L) H.toSubmodule =
    ∑ α ∈ (LieSubalgebra.root : Finset (Weight K (↥H) L)),
      ((Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α) :
        ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
have rw : Eq (α := LinearMap.BilinForm.{u_2, u_3} K ↥H.toSubmodule)
  (∑ χ : Weight K (↥H) L with χ.IsNonZero,
    HSMul.hSMul (β := ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
      (finrank.{u_2, u_3} K ↥(genWeightSpace L (⇑χ : (a : ↥H) → K)))
      ((Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)))
  (∑ α ∈ (LieSubalgebra.root : Finset (Weight K (↥H) L)),
    ((Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α) :
      ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
Tactic: rw [restrict_killingForm, traceForm_eq_sum_finrank_nsmul' K H L]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
⊢ Eq (α := LinearMap.BilinForm.{u_2, u_3} K ↥H.toSubmodule)
    (∑ χ : Weight K (↥H) L with χ.IsNonZero,
      HSMul.hSMul (β := ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
        (finrank.{u_2, u_3} K ↥(genWeightSpace L (⇑χ : (a : ↥H) → K)))
        ((Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)))
    (∑ α ∈ (LieSubalgebra.root : Finset (Weight K (↥H) L)),
      ((Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α) :
        ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
have refine : ∀ (χ : Weight K (↥H) L)
  (hχ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) χ),
  HSMul.hSMul (β := ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
      (finrank.{u_2, u_3} K ↥(genWeightSpace L (⇑χ : (a : ↥H) → K)))
      ((Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)
Tactic: refine Finset.sum_congr rfl fun χ hχ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
χ : Weight K (↥H) L
hχ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) χ
⊢ HSMul.hSMul (β := ↥H →ₗ[K] LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
      (finrank.{u_2, u_3} K ↥(genWeightSpace L (⇑χ : (a : ↥H) → K)))
      ((Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)) =
    (Weight.toLinear K (↥H) L χ).smulRight (Weight.toLinear K (↥H) L χ)
have hχ₁ : χ.IsNonZero
Tactic: replace hχ : χ.IsNonZero := by simpa [LieSubalgebra.root] using hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have refine : LieSubmodule.restr I H ≤
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
Tactic: refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ hα ↦ hα))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
| LieSubmodule.restr I H
have rw : LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
  ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
Tactic: rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have conv_lhs : LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
    ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
Tactic: conv_lhs => rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have refine : ∀ (α : Weight K (↥H) L) (hα : α.IsNonZero),
  LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
Tactic: refine sup_le_sup_left (iSup₂_le fun α hα ↦ ?_) _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have pos : ∀ (h : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
  LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
Tactic: by_cases h : rootSpace H α ≤ I.restr H
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
pos :
  ∀ (h : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
    LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have neg : ∀ (h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
  LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
Tactic: by_cases h : rootSpace H α ≤ I.restr H
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have ha : IsAtom (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L)
Tactic: have ha := Submodule.isAtom_iff_finrank_eq_one.mpr (finrank_rootSpace_eq_one α hα)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
ha : IsAtom (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L)
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
have this : LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) = ⊥
Tactic: have : I.restr H ⊓ rootSpace H (α : H → K) = ⊥ :=
      LieSubmodule.toSubmodule_injective ((ha.not_le_iff_disjoint.mp h).symm.eq_bot)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
χ : Weight R L M
h : χ.IsZero
⊢ toLinear R L M χ = 0
have h₁ : ∀ (x : L), Eq.{u_2 + 1} (α := R) ((toLinear R L M χ : (a : L) → R) x : R) ((0 : (a : L) → R) x : R)
Tactic: ext