norm_cast
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ ↑d ≤ ↑d2 ^ 2
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
d1 d2 : ℕ
h : d = d1.lcm d2
hle : d1 ≤ d2
hyp : ↑d2 ^ 2 ≤ y
⊢ d ≤ d2 ^ 2