P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsProper I ∧ IsPFilter (↑Iᶜ)
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPrime I
rw [IsPrime_iff]
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑Iᶜ)
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsProper I ∧ IsPFilter (↑Iᶜ)
use ‹_›
case refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ Set.Nonempty (↑Iᶜ)

case refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x x_1 => x ≥ x_1) (↑Iᶜ)

case refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ ↑Iᶜ → y ∈ ↑Iᶜ
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑Iᶜ)
refine .of_def ?_ ?_ ?_
no goals
case refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ Set.Nonempty (↑Iᶜ)
exact Set.nonempty_compl.2 (I.IsProper_iff.1 ‹_›)
case refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ ↑Iᶜ
y : P
hy : y ∈ ↑Iᶜ
⊢ ∃ z, z ∈ ↑Iᶜ ∧ (fun x x_1 => x ≥ x_1) x z ∧ (fun x x_1 => x ≥ x_1) y z
case refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x x_1 => x ≥ x_1) (↑Iᶜ)
intro x hx y hy
no goals
case refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ ↑Iᶜ
y : P
hy : y ∈ ↑Iᶜ
⊢ ∃ z, z ∈ ↑Iᶜ ∧ (fun x x_1 => x ≥ x_1) x z ∧ (fun x x_1 => x ≥ x_1) y z
exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩
no goals
case refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ ↑Iᶜ → y ∈ ↑Iᶜ
exact @mem_compl_of_ge _ _ _