-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem exists_le_prime_disjoint (S : Submonoid α) (disjoint : Disjoint (I : Set α) S) :
    ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ Disjoint (p : Set α) S

Proof state:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : Nonempty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩

Result:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
⊢ x ∉ ↑S

Proof state:
case refine_1.inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : IsEmpty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩

Result:
no goals

Proof state:
case refine_1
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Tactic:
cases isEmpty_or_nonempty c

Result:
case refine_1.inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : IsEmpty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : Nonempty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Proof state:
case refine_2
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
p : Ideal α
hIp : I ≤ p
hp : Maximal (fun x => x ∈ {p | Disjoint ↑p ↑S}) p
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
  (fun c hc hc' x hx ↦ ?_) I disjoint

Result:
case refine_2
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
p : Ideal α
hIp : I ≤ p
hp : Maximal (fun x => x ∈ {p | Disjoint ↑p ↑S}) p
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

case refine_1
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Proof state:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
⊢ x ∉ ↑S

Tactic:
have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)

Result:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
p : { a // a ∈ c }
hp : x ∈ ↑p
⊢ x ∉ ↑S

Proof state:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 => x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
p : { a // a ∈ c }
hp : x ∈ ↑p
⊢ x ∉ ↑S

Tactic:
exact Set.disjoint_left.mp (hc p.2) hp

Result:
no goals