R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥) ↔
    ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ IsSemisimple R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
rw [isSemisimple_iff_no_solvable_ideals]
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian { x // x ∈ ↑I }
⊢ I = ⊥

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable R { x // x ∈ ↑I }
⊢ I = ⊥
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥) ↔
    ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
constructor <;> intro h₁ I h₂
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsLieAbelian { x // x ∈ ↑I }
⊢ I = ⊥
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian { x // x ∈ ↑I }
⊢ I = ⊥
haveI : IsLieAbelian I := h₂
case mp.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsLieAbelian { x // x ∈ ↑I }
⊢ IsSolvable R { x // x ∈ ↑I }
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsLieAbelian { x // x ∈ ↑I }
⊢ I = ⊥
apply h₁
no goals
case mp.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsLieAbelian { x // x ∈ ↑I }
⊢ IsSolvable R { x // x ∈ ↑I }
exact LieAlgebra.ofAbelianIsSolvable R I
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ I = ⊥
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable R { x // x ∈ ↑I }
⊢ I = ⊥
haveI : IsSolvable R I := h₂
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ derivedAbelianOfIdeal I = ⊥
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ I = ⊥
rw [← abelian_of_solvable_ideal_eq_bot_iff]
case mpr.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ IsLieAbelian { x // x ∈ ↑(derivedAbelianOfIdeal I) }
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ derivedAbelianOfIdeal I = ⊥
apply h₁
no goals
case mpr.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
I : LieIdeal R L
h₂ this : IsSolvable R { x // x ∈ ↑I }
⊢ IsLieAbelian { x // x ∈ ↑(derivedAbelianOfIdeal I) }
exact abelian_derivedAbelianOfIdeal I