Lean refactor: make an application lemma take the sieve constant as a hypothesis

When a corollary (e.g. Linnik's squares bound from the arithmetic large sieve) is proved against one specific sieve inequality, and a better constant later appears in a file that imports the corollary's file, you cannot reuse the proof without an import cycle. The fix that worked: state the corollary as foo_of (C : ℝ) (hC : ∀ Ω, admissible Ω → |A| * L(Ω) ≤ C) : |A| ≤ 2*C/(π(Q)+1), replacing the internal have := sieve_lemma ... by hC _ hΩ. The old theorem then becomes a one-line term foo_of ... _ (fun Ω hΩ => old_sieve ...) with an unchanged signature, so downstream users are unaffected. The improved version, foo_of ... (fun Ω hΩ => new_sieve ...), lives in the newer file. The numeric constant is inferred from hC via _.