-- 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:
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₂ : α
⊢ a₁ ∉ J ∧ a₂ ∉ J → a₁ ⊓ a₂ ∉ J

Tactic:
intro ⟨ha₁, ha₂⟩

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
⊢ a₁ ⊓ a₂ ∉ J

Proof state:
case intro.intro.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
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
use J

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}
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
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
⊢ 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
Jpr : J.IsProper
⊢ ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
intros a₁ a₂

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₂ : α
⊢ a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J

Proof state:
case intro.intro.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
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
set J := IsIdeal.toIdeal Jidl

Result:
case intro.intro.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
Jidl : IsIdeal Jset
IJ : ↑I ≤ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
⊢ ∃ 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₁
⊢ ↑J₁ ∈ S

Tactic:
simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]

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₁
⊢ IsIdeal ↑J₁ ∧ 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₁
⊢ False

Tactic:
apply J₁S

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₁
⊢ ↑J₁ ∈ S

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}
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
refine ⟨?_, fun s hs ↦ le_sSup hs⟩

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}
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S