-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedLength_zero (I : LieIdeal R L) [IsSolvable I] :
    derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Tactic:
let s := { k | derivedSeriesOfIdeal R L k I = ⊥ }

Result:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Proof state:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeriesOfIdeal R L k I = ⊥
⊢ k ∈ s

Tactic:
exact hk

Result:
no goals

Proof state:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R (↥I) k = ⊥
⊢ k ∈ s

Tactic:
rw [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk

Result:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeriesOfIdeal R L k I = ⊥
⊢ k ∈ s

Proof state:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R (↥I) k = ⊥
⊢ s ≠ ∅

Tactic:
refine Set.Nonempty.ne_empty ⟨k, ?_⟩

Result:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R (↥I) k = ⊥
⊢ k ∈ s

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ I = ⊥

Tactic:
have hne : s ≠ ∅ := by
  obtain ⟨k, hk⟩ := IsSolvable.solvable R I
  refine Set.Nonempty.ne_empty ⟨k, ?_⟩
  rw [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk; exact hk

Result:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
hne : s ≠ ∅
⊢ sInf s = 0 ↔ I = ⊥

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
hne : s ≠ ∅
⊢ sInf s = 0 ↔ I = ⊥

Tactic:
simp [s, hne]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s ≠ ∅

Tactic:
obtain ⟨k, hk⟩ := IsSolvable.solvable R I

Result:
case intro
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : derivedSeries R (↥I) k = ⊥
⊢ s ≠ ∅

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Tactic:
change sInf s = 0 ↔ _

Result:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ I = ⊥