no goals
α : Type u_1
β : Type ?u.31833
γ : Type ?u.31836
ι : Type ?u.31839
ι' : Type ?u.31842
r✝ p q : α → α → Prop
s : Set α
r : α → α → Prop
⊢ (Pairwise fun x y => r ↑x ↑y) ↔ Set.Pairwise s r
simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne.def, Subtype.ext_iff, Subtype.coe_mk]