∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α} {g : ι' → ι}
  {s : Set ι'}, Set.InjOn g s → ((g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g))