case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I ≤ maximalIdeal R

case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson I
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I = maximalIdeal R
apply le_antisymm
no goals
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I ≤ maximalIdeal R
exact sInf_le ⟨LocalRing.le_maximalIdeal h, LocalRing.maximalIdeal.isMaximal R⟩
no goals
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson I
exact le_sInf fun J (hJ : I ≤ J ∧ J.IsMaximal) => le_of_eq (LocalRing.eq_maximalIdeal hJ.2).symm