awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ ⁅(↑h : L), ⁅e, f⁆⁆ = 0
have suffices : ⁅e, f⁆ ∈ rootSpace H 0
Tactic: suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
        lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ ⁅e, f⁆ ∈ rootSpace H 0
have rw : (↑(coroot α) : L) ∈ H.toLieSubmodule
Tactic: rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ ∃ (c₁_1 : K) (c₂_1 : K) (c₃_1 : K),
    c₁ • ⁅(↑h : L), e⁆ + c₂ • ⁅(↑h : L), f⁆ + c₃ • ⁅(↑h : L), ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
have hef_zero : ⁅(↑h : L), ⁅e, f⁆⁆ = 0
Tactic: have hef_zero : ⁅(h : L), ⁅e, f⁆⁆ = 0 := by
      suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
        lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
      rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]
      exact (coroot α).property
-- 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α =
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : ∀ (x : L),
  x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: ext x
-- 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
x : L
⊢ x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : ∀ (h' e f : L) (ht : IsSl2Triple h' e f) (heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
  (hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
  x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: obtain ⟨h', e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero 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
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : ∀ (hx : x ∈ sl2SubmoduleOfRoot hα),
  x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: refine ⟨fun hx ↦ ?_, fun 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h :
  ∀ (hx : x ∈ sl2SubmoduleOfRoot hα),
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h₁ : ∀ (hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α),
  x ∈ sl2SubmoduleOfRoot hα
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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α : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ sl2SubmoduleOfRoot hα
⊢ x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have hx₁ : x ∈ sl2SubalgebraOfRoot hα
Tactic: replace hx : x ∈ sl2SubalgebraOfRoot hα := hx
Cleared hypotheses: 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ sl2SubalgebraOfRoot hα
⊢ x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : ∀ (c₁ c₂ c₃ : K) (hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα),
  c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: obtain ⟨c₁, c₂, c₃, rfl⟩ := (mem_sl2SubalgebraOfRoot_iff hα ht heα hfα).mp hx
Cleared hypotheses: x, 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : c₁ • e ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: refine add_mem (add_mem ?_ ?_) ?_
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h : c₁ • e ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h₁ : c₂ • f ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: refine add_mem (add_mem ?_ ?_) ?_
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h : c₁ • e ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
h₁ : c₂ • f ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h₂ : c₃ • ⁅e, f⁆ ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
Tactic: refine add_mem (add_mem ?_ ?_) ?_
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₃ • ⁅e, f⁆ ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
have h : ∃ (y : ↥H),
  Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y ∧
    (H.subtype : (a : ↥H.toSubmodule) → L) y = c₃ • h'
Tactic: suffices ∃ y ∈ corootSpace α, H.subtype y = c₃ • h' from
        mem_sup_right <| by simpa [ht.lie_e_f, -Subtype.exists]
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ (y : ↥H),
    Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y ∧
      (H.subtype : (a : ↥H.toSubmodule) → L) y = c₃ • h'
have h : (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'
Tactic: refine ⟨c₃ • coroot α, smul_mem _ _ <| by simp, ?_⟩
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'
have h : (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • (↑(coroot α) : L)
Tactic: rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h : (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • (↑(coroot α) : L)
⊢ (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'
have h₁ : HSMul.hSMul (β := L) c₃ ((H.subtype : (a : ↥H.toSubmodule) → L) (coroot α) : L) = c₃ • (↑(coroot α) : L)
Tactic: rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h : (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • (↑(coroot α) : L)
h₁ : HSMul.hSMul (β := L) c₃ ((H.subtype : (a : ↥H.toSubmodule) → L) (coroot α) : L) = c₃ • (↑(coroot α) : L)
⊢ (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'
have h₂ : c₃ • (↑(coroot α) : L) = c₃ • (↑(coroot α) : L)
Tactic: rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]
-- 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
β : 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
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg ≠ 0
have rwa : ¬Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg = 0
Tactic: rwa [ne_eq, LieSubmodule.mk_eq_zero]
-- 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
β : 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
rwa : ¬Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg = 0
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg ≠ 0
have rwa₁ : ¬g = 0
Tactic: rwa [ne_eq, LieSubmodule.mk_eq_zero]
-- 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
β : 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
have obtain : ∀ (c : K)
  (hc :
    c • Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg =
      Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) y hy),
  ∃ (c : K), y = c • g
Tactic: obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨g, hg⟩
        (by rwa [ne_eq, LieSubmodule.mk_eq_zero])).mp (finrank_rootSpace_eq_one β hβ) ⟨y, hy⟩
-- 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α : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ x ∈ sl2SubmoduleOfRoot hα
have 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
Tactic: have aux {β : Weight K H L} (hβ : β.IsNonZero) {y g : L}
        (hy : y ∈ genWeightSpace L β) (hg : g ∈ rootSpace H β) (hg_ne_zero : g ≠ 0) :
        ∃ c : K, y = c • g := by
      obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨g, hg⟩
        (by rwa [ne_eq, LieSubmodule.mk_eq_zero])).mp (finrank_rootSpace_eq_one β hβ) ⟨y, hy⟩
      exact ⟨c, by simpa using hc.symm⟩
-- 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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
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
⊢ x ∈ sl2SubmoduleOfRoot hα
have h : ∀ (x_αneg : L)
  (hx_αneg :
    Membership.mem (γ := Submodule K L)
      (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) x_αneg)
  (y : ↥H.toLieSubmodule)
  (hy_coroot : y ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule))
  (hx :
    HAdd.hAdd (β := L) 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_αneg
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
Tactic: obtain ⟨x_αneg, hx_αneg, x_h, ⟨y, hy_coroot, rfl⟩, rfl⟩ := mem_sup.mp hx
Cleared hypotheses: x, 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
x_αneg : L
hx_αneg :
  Membership.mem (γ := Submodule K L)
    (↑(genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K))) : Submodule K L) x_αneg
y : ↥H.toLieSubmodule
hy_coroot : y ∈ (↑(↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H.toLieSubmodule) : Set ↥H.toLieSubmodule)
hx :
  HAdd.hAdd (β := L) 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_αneg
      (((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[K] L) : (a : ↥H.toLieSubmodule) → L) y : L) ∈
    sl2SubmoduleOfRoot hα
have h : ∀ (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α
Tactic: obtain ⟨x_pos, hx_pos, x_neg, hx_neg, rfl⟩ := mem_sup.mp hx_αneg
Cleared hypotheses: x_αneg, hx_αneg, hx