diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean
index ee95ae00050ea..a4ff5ac87b48c 100644
--- a/Mathlib/Algebra/Order/Module.lean
+++ b/Mathlib/Algebra/Order/Module.lean
@@ -73,8 +73,8 @@ theorem lt_of_smul_lt_smul_of_nonpos (h : c • a < c • b) (hc : c ≤ 0) : b
 lemma smul_le_smul_of_nonneg_right (h : c ≤ d) (hb : 0 ≤ b) : c • b ≤ d • b := by
   rw [← sub_nonneg, ← sub_smul]; exact smul_nonneg (sub_nonneg.2 h) hb
 
-lemma smul_le_smul (hcd : c ≤ d) (hab : a ≤ b) (ha : 0 ≤ a) (hd : 0 ≤ d) : c • a ≤ d • b :=
-  (smul_le_smul_of_nonneg_right hcd ha).trans $ smul_le_smul_of_nonneg_left hab hd
+lemma smul_le_smul (hcd : c ≤ d) (hab : a ≤ b) (hc : 0 ≤ c) (hb : 0 ≤ b) : c • a ≤ d • b :=
+  (smul_le_smul_of_nonneg_left hab hc).trans $ smul_le_smul_of_nonneg_right hcd hb
 
 theorem smul_lt_smul_iff_of_neg (hc : c < 0) : c • a < c • b ↔ b < a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
diff --git a/Mathlib/Analysis/Convex/Mul.lean b/Mathlib/Analysis/Convex/Mul.lean
index da2720a806aa8..d5749bfc15a75 100644
--- a/Mathlib/Analysis/Convex/Mul.lean
+++ b/Mathlib/Analysis/Convex/Mul.lean
@@ -31,8 +31,8 @@ lemma ConvexOn.smul' (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ :
     (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : MonovaryOn f g s) : ConvexOn 𝕜 s (f • g) := by
   refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
   dsimp
-  refine (smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) (hg₀ $ hf.1 hx hy ha hb hab) $
-    add_nonneg (smul_nonneg ha $ hf₀ hx) $ smul_nonneg hb $ hf₀ hy).trans ?_
+  refine (smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) (hf₀ $ hf.1 hx hy ha hb hab) $
+    add_nonneg (smul_nonneg ha $ hg₀ hx) $ smul_nonneg hb $ hg₀ hy).trans ?_
   calc
       _ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := ?_
     _ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by
@@ -50,7 +50,7 @@ lemma ConcaveOn.smul' (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀
   refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
   dsimp
   refine (smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) (add_nonneg
-    (smul_nonneg ha $ hg₀ hx) $ smul_nonneg hb $ hg₀ hy) $ hf₀ $ hf.1 hx hy ha hb hab).trans' ?_
+    (smul_nonneg ha $ hf₀ hx) $ smul_nonneg hb $ hf₀ hy) $ hg₀ $ hf.1 hx hy ha hb hab).trans' ?_
   calc a • f x • g x + b • f y • g y
         = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by simp_rw [hab, mul_one]
     _ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by