R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
⊢ (match nilpotencyLength R L M with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
⊢ Nontrivial { x // x ∈ ↑(lowerCentralSeriesLast R L M) }
rw [LieSubmodule.nontrivial_iff_ne_bot, lowerCentralSeriesLast]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : nilpotencyLength R L M = Nat.zero
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥

case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : nilpotencyLength R L M = Nat.succ n✝
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
⊢ (match nilpotencyLength R L M with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
cases h : nilpotencyLength R L M
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : ¬Nontrivial M
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : nilpotencyLength R L M = Nat.zero
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
rw [nilpotencyLength_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h
no goals
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : ¬Nontrivial M
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
contradiction
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : nilpotencyLength R L M = Nat.succ n✝
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
rw [nilpotencyLength_eq_succ_iff] at h
no goals
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
exact h.2