Interaction of equivalences with Pairwise

theorem EmbeddingLike.pairwise_comp {X : Type u_1} {Y : Type u_2} {F : Sort u_3} [FunLike F Y X] [EmbeddingLike F Y X] (f : F) {p : X → X → Prop} (h : Pairwise p) : Pairwise (p on ⇑f)

theorem EquivLike.pairwise_comp_iff {X : Type u_1} {Y : Type u_2} {F : Sort u_3} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (p on ⇑f) ↔ Pairwise p