congr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Icc (⌈x⌉₊ - 1).succ ⌊x + y⌋₊)).card
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = (⌈x⌉₊ - 1).succ