no goals
α : Type u_2
β : Type u_1
s✝ t : Set α
a b x y : α
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ ncard (f ⁻¹' s) = ncard s
rw [← ncard_image_ofInjective _ H, image_preimage_eq_iff.mpr hs]