no goals
α : Type u_2
β : Type ?u.17412
γ : Type ?u.17415
ι : Type u_1
ι' : Type ?u.17421
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
s : Set ι
h : InjOn f s
⊢ Set.Pairwise (f '' s) r ↔ Set.Pairwise s (r on f)
simp (config := { contextual := true }) [h.eq_iff, Set.Pairwise]