P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.Fᶜ)
rw [IF.compl_F_eq_I]
no goals
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
exact IF.I.isIdeal