awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
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α
⊢ HAdd.hAdd (β := L) (x_pos + 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

Premises used: IsSl2Triple.e_ne_zero, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
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α
⊢ 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 (Weight.IsNonZero.neg hα) hx_neg hfα ht.f_ne_zero

Premises used: LieModule.Weight.IsNonZero.neg, IsSl2Triple.f_ne_zero, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
⊢ ∃ (c₃ : K), c₃ • coroot α = y

Tactic:
simpa [← mem_span_singleton, ← coe_corootSpace_eq_span_singleton α]

Premises used: Submodule.mem_span_singleton, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
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α
⊢ 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⟩ : ∃ c₃ : K, c₃ • coroot α = y := by
      simpa [← mem_span_singleton, ← coe_corootSpace_eq_span_singleton α]

Premises used: LieAlgebra.IsKilling.coroot, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
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⁆
⊢ HAdd.hAdd (β := L) (c₁ • e + c₂ • f)
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) (c₃ • coroot α) : L) ∈
    sl2SubalgebraOfRoot hα

Tactic:
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα]

Premises used: LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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 α
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⁆
⊢ ∃ (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:
use c₁, c₂, c₃
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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) =
    c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
simp [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, -LieSubmodule.incl_coe]

Premises used: IsSl2Triple.h_eq_coroot, LieSubmodule.incl_coe, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
rw : genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α ≠ ⊥
⊢ sl2SubmoduleOfRoot hα ≠ ⊥

Tactic:
rw [sl2SubmoduleOfRoot_eq_sup]

Premises used: LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α ≠ ⊥

Tactic:
ne_bot_of_le_ne_bot α.genWeightSpace_ne_bot (le_sup_of_le_left le_sup_left)

Premises used: ne_bot_of_le_ne_bot, le_sup_left, le_sup_of_le_left, LieModule.Weight.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
⊢ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α ≠ ⊥

Tactic:
exact ne_bot_of_le_ne_bot α.genWeightSpace_ne_bot (le_sup_of_le_left le_sup_left)

Premises used: ne_bot_of_le_ne_bot, le_sup_left, le_sup_of_le_left, LieModule.Weight.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ (↑α : Weight K (↥H) L).IsNonZero

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
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))
⊢ 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)

Tactic:
rw [restrict_killingForm, traceForm_eq_sum_finrank_nsmul' K H L]

Premises used: LieModule.traceForm_eq_sum_finrank_nsmul', Membership.mem, Subtype, LieAlgebra.restrict_killingForm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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))

Tactic:
Finset.sum_congr rfl fun χ hχ ↦ ?_

Premises used: Set.Mem, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
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 χ)
⊢ 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:
refine Finset.sum_congr rfl fun χ hχ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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)) χ
⊢ χ.IsNonZero

Tactic:
simpa [LieSubalgebra.root] using hχ

Premises used: LieSubalgebra.root
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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)) χ
⊢ χ.IsNonZero

Tactic:
replace hχ : χ.IsNonZero := by simpa [LieSubalgebra.root] using hχ
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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
⊢ 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:
simp [finrank_rootSpace_eq_one _ hχ]

Premises used: LieAlgebra.IsKilling.finrank_rootSpace_eq_one
-- Module: Mathlib.Algebra.Lie.Weights.Killing
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)

Tactic:
le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ hα ↦ hα))

Premises used: iSup₂_le, le_antisymm, sup_le, inf_le_left