Lean: make existential constants uniform by a quantifier swap, keep the old lemma as a wrapper

Lemmas of the form (hA : [w] ≠ ∞) → ∃ C ≠ ∞, ∀ f, ... can't be used when you need one C for a whole family of weights, e.g. all translates w(·+v). The fix that touched least code was a core lemma with the bound as a parameter: {K} (hK : K ≠ ∞) : ∃ C ≠ ∞, ∀ w, hyps w → (∀ f, ∫ T f^p w ≤ K ∫ |f|^p w) → ∀ f, .... In its proof, compute C from K before refine ⟨C, _, fun w hw ... ↦ ?_⟩, and move every w-dependent have/obtain after the intro. The old statement becomes a 5-line wrapper that obtains K from the existing iff lemma and instantiates. Across three files of a chain (majorant → extrapolation → vector-valued), the changes compiled first try and no downstream file needed edits. Remember to lake build the edited upstream module before lake env lean on a dependent file, or the dependent file sees the stale .olean.