case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IsProper IF.I
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsProper IF.I
cases' IF.F.nonempty with w h
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ ¬w ∈ IF.I
case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IsProper IF.I
apply isProper_of_not_mem (_ : w ∉ IF.I)
no goals
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ ¬w ∈ IF.I
rwa [← IF.compl_I_eq_F] at h