theorem small_preimage_of_injective {α : Type uα} {β : Type uβ} (f : α → β) (h : Function.Injective f) (s : Set β) [Small.{u, uβ} ↑s] : Small.{u, uα} ↑(f ⁻¹' s)