-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem nilpotencyLength_eq_zero_iff [IsNilpotent L M] :
    nilpotencyLength L M = 0 ↔ Subsingleton M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Tactic:
change sInf s = 0 ↔ _

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Subsingleton M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Tactic:
have hs : s.Nonempty := by
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M
  exact ⟨k, hk⟩

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ sInf s = 0

Tactic:
rw [Nat.sInf_eq_zero]

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Tactic:
let s := {k | lowerCentralSeries ℤ L M k = ⊥}

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = 0 ↔ Subsingleton M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ Subsingleton M

Tactic:
rw [← LieSubmodule.subsingleton_iff ℤ L M, ← subsingleton_iff_bot_eq_top, ←
  lowerCentralSeries_zero, @eq_comm (LieSubmodule ℤ L M)]

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ lowerCentralSeries ℤ L M 0 = ⊥

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ s.Nonempty

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M

Result:
case intro
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k : ℕ
hk : lowerCentralSeries ℤ L M k = ⊥
⊢ s.Nonempty

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
⊢ sInf s = 0 ↔ lowerCentralSeries ℤ L M 0 = ⊥

Tactic:
refine ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => ?_⟩

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : s.Nonempty
h : lowerCentralSeries ℤ L M 0 = ⊥
⊢ sInf s = 0

Proof state:
case intro
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k : ℕ
hk : lowerCentralSeries ℤ L M k = ⊥
⊢ s.Nonempty

Tactic:
exact ⟨k, hk⟩

Result:
no goals