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 }

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) }
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 }
constructor
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 }
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 }
rintro h₁ I h₂
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 }
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 }
rw [LieIdeal.solvable_iff_le_radical] at h₂
no goals
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 }
exact (LieIdeal.homOfLe_injective h₂).isLieAbelian h₁
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) }
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) }
intro h
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) }
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) }
apply h
no goals
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) }
infer_instance