Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
set S : Set (Set α) := { J : Set α | IsIdeal J ∧ I ≤ J ∧ Disjoint (F : Set α) J }
  -- Then I is in S...
  have IinS : ↑I ∈ S := ⟨Order.Ideal.isIdeal I, by trivial⟩
  -- ...and S contains upper bounds for any non-empty chains.
  have chainub : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub := by
    intro c hcS hcC hcNe
    use sUnion c
    refine ⟨?_, fun s hs ↦ le_sSup hs⟩
    simp only [mem_ofPred_eq, disjoint_sUnion_right, S]
    let ⟨J, hJ⟩ := hcNe
    refine ⟨Order.isIdeal_sUnion_of_isChain (fun _ hJ ↦ (hcS hJ).1) hcC hcNe,
            ⟨le_trans (hcS hJ).2.1 (le_sSup hJ), fun J hJ ↦ (hcS hJ).2.2⟩⟩
  -- Thus, by Zorn's lemma, we can pick a maximal ideal J in S.
  obtain ⟨Jset, _, hmax⟩ := zorn_subset_nonempty S chainub I IinS
  obtain ⟨Jidl, IJ, JF⟩ := hmax.prop
  set J := IsIdeal.toIdeal Jidl
  use J
  have IJ' : I ≤ J := IJ
  clear chainub IinS
  -- By construction, J contains I and is disjoint from F. It remains to prove that J is prime.
  refine ⟨?_, ⟨IJ, JF⟩⟩
  -- First note that J is proper: ⊤ ∈ F so ⊤ ∉ J because F and J are disjoint.
  have Jpr : IsProper J := isProper_of_notMem (Set.disjoint_left.1 JF F.nonempty.some_mem)
  -- Suppose that a₁ ∉ J, a₂ ∉ J. We need to prove that a₁ ⊔ a₂ ∉ J.
  rw [isPrime_iff_mem_or_mem]
  intro a₁ a₂
  contrapose!
  intro ⟨ha₁, ha₂⟩
  -- Consider the ideals J₁, J₂ generated by J ∪ {a₁} and J ∪ {a₂}, respectively.
  let J₁ := J ⊔ principal a₁
  let J₂ := J ⊔ principal a₂
  -- For each i, Jᵢ is an ideal that contains aᵢ, and is not equal to J.
  have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
  have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
  have J₁J : ↑J₁ ≠ Jset := ne_of_mem_of_not_mem' a₁J₁ ha₁
  have J₂J : ↑J₂ ≠ Jset := ne_of_mem_of_not_mem' a₂J₂ ha₂
  -- Therefore, since J is maximal, we must have Jᵢ ∉ S.
  have J₁S : ↑J₁ ∉ S := fun h => J₁J (hmax.eq_of_le h (le_sup_left : J ≤ J₁)).symm
  have J₂S : ↑J₂ ∉ S := fun h => J₂J (hmax.eq_of_le h (le_sup_left : J ≤ J₂)).symm
  -- Since Jᵢ is an ideal that contains I, we have that Jᵢ is not disjoint from F.
  have J₁F : ¬ (Disjoint (F : Set α) J₁) := by
    intro hdis
    apply J₁S
    simp only [mem_ofPred_eq, SetLike.coe_subset_coe, S]
    exact ⟨J₁.isIdeal, le_trans IJ' le_sup_left, hdis⟩
  have J₂F : ¬ (Disjoint (F : Set α) J₂) := by
    intro hdis
    apply J₂S
    simp only [mem_ofPred_eq, SetLike.coe_subset_coe, S]
    exact ⟨J₂.isIdeal, le_trans IJ' le_sup_left, hdis⟩
  -- Thus, pick cᵢ ∈ F ∩ Jᵢ.
  let ⟨c₁, ⟨c₁F, c₁J₁⟩⟩ := Set.not_disjoint_iff.1 J₁F
  let ⟨c₂, ⟨c₂F, c₂J₂⟩⟩ := Set.not_disjoint_iff.1 J₂F
  -- Using the definition of Jᵢ, we can pick bᵢ ∈ J such that cᵢ ≤ bᵢ ⊔ aᵢ.
  let ⟨b₁, ⟨b₁J, cba₁⟩⟩ := (Lattice.mem_ideal_sup_principal a₁ c₁ J).1 c₁J₁
  let ⟨b₂, ⟨b₂J, cba₂⟩⟩ := (Lattice.mem_ideal_sup_principal a₂ c₂ J).1 c₂J₂
  -- Since J is an ideal, we have b := b₁ ⊔ b₂ ∈ J.
  let b := b₁ ⊔ b₂
  have bJ : b ∈ J := sup_mem b₁J b₂J
  -- We now prove a key inequality, using crucially that the lattice is distributive.
  have ineq : c₁ ⊓ c₂ ≤ b ⊔ (a₁ ⊓ a₂) :=
  calc
    c₁ ⊓ c₂ ≤ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) := inf_le_inf cba₁ cba₂
    _       ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂) := by gcongr; exacts [le_sup_left, le_sup_right]
    _       = b ⊔ (a₁ ⊓ a₂) := (sup_inf_left b a₁ a₂).symm
  -- Note that c₁ ⊓ c₂ ∈ F, since c₁ and c₂ are both in F and F is a filter.
  -- Since F is an upper set, it now follows that b ⊔ (a₁ ⊓ a₂) ∈ F.
  have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F := PFilter.mem_of_le ineq (PFilter.inf_mem c₁F c₂F)
  -- Now, if we would have a₁ ⊓ a₂ ∈ J, then, since J is an ideal and b ∈ J, we would also get
  -- b ⊔ (a₁ ⊓ a₂) ∈ J. But this contradicts that J is disjoint from F.
  contrapose JF with ha₁a₂
  rw [Set.not_disjoint_iff]
  use b ⊔ (a₁ ⊓ a₂)
  exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩

Goal state after: