-- Mathlib/Order/PrimeSeparator.lean
theorem prime_ideal_of_disjoint_filter_ideal (hFI : Disjoint (F : Set α) (I : Set α)) :
    ∃ J : Ideal α, (IsPrime J) ∧ I ≤ J ∧ Disjoint (F : Set α) J

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
chainub : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
obtain ⟨Jset, _, hmax⟩ := zorn_subset_nonempty S chainub I IinS

Result:
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
chainub : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Proof state:
case h
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
refine ⟨?_, ⟨IJ, JF⟩⟩

Result:
case h
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
⊢ J.IsPrime

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
have IinS : ↑I ∈ S := by
  refine ⟨Order.Ideal.isIdeal I, by trivial⟩

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
hdis : Disjoint ↑F ↑J₁
⊢ IsIdeal ↑J₁ ∧ I ≤ J₁ ∧ Disjoint ↑F ↑J₁

Tactic:
exact ⟨J₁.isIdeal, le_trans IJ' le_sup_left, hdis⟩

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ b ⊔ a₁ ⊓ a₂ ∈ ↑F ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset

Tactic:
exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self

Result:
case h
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
⊢ a₁ ⊓ a₂ ∉ J

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
⊢ ¬Disjoint ↑F ↑J₁

Tactic:
intro hdis

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x => x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
hdis : Disjoint ↑F ↑J₁
⊢ False