ext n
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) = Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ n ∈ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) ↔ n ∈ Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))