rw [Finset.card_image_of_injective _ <| mul_left_injective₀ hd]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))).card = b / d - a / d
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.Ioc (a / d) (b / d)).card = b / d - a / d