-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem sInf_isPrime_of_isChain {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (· ≤ ·) s)
    (H : ∀ p ∈ s, Ideal.IsPrime p) : (sInf s).IsPrime :=
  ⟨fun e =>
    let ⟨x, hx⟩ := hs
    (H x hx).ne_top (eq_top_iff.mpr (e.symm.trans_le (sInf_le hx))),
    fun e =>
    or_iff_not_imp_left.mpr fun hx => by
      rw [Ideal.mem_sInf] at hx e ⊢
      push_neg at hx
      obtain ⟨I, hI, hI'⟩ := hx
      intro J hJ
      rcases hs'.total hI hJ with h | h
      · exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')
      · exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x⟩

Proof state:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ∃ I ∈ s, x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
obtain ⟨I, hI, hI'⟩ := hx

Result:
case intro.intro
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : x✝ * y✝ ∈ sInf s
hx : x✝ ∉ sInf s
⊢ y✝ ∈ sInf s

Tactic:
rw [Ideal.mem_sInf] at hx e ⊢

Result:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Proof state:
case intro.intro.inr
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
h : J ≤ I
⊢ y✝ ∈ J

Tactic:
exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
push_neg at hx

Result:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ∃ I ∈ s, x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Proof state:
case intro.intro
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
intro J hJ

Result:
case intro.intro
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
⊢ y✝ ∈ J

Proof state:
case intro.intro
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
⊢ y✝ ∈ J

Tactic:
rcases hs'.total hI hJ with h | h

Result:
case intro.intro.inl
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y✝ ∈ J

case intro.intro.inr
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
h : J ≤ I
⊢ y✝ ∈ J

Proof state:
case intro.intro.inl
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 => x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y✝ ∈ J

Tactic:
exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')

Result:
no goals