case intro.intro.intro.mk
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I, Ideal.IsMaximal I
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ ∃! I, Ideal.IsMaximal I
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤

case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I => Ideal.IsMaximal I) M
⊢ M ≠ ⊥
case intro.intro.intro.mk
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I, Ideal.IsMaximal I
refine' ⟨P, ⟨⟨hPnot_top, _⟩⟩, fun M hM => hPunique _ ⟨_, Ideal.IsMaximal.isPrime hM⟩⟩
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : Ideal.IsMaximal M
⊢ P = M
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤
refine' Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM _
no goals
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : Ideal.IsMaximal M
⊢ P = M
exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal ⊥
⊢ False
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I => Ideal.IsMaximal I) M
⊢ M ≠ ⊥
rintro rfl
no goals
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal ⊥
⊢ False
exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))