-- Mathlib/Algebra/Lie/Solvable.lean
theorem abelian_of_solvable_ideal_eq_bot_iff (I : LieIdeal R L) [h : IsSolvable I] :
    derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ derivedSeriesOfIdeal R L k ⊥ = ⊥

Tactic:
apply derivedSeries_of_bot_eq_bot

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ False

Tactic:
apply h₂

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ derivedSeriesOfIdeal R L k ⊥ = ⊥

Proof state:
case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = k✝.succ
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥

Tactic:
rename_i k h

Result:
case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

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

Tactic:
dsimp only [derivedAbelianOfIdeal]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
⊢ (match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I) =
      ⊥ ↔
    I = ⊥

Proof state:
case h_2.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Tactic:
have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot

Result:
case h_2.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
h₃ : I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Proof state:
case h_2.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
h₃ : I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Tactic:
simp only [h₂, h₃]

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
h : IsSolvable ↥I
⊢ (match derivedLengthOfIdeal R L I with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I) =
      ⊥ ↔
    I = ⊥

Tactic:
split

Result:
case h_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = 0
⊢ ⊥ = ⊥ ↔ I = ⊥

case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ k✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = k✝.succ
⊢ derivedSeriesOfIdeal R L k✝ I = ⊥ ↔ I = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ I ≠ ⊥

Tactic:
rintro rfl

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ k : ℕ
h✝ : IsSolvable ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : derivedSeriesOfIdeal R L k ⊥ ≠ ⊥
⊢ False

Proof state:
case h_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Tactic:
obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h

Result:
case h_2.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : IsSolvable ↥I
x✝ k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left✝ : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥

Proof state:
case h_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
x✝ : ℕ
heq✝ : derivedLengthOfIdeal R L I = 0
⊢ ⊥ = ⊥ ↔ I = ⊥

Tactic:
simp_all only [derivedLength_zero]

Result:
no goals