[GOAL]
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 = ⊥
[PROOFSTEP]
rw [isSemisimple_iff_no_solvable_ideals]
[GOAL]
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 = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
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 = ⊥
[PROOFSTEP]
intro h₁ I h₂
[GOAL]
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥) →
    ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → I = ⊥
[PROOFSTEP]
intro h₁ I h₂
[GOAL]
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 = ⊥
[PROOFSTEP]
haveI : IsLieAbelian I := h₂
[GOAL]
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 = ⊥
[PROOFSTEP]
apply h₁
[GOAL]
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 }
[PROOFSTEP]
exact LieAlgebra.ofAbelianIsSolvable R I
[GOAL]
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 = ⊥
[PROOFSTEP]
haveI : IsSolvable R I := h₂
[GOAL]
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 = ⊥
[PROOFSTEP]
rw [← abelian_of_solvable_ideal_eq_bot_iff]
[GOAL]
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 = ⊥
[PROOFSTEP]
apply h₁
[GOAL]
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) }
[PROOFSTEP]
exact abelian_derivedAbelianOfIdeal I
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSemisimple R L
⊢ center R L = ⊥
[PROOFSTEP]
rw [isSemisimple_iff_no_abelian_ideals] at h 
[GOAL]
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 = ⊥
⊢ center R L = ⊥
[PROOFSTEP]
apply h
[GOAL]
case 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 = ⊥
⊢ IsLieAbelian { x // x ∈ ↑(center R L) }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
⊢ IsSemisimple R L
[PROOFSTEP]
rw [isSemisimple_iff_no_abelian_ideals]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
⊢ ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
[PROOFSTEP]
intro I hI
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian { x // x ∈ ↑I }
⊢ I = ⊥
[PROOFSTEP]
obtain @⟨⟨h₁⟩, h₂⟩ := id h
[GOAL]
case mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian { x // x ∈ ↑I }
h₂ : ¬IsLieAbelian L
h₁ : ∀ (N : LieSubmodule R L L), N ≠ ⊥ → N = ⊤
⊢ I = ⊥
[PROOFSTEP]
by_contra contra
[GOAL]
case mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian { x // x ∈ ↑I }
h₂ : ¬IsLieAbelian L
h₁ : ∀ (N : LieSubmodule R L L), N ≠ ⊥ → N = ⊤
contra : ¬I = ⊥
⊢ False
[PROOFSTEP]
rw [h₁ I contra, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI 
[GOAL]
case mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian L
h₂ : ¬IsLieAbelian L
h₁ : ∀ (N : LieSubmodule R L L), N ≠ ⊥ → N = ⊤
contra : ¬I = ⊥
⊢ False
[PROOFSTEP]
exact h₂ hI
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
h : IsLieAbelian L
⊢ Subsingleton L
[PROOFSTEP]
rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot_of_semisimple] at h 
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
h : ⊥ = ⊤
⊢ Subsingleton L
[PROOFSTEP]
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ IsLieAbelian { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
rw [IsSemisimple.semisimple]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ IsLieAbelian { x // x ∈ ↑⊥ }
[PROOFSTEP]
exact isLieAbelian_bot R L
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian { x // x ∈ ↑(radical R L) } ↔
    ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → IsLieAbelian { x // x ∈ ↑I }
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian { x // x ∈ ↑(radical R L) } →
    ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → IsLieAbelian { x // x ∈ ↑I }
[PROOFSTEP]
rintro h₁ I h₂
[GOAL]
case mp
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
h₁ : IsLieAbelian { x // x ∈ ↑(radical R L) }
I : LieIdeal R L
h₂ : IsSolvable R { x // x ∈ ↑I }
⊢ IsLieAbelian { x // x ∈ ↑I }
[PROOFSTEP]
rw [LieIdeal.solvable_iff_le_radical] at h₂ 
[GOAL]
case mp
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
h₁ : IsLieAbelian { x // x ∈ ↑(radical R L) }
I : LieIdeal R L
h₂ : I ≤ radical R L
⊢ IsLieAbelian { x // x ∈ ↑I }
[PROOFSTEP]
exact (LieIdeal.homOfLe_injective h₂).isLieAbelian h₁
[GOAL]
case mpr
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ (∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → IsLieAbelian { x // x ∈ ↑I }) →
    IsLieAbelian { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
h : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → IsLieAbelian { x // x ∈ ↑I }
⊢ IsLieAbelian { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
apply h
[GOAL]
case mpr.a
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
h : ∀ (I : LieIdeal R L), IsSolvable R { x // x ∈ ↑I } → IsLieAbelian { x // x ∈ ↑I }
⊢ IsSolvable R { x // x ∈ ↑(radical R L) }
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ LieHom.ker (ad R L) = ⊥
[PROOFSTEP]
simp
