case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : Ideal.IsMaximal M
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
no goals
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : Ideal.IsMaximal M
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
rwa [← eq_maximalIdeal hM1]