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
α : Weight K (↥H) L
⊢ (↑(coroot α) : L) ∈ corootSubmodule α

Tactic:
(LieSubmodule.mem_map _).mpr
    ⟨⟨coroot α, (coroot α).property⟩, coroot_mem_corootSpace α, rfl⟩

Premises used: Iff.mpr, Set.Mem, LieAlgebra.IsKilling.coroot, LieAlgebra.IsKilling.coroot_mem_corootSpace, Subtype.mk, And.intro, Exists.intro, Subtype.val, rfl, LieSubmodule.mem_map, Subtype.property
-- 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 :
  ∀ (x : L),
    x ∈ sl2SubmoduleOfRoot hα ↔
      x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α
⊢ sl2SubmoduleOfRoot hα =
    genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
ext x
-- 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
x : L
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 α
⊢ 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α

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- 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
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 α

Tactic:
⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- 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
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 α
h₁ :
  ∀ (hx : x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α),
    x ∈ sl2SubmoduleOfRoot hα
⊢ x ∈ sl2SubmoduleOfRoot hα ↔
    x ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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
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 ∈ sl2SubalgebraOfRoot hα

Tactic:
replace hx : x ∈ sl2SubalgebraOfRoot hα := hx
-- 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
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α
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 α
⊢ x ∈ 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

Premises used: Iff.mp, LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, 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))
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:
add_mem (add_mem ?_ ?_) ?_

Premises used: AddMemClass.add_mem
-- 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))
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 α
h₂ : c₃ • ⁅e, 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 α

Tactic:
refine add_mem (add_mem ?_ ?_) ?_

Premises used: AddMemClass.add_mem
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₁ • e ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
mem_sup_left <| mem_sup_left <| smul_mem _ _ heα

Premises used: Set.Mem, Submodule.mem_sup_left, Submodule.smul_mem
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₁ • e ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
exact mem_sup_left <| mem_sup_left <| smul_mem _ _ heα

Premises used: Submodule.mem_sup_left, Submodule.smul_mem
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₂ • f ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
mem_sup_left <| mem_sup_right <| smul_mem _ _ hfα

Premises used: Set.Mem, Submodule.mem_sup_left, Submodule.mem_sup_right, Submodule.smul_mem
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₂ • f ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
exact mem_sup_left <| mem_sup_right <| smul_mem _ _ hfα

Premises used: Submodule.mem_sup_left, Submodule.mem_sup_right, Submodule.smul_mem
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h :
  ∃ (y : ↥H),
    Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y ∧
      (H.subtype : (a : ↥H.toSubmodule) → L) y = c₃ • h'
⊢ c₃ • ⁅e, f⁆ ∈ genWeightSpace L (⇑α : (a : ↥H) → K) ⊔ genWeightSpace L (-(⇑α : (a : ↥H) → K)) ⊔ corootSubmodule α

Tactic:
suffices ∃ y ∈ corootSpace α, H.subtype y = c₃ • h' from
        mem_sup_right <| by simpa [ht.lie_e_f, -Subtype.exists]
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (coroot α)

Tactic:
simp
-- 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))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
h : (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'
⊢ ∃ (y : ↥H),
    Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y ∧
      (H.subtype : (a : ↥H.toSubmodule) → L) y = c₃ • h'

Tactic:
refine ⟨c₃ • coroot α, smul_mem _ _ <| by simp, ?_⟩
-- 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))
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₂ h₃ : c₃ • (↑(coroot α) : L) = c₃ • (↑(coroot α) : L)
⊢ (H.subtype : (a : ↥H.toSubmodule) → L) (c₃ • coroot α) = c₃ • h'

Tactic:
rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]

Premises used: Submodule.subtype_apply, IsSl2Triple.h_eq_coroot, map_smul
-- 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
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
rwa₁ rwa₂ rwa₃ rwa₄ : ¬g = 0
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑β : (a : ↥H) → K)) g hg ≠ 0

Tactic:
rwa [ne_eq, LieSubmodule.mk_eq_zero]

Premises used: ne_eq, LieSubmodule.mk_eq_zero
-- 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
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
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
⊢ ∃ (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⟩

Premises used: Subtype.mk, Iff.mp, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, finrank_eq_one_iff_of_nonzero'
-- 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
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
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
⊢ y = c • g

Tactic:
simpa using hc.symm

Premises used: Eq.symm
-- 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
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
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:
exact ⟨c, by simpa using hc.symm⟩
-- 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
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

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⟩
-- 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
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
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α
⊢ x ∈ sl2SubmoduleOfRoot hα

Tactic:
obtain ⟨x_αneg, hx_αneg, x_h, ⟨y, hy_coroot, rfl⟩, rfl⟩ := mem_sup.mp hx

Premises used: Iff.mp, Submodule.mem_sup, 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
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 α
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α
⊢ HAdd.hAdd (β := L) 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

Premises used: Iff.mp, Submodule.mem_sup, rfl