chore: generalise ENNReal lemmas to WithTop (#17786)

That way, they will also apply to a potential future `ENNRat`.

Author: YaelDillies

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -143,6 +143,14 @@ section Preorder
 
 variable [Preorder α]
 
+@[to_additive]
+lemma mul_left_mono [CovariantClass α α (· * ·) (· ≤ ·)] {a : α} : Monotone (a * ·) :=
+  fun _ _ h ↦ mul_le_mul_left' h _
+
+@[to_additive]
+lemma mul_right_mono [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a : α} : Monotone (· * a) :=
+  fun _ _ h ↦ mul_le_mul_right' h _
+
 @[to_additive (attr := gcongr)]
 theorem mul_lt_mul_of_lt_of_lt [MulLeftStrictMono α]
     [MulRightStrictMono α]
@@ -280,6 +288,14 @@ end PartialOrder
 section LinearOrder
 variable [LinearOrder α] {a b c d : α}
 
+@[to_additive]
+lemma mul_max [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
+    a * max b c = max (a * b) (a * c) := mul_left_mono.map_max
+
+@[to_additive]
+lemma max_mul [CovariantClass α α (swap (· * ·)) (· ≤ ·)] :
+    max a b * c = max (a * c) (b * c) := mul_right_mono.map_max
+
 @[to_additive] lemma min_lt_max_of_mul_lt_mul
     [MulLeftMono α] [MulRightMono α]
     (h : a * b < c * d) : min a b < max c d := by
@@ -1055,38 +1071,36 @@ section Mono
 variable [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β}
 
 @[to_additive const_add]
-theorem Monotone.const_mul' [MulLeftMono α] (hf : Monotone f) (a : α) :
-    Monotone fun x => a * f x := fun _ _ h => mul_le_mul_left' (hf h) a
+theorem Monotone.const_mul' [MulLeftMono α] (hf : Monotone f) (a : α) : Monotone fun x ↦ a * f x :=
+  mul_left_mono.comp hf
 
 @[to_additive const_add]
 theorem MonotoneOn.const_mul' [MulLeftMono α] (hf : MonotoneOn f s) (a : α) :
-    MonotoneOn (fun x => a * f x) s := fun _ hx _ hy h => mul_le_mul_left' (hf hx hy h) a
+    MonotoneOn (fun x => a * f x) s := mul_left_mono.comp_monotoneOn hf
 
 @[to_additive const_add]
-theorem Antitone.const_mul' [MulLeftMono α] (hf : Antitone f) (a : α) :
-    Antitone fun x => a * f x := fun _ _ h => mul_le_mul_left' (hf h) a
+theorem Antitone.const_mul' [MulLeftMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ a * f x :=
+  mul_left_mono.comp_antitone hf
 
 @[to_additive const_add]
 theorem AntitoneOn.const_mul' [MulLeftMono α] (hf : AntitoneOn f s) (a : α) :
-    AntitoneOn (fun x => a * f x) s := fun _ hx _ hy h => mul_le_mul_left' (hf hx hy h) a
+    AntitoneOn (fun x => a * f x) s := mul_left_mono.comp_antitoneOn hf
 
 @[to_additive add_const]
 theorem Monotone.mul_const' [MulRightMono α] (hf : Monotone f) (a : α) :
-    Monotone fun x => f x * a := fun _ _ h => mul_le_mul_right' (hf h) a
+    Monotone fun x => f x * a := mul_right_mono.comp hf
 
 @[to_additive add_const]
-theorem MonotoneOn.mul_const' [MulRightMono α] (hf : MonotoneOn f s)
-    (a : α) :
-    MonotoneOn (fun x => f x * a) s := fun _ hx _ hy h => mul_le_mul_right' (hf hx hy h) a
+theorem MonotoneOn.mul_const' [MulRightMono α] (hf : MonotoneOn f s) (a : α) :
+    MonotoneOn (fun x => f x * a) s := mul_right_mono.comp_monotoneOn hf
 
 @[to_additive add_const]
-theorem Antitone.mul_const' [MulRightMono α] (hf : Antitone f) (a : α) :
-    Antitone fun x => f x * a := fun _ _ h => mul_le_mul_right' (hf h) a
+theorem Antitone.mul_const' [MulRightMono α] (hf : Antitone f) (a : α) : Antitone fun x ↦ f x * a :=
+  mul_right_mono.comp_antitone hf
 
 @[to_additive add_const]
-theorem AntitoneOn.mul_const' [MulRightMono α] (hf : AntitoneOn f s)
-    (a : α) :
-    AntitoneOn (fun x => f x * a) s := fun _ hx _ hy h => mul_le_mul_right' (hf hx hy h) a
+theorem AntitoneOn.mul_const' [MulRightMono α] (hf : AntitoneOn f s) (a : α) :
+    AntitoneOn (fun x => f x * a) s := mul_right_mono.comp_antitoneOn hf
 
 /-- The product of two monotone functions is monotone. -/
 @[to_additive add "The sum of two monotone functions is monotone."]

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -195,6 +195,39 @@ protected def _root_.RingHom.withTopMap {R S : Type*} [CanonicallyOrderedCommSem
     (f : R →+* S) (hf : Function.Injective f) : WithTop R →+* WithTop S :=
   {MonoidWithZeroHom.withTopMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.withTopMap with}
 
+variable [PosMulStrictMono α] {a a₁ a₂ b₁ b₂ : WithTop α}
+
+@[gcongr]
+protected lemma mul_lt_mul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂ := by
+  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
+  lift a₁ to α using ha.lt_top.ne
+  lift b₁ to α using hb.lt_top.ne
+  obtain rfl | ha₂ := eq_or_ne a₂ ⊤
+  · rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
+    exact coe_lt_top _
+  obtain rfl | hb₂ := eq_or_ne b₂ ⊤
+  · rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
+    exact coe_lt_top _
+  lift a₂ to α using ha₂
+  lift b₂ to α using hb₂
+  norm_cast at *
+  obtain rfl | hb₁ := eq_zero_or_pos b₁
+  · rw [mul_zero]
+    exact mul_pos (by simpa [bot_eq_zero] using ha.bot_lt) hb
+  · exact mul_lt_mul ha hb.le hb₁ (zero_le _)
+
+variable [NoZeroDivisors α] [Nontrivial α] {a b : WithTop α}
+
+protected lemma pow_right_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a : WithTop α ↦ a ^ n
+  | 0, h => absurd rfl h
+  | 1, _ => by simpa only [pow_one] using strictMono_id
+  | n + 2, _ => fun x y h ↦ by
+    simp_rw [pow_succ _ (n + 1)]
+    exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h
+
+@[gcongr] protected lemma pow_lt_pow_left (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n :=
+  WithTop.pow_right_strictMono hn hab
+
 end WithTop
 
 namespace WithBot

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -124,7 +124,7 @@ lemma IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm {a : A} (ha : IsSelfAd
 
 theorem IsStarNormal.spectralRadius_eq_nnnorm (a : A) [IsStarNormal a] :
     spectralRadius ℂ a = ‖a‖₊ := by
-  refine (ENNReal.pow_strictMono two_ne_zero).injective ?_
+  refine (ENNReal.pow_right_strictMono two_ne_zero).injective ?_
   have heq :
     (fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
       (fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) := by

Mathlib/Analysis/NormedSpace/ENorm.lean

@@ -151,7 +151,7 @@ noncomputable instance : SemilatticeSup (ENorm 𝕜 V) :=
         map_add_le' := fun _ _ =>
           max_le (le_trans (e₁.map_add_le _ _) <| add_le_add (le_max_left _ _) (le_max_left _ _))
             (le_trans (e₂.map_add_le _ _) <| add_le_add (le_max_right _ _) (le_max_right _ _))
-        map_smul_le' := fun c x => le_of_eq <| by simp only [map_smul, ENNReal.mul_max] }
+        map_smul_le' := fun c x => le_of_eq <| by simp only [map_smul, mul_max] }
     le_sup_left := fun _ _ _ => le_max_left _ _
     le_sup_right := fun _ _ _ => le_max_right _ _
     sup_le := fun _ _ _ h₁ h₂ x => max_le (h₁ x) (h₂ x) }

Mathlib/Data/ENNReal/Inv.lean

@@ -97,15 +97,6 @@ protected theorem div_mul_cancel (h0 : a ≠ 0) (hI : a ≠ ∞) : b / a * a = b
 protected theorem mul_div_cancel' (h0 : a ≠ 0) (hI : a ≠ ∞) : a * (b / a) = b := by
   rw [mul_comm, ENNReal.div_mul_cancel h0 hI]
 
-protected theorem mul_eq_left (ha : a ≠ 0) (h'a : a ≠ ∞) : a * b = a ↔ b = 1 := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, mul_one]⟩
-  have : a * b * a⁻¹ = a * a⁻¹ := by rw [h]
-  rwa [mul_assoc, mul_comm b, ← mul_assoc, ENNReal.mul_inv_cancel ha h'a, one_mul] at this
-
-protected theorem mul_eq_right (ha : a ≠ 0) (h'a : a ≠ ∞) : b * a = a ↔ b = 1 := by
-  rw [mul_comm]
-  exact ENNReal.mul_eq_left ha h'a
-
 -- Porting note: `simp only [div_eq_mul_inv, mul_comm, mul_assoc]` doesn't work in the following two
 protected theorem mul_comm_div : a / b * c = a * (c / b) := by
   simp only [div_eq_mul_inv, mul_right_comm, ← mul_assoc]

Mathlib/Data/ENNReal/Operations.lean

@@ -27,38 +27,28 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0}
 
 section Mul
 
--- Porting note (#11215): TODO: generalize to `WithTop`
 @[mono, gcongr]
-theorem mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d := by
-  rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩
-  lift a to ℝ≥0 using ne_top_of_lt aa'
-  rcases lt_iff_exists_nnreal_btwn.1 bd with ⟨b', bb', b'd⟩
-  lift b to ℝ≥0 using ne_top_of_lt bb'
-  norm_cast at *
-  calc
-    ↑(a * b) < ↑(a' * b') := coe_lt_coe.2 (mul_lt_mul₀ aa' bb')
-    _ ≤ c * d := mul_le_mul' a'c.le b'd.le
-
--- TODO: generalize to `MulLeftMono α`
-theorem mul_left_mono : Monotone (a * ·) := fun _ _ => mul_le_mul' le_rfl
-
--- TODO: generalize to `MulRightMono α`
-theorem mul_right_mono : Monotone (· * a) := fun _ _ h => mul_le_mul' h le_rfl
+theorem mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d := WithTop.mul_lt_mul ac bd
 
--- Porting note (#11215): TODO: generalize to `WithTop`
-theorem pow_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x : ℝ≥0∞ => x ^ n
-  | 0, h => absurd rfl h
-  | 1, _ => by simpa only [pow_one] using strictMono_id
-  | n + 2, _ => fun x y h ↦ by
-    simp_rw [pow_succ _ (n + 1)]; exact mul_lt_mul (pow_strictMono n.succ_ne_zero h) h
+@[deprecated mul_left_mono (since := "2024-10-15")]
+protected theorem mul_left_mono : Monotone (a * ·) := mul_left_mono
+
+@[deprecated mul_right_mono (since := "2024-10-15")]
+protected theorem mul_right_mono : Monotone (· * a) := mul_right_mono
+
+protected lemma pow_right_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun a : ℝ≥0∞ ↦ a ^ n :=
+  WithTop.pow_right_strictMono hn
 
-@[gcongr] protected theorem pow_lt_pow_left (h : a < b) {n : ℕ} (hn : n ≠ 0) :
-    a ^ n < b ^ n :=
-  ENNReal.pow_strictMono hn h
+@[deprecated (since := "2024-10-15")] alias pow_strictMono := ENNReal.pow_right_strictMono
 
-theorem max_mul : max a b * c = max (a * c) (b * c) := mul_right_mono.map_max
+@[gcongr] protected lemma pow_lt_pow_left (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n :=
+  WithTop.pow_lt_pow_left hab hn
 
-theorem mul_max : a * max b c = max (a * b) (a * c) := mul_left_mono.map_max
+@[deprecated max_mul (since := "2024-10-15")]
+protected theorem max_mul : max a b * c = max (a * c) (b * c) := mul_right_mono.map_max
+
+@[deprecated mul_max (since := "2024-10-15")]
+protected theorem mul_max : a * max b c = max (a * b) (a * c) := mul_left_mono.map_max
 
 -- Porting note (#11215): TODO: generalize to `WithTop`
 theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : StrictMono (a * ·) := by
@@ -101,6 +91,12 @@ theorem mul_lt_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b
 theorem mul_lt_mul_right : c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b) :=
   mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_left
 
+protected lemma mul_eq_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * b = a ↔ b = 1 := by
+  simpa using ENNReal.mul_eq_mul_left ha₀ ha (c := 1)
+
+protected lemma mul_eq_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b = b ↔ a = 1 := by
+  simpa using ENNReal.mul_eq_mul_right hb₀ hb (b := 1)
+
 end Mul
 
 section OperationsAndOrder

Mathlib/MeasureTheory/Measure/Haar/Unique.lean

@@ -967,7 +967,7 @@ instance (priority := 100) IsHaarMeasure.isInvInvariant_of_regular
   have : c ^ 2 = 1 ^ 2 :=
     (ENNReal.mul_eq_mul_right (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne'
           K.isCompact.measure_lt_top.ne).1 this
-  have : c = 1 := (ENNReal.pow_strictMono two_ne_zero).injective this
+  have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
   rw [hc, this, one_smul]
 
 /-- Any inner regular Haar measure is invariant under inversion in an abelian group. -/
@@ -992,7 +992,7 @@ instance (priority := 100) IsHaarMeasure.isInvInvariant_of_innerRegular
   have : c ^ 2 = 1 ^ 2 :=
     (ENNReal.mul_eq_mul_right (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne'
           K.isCompact.measure_lt_top.ne).1 this
-  have : c = 1 := (ENNReal.pow_strictMono two_ne_zero).injective this
+  have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
   rw [hc, this, one_smul]
 
 @[to_additive]

Mathlib/MeasureTheory/OuterMeasure/Operations.lean

@@ -77,10 +77,10 @@ instance instSMul : SMul R (OuterMeasure α) :=
       mono := fun {s t} h => by
         simp only
         rw [← smul_one_mul c, ← smul_one_mul c (m t)]
-        exact ENNReal.mul_left_mono (m.mono h)
+        exact mul_left_mono (m.mono h)
       iUnion_nat := fun s _ => by
         simp_rw [← smul_one_mul c (m _), ENNReal.tsum_mul_left]
-        exact ENNReal.mul_left_mono (measure_iUnion_le _) }⟩
+        exact mul_left_mono (measure_iUnion_le _) }⟩
 
 @[simp]
 theorem coe_smul (c : R) (m : OuterMeasure α) : ⇑(c • m) = c • ⇑m :=

Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean

@@ -353,11 +353,10 @@ theorem finite_of_discr_bdd_of_isReal :
       convert hx₁
       · simp only [IntermediateField.lift_top]
       · simp only [IntermediateField.lift_adjoin, Set.image_singleton]
-  have := one_le_convexBodyLTFactor K
-  convert lt_of_le_of_lt (mul_right_mono (coe_le_coe.mpr this))
-    (ENNReal.mul_lt_mul_left' (by positivity) coe_ne_top (minkowskiBound_lt_boundOfDiscBdd hK₂))
-  simp_rw [ENNReal.coe_one, one_mul]
-
+  calc
+    minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
+    _ = 1 * B := by rw [one_mul]
+    _ ≤ convexBodyLTFactor K * B := by gcongr; exact mod_cast one_le_convexBodyLTFactor K
 
 theorem finite_of_discr_bdd_of_isComplex :
     {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F} |
@@ -402,10 +401,10 @@ theorem finite_of_discr_bdd_of_isComplex :
       convert hx₁
       · simp only [IntermediateField.lift_top]
       · simp only [IntermediateField.lift_adjoin, Set.image_singleton]
-  have := one_le_convexBodyLT'Factor K
-  convert lt_of_le_of_lt (mul_right_mono (coe_le_coe.mpr this))
-    (ENNReal.mul_lt_mul_left' (by positivity) coe_ne_top (minkowskiBound_lt_boundOfDiscBdd hK₂))
-  simp_rw [ENNReal.coe_one, one_mul]
+  calc
+    minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
+    _ = 1 * B := by rw [one_mul]
+    _ ≤ convexBodyLT'Factor K * B := by gcongr; exact mod_cast one_le_convexBodyLT'Factor K
 
 /-- **Hermite Theorem**. Let `N` be an integer. There are only finitely many number fields
 (in some fixed extension of `ℚ`) of discriminant bounded by `N`. -/

Mathlib/Topology/EMetricSpace/Lipschitz.lean

@@ -138,7 +138,7 @@ theorem edist_le_mul (h : LipschitzWith K f) (x y : α) : edist (f x) (f y) ≤
 
 theorem edist_le_mul_of_le (h : LipschitzWith K f) (hr : edist x y ≤ r) :
     edist (f x) (f y) ≤ K * r :=
-  (h x y).trans <| ENNReal.mul_left_mono hr
+  (h x y).trans <| mul_left_mono hr
 
 theorem edist_lt_mul_of_lt (h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) :
     edist (f x) (f y) < K * r :=
@@ -163,7 +163,7 @@ protected theorem of_edist_le (h : ∀ x y, edist (f x) (f y) ≤ edist x y) : L
   fun x y => by simp only [ENNReal.coe_one, one_mul, h]
 
 protected theorem weaken (hf : LipschitzWith K f) {K' : ℝ≥0} (h : K ≤ K') : LipschitzWith K' f :=
-  fun x y => le_trans (hf x y) <| ENNReal.mul_right_mono (ENNReal.coe_le_coe.2 h)
+  fun x y => le_trans (hf x y) <| mul_right_mono (ENNReal.coe_le_coe.2 h)
 
 theorem ediam_image_le (hf : LipschitzWith K f) (s : Set α) :
     EMetric.diam (f '' s) ≤ K * EMetric.diam s := by
@@ -218,7 +218,7 @@ protected theorem comp {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} (hf : L
     (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f ∘ g) := fun x y =>
   calc
     edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) := hf _ _
-    _ ≤ Kf * (Kg * edist x y) := ENNReal.mul_left_mono (hg _ _)
+    _ ≤ Kf * (Kg * edist x y) := mul_left_mono (hg _ _)
     _ = (Kf * Kg : ℝ≥0) * edist x y := by rw [← mul_assoc, ENNReal.coe_mul]
 
 theorem comp_lipschitzOnWith {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} {s : Set α}
@@ -235,7 +235,7 @@ protected theorem prod_snd : LipschitzWith 1 (@Prod.snd α β) :=
 protected theorem prod {f : α → β} {Kf : ℝ≥0} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : ℝ≥0}
     (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => (f x, g x) := by
   intro x y
-  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, ENNReal.max_mul]
+  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
   exact max_le_max (hf x y) (hg x y)
 
 protected theorem prod_mk_left (a : α) : LipschitzWith 1 (Prod.mk a : β → α × β) := by
@@ -250,8 +250,8 @@ protected theorem uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀
   simp only [Function.uncurry, ENNReal.coe_add, add_mul]
   apply le_trans (edist_triangle _ (f a₂ b₁) _)
   exact
-    add_le_add (le_trans (hα _ _ _) <| ENNReal.mul_left_mono <| le_max_left _ _)
-      (le_trans (hβ _ _ _) <| ENNReal.mul_left_mono <| le_max_right _ _)
+    add_le_add (le_trans (hα _ _ _) <| mul_left_mono <| le_max_left _ _)
+      (le_trans (hβ _ _ _) <| mul_left_mono <| le_max_right _ _)
 
 /-- Iterates of a Lipschitz function are Lipschitz. -/
 protected theorem iterate {f : α → α} (hf : LipschitzWith K f) : ∀ n, LipschitzWith (K ^ n) f^[n]
@@ -299,7 +299,7 @@ protected theorem continuousOn (hf : LipschitzOnWith K f s) : ContinuousOn f s :
 theorem edist_le_mul_of_le (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
     {r : ℝ≥0∞} (hr : edist x y ≤ r) :
     edist (f x) (f y) ≤ K * r :=
-  (h hx hy).trans <| ENNReal.mul_left_mono hr
+  (h hx hy).trans <| mul_left_mono hr
 
 theorem edist_lt_of_edist_lt_div (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
     {d : ℝ≥0∞} (hd : edist x y < d / K) : edist (f x) (f y) < d :=
@@ -314,7 +314,7 @@ protected theorem comp {g : β → γ} {t : Set β} {Kg : ℝ≥0} (hg : Lipschi
 protected theorem prod {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s)
     (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s := by
   intro _ hx _ hy
-  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, ENNReal.max_mul]
+  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
   exact max_le_max (hf hx hy) (hg hx hy)
 
 theorem ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α) (t : Set β)
@@ -325,8 +325,8 @@ theorem ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α
   refine (edist_triangle _ (f a₂ b₁) _).trans ?_
   exact
     add_le_add
-      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| ENNReal.mul_left_mono <| EMetric.edist_le_diam_of_mem ha₁ ha₂)
-      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| ENNReal.mul_left_mono <| EMetric.edist_le_diam_of_mem hb₁ hb₂)
+      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_left_mono <| EMetric.edist_le_diam_of_mem ha₁ ha₂)
+      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_left_mono <| EMetric.edist_le_diam_of_mem hb₁ hb₂)
 
 end LipschitzOnWith