simp only [Finset.mem_filter, Finset.mem_Ioc, Nat.ceil_le, Finset.mem_image,
  Nat.le_floor_iff (show 0 ≤ x+y by linarith)]
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))
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n