awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
x : L
⊢ (↑⁅x,
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
      M) =
    0

Tactic:
have := hm₁ x
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
x : L
this :
  (↑⁅x,
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
      M) =
    0
rwa :
  ∀
    (this :
      ⁅x,
            (↑(Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                  property) :
              M)⁆ -
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R)
            (↑(Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                  property) :
              M) =
        0),
    ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      ⁅x,
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                property) :
            M)⁆ =
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R)
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                property) :
            M)),
    ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
⊢ ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m

Tactic:
rwa [coe_lie_shiftedGenWeightSpace_apply, sub_eq_zero] at this

Premises used: sub_eq_zero, LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
by_contra! : ∀ (contra : IsEmpty (Weight k L M)), False
⊢ Nonempty (Weight k L M)

Tactic:
by_contra! contra
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
contra : IsEmpty (Weight k L M)
⊢ False

Tactic:
simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M

Premises used: LieModule.iSup_genWeightSpace_eq_top', bot_ne_top, iSup_of_empty
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
obtain : ∀ (χ : Weight k L M), ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))

Tactic:
obtain ⟨χ⟩ : Nonempty (Weight k L M) := by
    by_contra! contra
    simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M

Premises used: Nonempty, LieModule.Weight
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
obtain :
  ∀ (m : M) (hm₀ : m ≠ 0) (hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m),
    ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))

Tactic:
obtain ⟨m, hm₀, hm⟩ := exists_forall_lie_eq_smul k L M χ

Premises used: LieModule.exists_forall_lie_eq_smul
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m
simp :
  ∃ (χ : Module.Dual k L) (x : M) (_ : Membership.mem (γ := LieSubmodule k L M) (weightSpace M (⇑χ : (a : L) → k)) x),
    ¬x = 0
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))

Tactic:
simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, ne_eq, not_forall]

Premises used: ne_eq, LieSubmodule.nontrivial_iff_ne_bot, Classical.not_forall, LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m
⊢ Membership.mem (γ := LieSubmodule k L M) (weightSpace M (⇑(Weight.toLinear k L M χ) : (a : L) → k)) m

Tactic:
simpa [mem_weightSpace]

Premises used: LieModule.mem_weightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m
⊢ ∃ (χ : Module.Dual k L) (x : M) (_ : Membership.mem (γ := LieSubmodule k L M) (weightSpace M (⇑χ : (a : L) → k)) x),
    ¬x = 0

Tactic:
exact ⟨χ.toLinear, m, by simpa [mem_weightSpace], hm₀⟩
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
pos : ∀ (hx' : x = 0), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
neg : ∀ (hx' : ¬x = 0), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆

Tactic:
by_cases hx' : x = 0
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : x = 0
⊢ HSMul.hSMul (α := ℕ) 0 x = ⁅coroot α, x⁆

Tactic:
simp [hx']
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : x = 0
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆

Tactic:
exact ⟨0, by simp [hx']⟩
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
neg :
  ∀ (h e f : L) (isSl2 : IsSl2Triple h e f) (he : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆

Tactic:
obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
h e f : L
isSl2 : IsSl2Triple h e f
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ IsSl2Triple (↑(coroot α) : L) e f

Tactic:
obtain rfl := isSl2.h_eq_coroot hα he hf

Premises used: IsSl2Triple.h_eq_coroot, rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := ↥H → K) (⇑α : (a : ↥H) → K) (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⁅e, x⁆
rw : ⁅(↑(coroot α) : L), x⁆ = ⁅coroot α, x⁆
⊢ ⁅(↑(coroot α) : L), x⁆ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x

Tactic:
rw [← lie_eq_smul_of_mem_rootSpace hx]

Premises used: LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := ↥H → K) (⇑α : (a : ↥H) → K) (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⁅e, x⁆
⊢ ⁅(↑(coroot α) : L), x⁆ = ⁅coroot α, x⁆

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := ↥H → K) (⇑α : (a : ↥H) → K) (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⁅e, x⁆
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅e, x⁆), ⁅e, x⁆ = 0
⊢ ⁅e, x⁆ = 0

Tactic:
rwa [genWeightSpace_add_chainTop α β hα] at this

Premises used: DFunLike.coe, LieModule.genWeightSpace_add_chainTop
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
⊢ IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)

Tactic:
have : isSl2.HasPrimitiveVectorWith x (chainTop α β (coroot α)) :=
    have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
    ⟨hx', by rw [← lie_eq_smul_of_mem_rootSpace hx]; rfl,
      by rwa [genWeightSpace_add_chainTop α β hα] at this⟩
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
neg :
  ∀ (μ : ℕ)
    (hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)),
    ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆

Tactic:
obtain ⟨μ, hμ⟩ := this.exists_nat

Premises used: IsSl2Triple.HasPrimitiveVectorWith.exists_nat
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
μ : ℕ
hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑μ : K) x = ⁅coroot α, x⁆
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x =
    ⁅coroot α, x⁆
rw₂ rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x
⊢ μ • x = ⁅coroot α, x⁆

Tactic:
rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]

Premises used: LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
μ : ℕ
hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆

Tactic:
exact ⟨μ, by rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]⟩
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsZero
⊢ chainLength α β = 0

Tactic:
dif_pos hα

Premises used: dif_pos, LieAlgebra.IsKilling.chainLength
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), chainLength α β • x = ⁅coroot α, x⁆
neg : ∀ (hα : ¬α.IsZero), chainLength α β • x = ⁅coroot α, x⁆
⊢ chainLength α β • x = ⁅coroot α, x⁆

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : α.IsZero
pos : chainLength α β • x = Bracket.bracket (L := ↥H) 0 x
pos₁ : HSMul.hSMul (α := ℕ) 0 x = Bracket.bracket (L := ↥H) 0 x
pos₂ : 0 = Bracket.bracket (L := ↥H) 0 x
pos₃ pos₄ : Eq.{u_2 + 1} (α := L) 0 0
⊢ chainLength α β • x = ⁅coroot α, x⁆

Tactic:
rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]

Premises used: Iff.mpr, zero_smul, zero_lie, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.chainLength_of_isZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : ¬α.IsZero
x' : L :=
  ⋯.choose (p := fun (x : L) ↦
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x ∧
      x ≠ 0)
⊢ x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ∧ x' ≠ 0

Tactic:
have h : x' ∈ rootSpace H (chainTop α β) ∧ x' ≠ 0 :=
    (chainTop α β).exists_ne_zero.choose_spec
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : ¬α.IsZero
x' : L :=
  ⋯.choose (p := fun (x : L) ↦
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x ∧
      x ≠ 0)
h : x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ∧ x' ≠ 0
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x' ⋯ ≠ 0

Tactic:
simpa using h.2

Premises used: And.right