-- Mathlib/Algebra/Lie/Weights/Linear.lean
/-- See `LieModule.exists_nontrivial_weightSpace_of_isSolvable` for the variant that
only assumes that `L` is solvable but additionally requires `k` to be of characteristic zero. -/
lemma exists_nontrivial_weightSpace_of_isNilpotent [Field k] [LieAlgebra k L] [Module k M]
    [Module.Finite k M] [LieModule k L M] [LinearWeights k L M]
    [IsTriangularizable k L M] [Nontrivial M] :
    ∃ χ : Module.Dual k L, Nontrivial (weightSpace M χ)

Proof state:
case intro.intro.intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ ∃ χ x, ∃ (_ : x ∈ weightSpace M ⇑χ), ¬x = 0

Tactic:
exact ⟨χ.toLinear, m, by simpa [mem_weightSpace], hm₀⟩

Result:
no goals

Proof state:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : 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

Result:
no goals

Proof state:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
contra : ¬Nonempty (Weight k L M)
⊢ False

Tactic:
rw [not_nonempty_iff] at contra

Result:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
contra : IsEmpty (Weight k L M)
⊢ False

Proof state:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

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

Result:
case intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

Proof state:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ Nonempty (Weight k L M)

Tactic:
by_contra contra

Result:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
contra : ¬Nonempty (Weight k L M)
⊢ False

Proof state:
case intro.intro.intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

Tactic:
simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, Weight.coe_coe, ne_eq,
  not_forall, Classical.not_imp]

Result:
case intro.intro.intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ ∃ χ x, ∃ (_ : x ∈ weightSpace M ⇑χ), ¬x = 0

Proof state:
case intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

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

Result:
case intro.intro.intro
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

Proof state:
k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ m ∈ weightSpace M ⇑(Weight.toLinear k L M χ)

Tactic:
simpa [mem_weightSpace]

Result:
no goals