chore(Analysis/Normed/Group/Uniform): fix statement from leanprover-community#35247 (leanprover-community#35264)

PR leanprover-community#35247 (merged just an hour ago) introduced a new declaration, but the name wasn't quite right (should be `mul_le_norm` in analogy to `le_mul_norm` above),  and the explicit `f` argument should be implicit since the lemma is an `iff`.

I can add deprecations if desired, although given that the previous PR was merged just now, I think it's probably not necessary.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -154,8 +154,8 @@ theorem AntilipschitzWith.le_mul_norm' {f : E → F} {K : ℝ≥0} (h : Antilips
     (hf : f 1 = 1) (x) : ‖x‖ ≤ K * ‖f x‖ := by
   simpa only [dist_one_right, hf] using h.le_mul_dist x 1
 
-@[to_additive antilipschitzWith_iff_exists_mul_le_mul]
-theorem antilipschitzWith_iff_exists_mul_le_mul' [MonoidHomClass 𝓕 E F] (f : 𝓕) :
+@[to_additive antilipschitzWith_iff_exists_mul_le_norm]
+theorem antilipschitzWith_iff_exists_mul_le_norm' [MonoidHomClass 𝓕 E F] {f : 𝓕} :
     (∃ K, AntilipschitzWith K f) ↔ ∃ c > 0, ∀ x, c * ‖x‖ ≤ ‖f x‖ := by
   refine ⟨fun ⟨K, hK⟩ ↦ ⟨(K + 1)⁻¹, by positivity, fun x ↦ ?_⟩, fun ⟨c, hc0, hc⟩ ↦
     ⟨⟨c⁻¹, by positivity⟩, MonoidHomClass.antilipschitz_of_bound f fun x ↦ ?_⟩⟩

Mathlib/Topology/MetricSpace/Antilipschitz.lean

@@ -33,7 +33,7 @@ variable {α β γ : Type*}
 
 /-- We say that `f : α → β` is `AntilipschitzWith K` if for any two points `x`, `y` we have
 `edist x y ≤ K * edist (f x) (f y)`. This can also be used as a predicate for bounded below
-linear operators, see `antilipschitzWith_iff_exists_mul_le_mul`. -/
+linear operators, see `antilipschitzWith_iff_exists_mul_le_norm`. -/
 def AntilipschitzWith [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) (f : α → β) :=
   ∀ x y, edist x y ≤ K * edist (f x) (f y)