-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem nilpotencyLength_eq_succ_iff (k : ℕ) :
    nilpotencyLength L M = k + 1 ↔
      lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

Proof state:
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✝ k : ℕ
⊢ lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥

Tactic:
simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

Result:
no goals

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

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

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries ℤ L M k₁ = ⊥)

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : lowerCentralSeries ℤ L M k₁ = ⊥
⊢ k₂ ∈ s

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := by
  rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries ℤ L M k₁ = ⊥)
  exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : lowerCentralSeries ℤ L M k₁ = ⊥
⊢ k₂ ∈ s

Tactic:
exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)

Result:
no goals

Proof state:
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 : ℕ
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

Tactic:
have aux (k : ℕ) : lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥ := by
  simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries ℤ L M (k + 1) = ⊥ ∧ ¬lowerCentralSeries ℤ L M k = ⊥

Tactic:
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
exact Nat.sInf_upward_closed_eq_succ_iff hs k

Result:
no goals

Proof state:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

Tactic:
rw [aux, ne_eq, aux]

Result:
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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries ℤ L M (k + 1) = ⊥ ∧ ¬lowerCentralSeries ℤ L M k = ⊥