P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter ↑IF.F
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter (↑IF.Iᶜ)
rw [IF.compl_I_eq_F]
no goals
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter ↑IF.F
exact IF.F.isPFilter