diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index ee9515038917d..dcf4e997f2617 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -587,13 +587,12 @@ theorem exists_one_lt_of_prod_one_of_exists_ne_one' (f : ι → M) (h₁ : ∏ i
 
 end LinearOrderedCancelCommMonoid
 
-section OrderedCommSemiring
-
-variable [OrderedCommSemiring R] {f g : ι → R} {s t : Finset ι}
+section CommMonoidWithZero
+variable [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R]
 
-open Classical
+section PosMulMono
+variable [PosMulMono R] {f g : ι → R} {s t : Finset ι}
 
--- this is also true for an ordered commutative multiplicative monoid with zero
 theorem prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i in s, f i :=
   prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0
 #align finset.prod_nonneg Finset.prod_nonneg
@@ -603,14 +602,15 @@ product of `f i` is less than or equal to the product of `g i`. See also `Finset
 the case of an ordered commutative multiplicative monoid. -/
 theorem prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
     ∏ i in s, f i ≤ ∏ i in s, g i := by
-  induction' s using Finset.induction with a s has ih h
+  induction' s using Finset.cons_induction with a s has ih h
   · simp
-  · simp only [prod_insert has]
+  · simp only [prod_cons]
+    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
     apply mul_le_mul
-    · exact h1 a (mem_insert_self a s)
-    · refine ih (fun x H ↦ h0 _ ?_) (fun x H ↦ h1 _ ?_) <;> exact mem_insert_of_mem H
-    · apply prod_nonneg fun x H ↦ h0 x (mem_insert_of_mem H)
-    · apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s))
+    · exact h1 a (mem_cons_self a s)
+    · refine ih (fun x H ↦ h0 _ ?_) (fun x H ↦ h1 _ ?_) <;> exact subset_cons _ H
+    · apply prod_nonneg fun x H ↦ h0 x (subset_cons _ H)
+    · apply le_trans (h0 a (mem_cons_self a s)) (h1 a (mem_cons_self a s))
 #align finset.prod_le_prod Finset.prod_le_prod
 
 /-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
@@ -630,31 +630,10 @@ theorem prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1)
   exact Finset.prod_const_one
 #align finset.prod_le_one Finset.prod_le_one
 
-/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
-  sum of the products of `g` and `h`. This is the version for `OrderedCommSemiring`. -/
-theorem prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h i ≤ f i)
-    (hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j) (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) (hg : ∀ i ∈ s, 0 ≤ g i)
-    (hh : ∀ i ∈ s, 0 ≤ h i) : ((∏ i in s, g i) + ∏ i in s, h i) ≤ ∏ i in s, f i := by
-  simp_rw [prod_eq_mul_prod_diff_singleton hi]
-  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
-  · rw [right_distrib]
-    refine add_le_add ?_ ?_ <;>
-    · refine mul_le_mul_of_nonneg_left ?_ ?_
-      · refine prod_le_prod ?_ ?_
-        <;> simp (config := { contextual := true }) [*]
-      · try apply_assumption
-        try assumption
-  · apply prod_nonneg
-    simp only [and_imp, mem_sdiff, mem_singleton]
-    intro j h1j h2j
-    exact le_trans (hg j h1j) (hgf j h1j h2j)
-#align finset.prod_add_prod_le Finset.prod_add_prod_le
-
-end OrderedCommSemiring
-
-section StrictOrderedCommSemiring
+end PosMulMono
 
-variable [StrictOrderedCommSemiring R] {f g : ι → R} {s : Finset ι}
+section PosMulStrictMono
+variable [PosMulStrictMono R] [MulPosMono R] [Nontrivial R] {f g : ι → R} {s t : Finset ι}
 
 -- This is also true for an ordered commutative multiplicative monoid with zero
 theorem prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i in s, f i :=
@@ -667,11 +646,12 @@ theorem prod_lt_prod (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i
   classical
   obtain ⟨i, hi, hilt⟩ := hlt
   rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
-  apply mul_lt_mul hilt
+  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
+  refine mul_lt_mul_of_le_of_lt' hilt ?_ ?_ ?_
   · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
       (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
+  · exact (hf i hi).le.trans hilt.le
   · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
-  · exact le_of_lt <| (hf i hi).trans hilt
 
 theorem prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i)
     (h_ne : s.Nonempty) :
@@ -680,8 +660,37 @@ theorem prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s,
   obtain ⟨i, hi⟩ := h_ne
   exact ⟨i, hi, hfg i hi⟩
 
+end PosMulStrictMono
+end CommMonoidWithZero
+
+section StrictOrderedCommSemiring
+
 end StrictOrderedCommSemiring
 
+section OrderedCommSemiring
+variable [OrderedCommSemiring R] {f g : ι → R} {s t : Finset ι}
+
+/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
+  sum of the products of `g` and `h`. This is the version for `OrderedCommSemiring`. -/
+lemma prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h i ≤ f i)
+    (hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j) (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) (hg : ∀ i ∈ s, 0 ≤ g i)
+    (hh : ∀ i ∈ s, 0 ≤ h i) : ((∏ i in s, g i) + ∏ i in s, h i) ≤ ∏ i in s, f i := by
+  classical
+  simp_rw [prod_eq_mul_prod_diff_singleton hi]
+  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
+  · rw [right_distrib]
+    refine add_le_add ?_ ?_ <;>
+    · refine mul_le_mul_of_nonneg_left ?_ ?_
+      · refine prod_le_prod ?_ ?_ <;> simp (config := { contextual := true }) [*]
+      · try apply_assumption
+        try assumption
+  · apply prod_nonneg
+    simp only [and_imp, mem_sdiff, mem_singleton]
+    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
+#align finset.prod_add_prod_le Finset.prod_add_prod_le
+
+end OrderedCommSemiring
+
 section LinearOrderedCommSemiring
 variable [LinearOrderedCommSemiring α] [ExistsAddOfLE α]
 
@@ -825,7 +834,7 @@ positive if each `f i` is and `s` is nonempty.
 
 Note that this does not do any complicated reasoning. In particular, it does not try to feed in the
 `i ∈ s` hypothesis to local assumptions, and the only ways it can prove `s` is nonempty is if there
-is a local `s.Nonempty` hypothesis or `s = (univ : Finset α)` and `Nonempty α` can be synthesized by
+is a local `s.Nonempty` hypothesis or `s = (univ : Finset ι)` and `Nonempty ι` can be synthesized by
 TC inference.
 
 TODO: The following example does not work
@@ -852,7 +861,7 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
           match s with
           | ~q(@univ _ $fi) => do
             let _no ← synthInstanceQ q(Nonempty $ι)
-            return q(Finset.univ_nonempty (α := $ι))
+            pure q(Finset.univ_nonempty (α := $ι))
           | _ => throwError "`s` is not `univ`"
         catch _ => do
           let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s)
@@ -861,16 +870,14 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      return .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $ps)
+      pure $ .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $ps)
     -- Try to show that the sum is nonnegative
     catch _ => do
       let pbody ← rbody.toNonneg
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
       let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
       assertInstancesCommute
-      let proof := q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
-      proof.check
-      return .nonnegative proof
+      pure $ .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
 example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∑ j in range n, a j^2 := by positivity
@@ -889,4 +896,76 @@ example (s : Finset ℕ) (f : ℕ → ℕ) (a : ℕ) : 0 ≤ s.sum (f a) := by p
 set_option linter.unusedVariables false in
 example (f : ℕ → ℕ) (hf : 0 ≤ f 0) : 0 ≤ ∑ n in Finset.range 10, f n := by positivity
 
+/-- We make an alias by hand to keep control over the order of the arguments. -/
+private lemma prod_ne_zero {ι α : Type*} [CommMonoidWithZero α] [Nontrivial α] [NoZeroDivisors α]
+    {f : ι → α} {s : Finset ι} : (∀ i ∈ s, f i ≠ 0) → ∏ i in s, f i ≠ 0 := prod_ne_zero_iff.2
+
+/-- The `positivity` extension which proves that `∏ i in s, f i` is nonnegative if `f` is, and
+positive if each `f i` is.
+
+Note that this does not do any complicated reasoning. In particular, it does not try to feed in the
+`i ∈ s` hypothesis to local assumptions.
+
+TODO: The following example does not work
+```
+example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.prod f := by positivity
+```
+because `compareHyp` can't look for assumptions behind binders.
+-/
+@[positivity Finset.prod _ _]
+def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.prod _ $ι $instα $s $f) =>
+    let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
+    have body : Q($α) := Expr.betaRev f #[i]
+    let rbody ← core zα pα body
+    -- Try to show that the sum is positive
+    try
+      let .positive pbody := rbody | failure -- Fail if the body is not provably positive
+      let instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+      let instαzeroone ← synthInstanceQ q(ZeroLEOneClass $α)
+      let instαposmul ← synthInstanceQ q(PosMulStrictMono $α)
+      let instαnontriv ← synthInstanceQ q(Nontrivial $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
+      pure $ .positive q(@prod_pos $ι $α $instαmon $pα $instαzeroone $instαposmul $instαnontriv $f
+        $s fun i _ ↦ $pr i)
+    -- Try to show that the sum is nonnegative
+    catch _ => try
+      let pbody ← rbody.toNonneg
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
+      let instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+      let instαzeroone ← synthInstanceQ q(ZeroLEOneClass $α)
+      let instαposmul ← synthInstanceQ q(PosMulMono $α)
+      assertInstancesCommute
+      pure $ .nonnegative q(@prod_nonneg $ι $α $instαmon $pα $instαzeroone $instαposmul $f $s
+        fun i _ ↦ $pr i)
+    catch _ =>
+      let pbody ← rbody.toNonzero
+      let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody
+      let instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+      let instαnontriv ← synthInstanceQ q(Nontrivial $α)
+      let instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
+      assertInstancesCommute
+      pure $ .nonzero q(@prod_ne_zero $ι $α $instαmon $instαnontriv $instαnozerodiv $f $s
+        fun i _ ↦ $pr i)
+  | _ => throwError "not Finset.sum"
+
+example (n : ℕ) : ∏ j in range n, (-1) ≠ 0 := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∏ j in range n, a j^2 := by positivity
+example (a : ULift.{2} ℕ → ℤ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ ∏ j in s, a j^2 := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∏ j : Fin 8, ∏ i in range n, (a j^2 + i ^ 2) := by positivity
+example (n : ℕ) (a : ℕ → ℤ) : 0 < ∏ j : Fin (n + 1), (a j^2 + 1) := by positivity
+example (a : ℕ → ℤ) : 0 < ∏ j in ({1} : Finset ℕ), (a j^2 + 1) := by
+  have : Finset.Nonempty {1} := singleton_nonempty 1
+  positivity
+example (s : Finset ℕ) : 0 ≤ ∏ j in s, j := by positivity
+example (s : Finset ℕ) : 0 ≤ s.sum id := by positivity
+example (s : Finset ℕ) (f : ℕ → ℕ) (a : ℕ) : 0 ≤ s.sum (f a) := by positivity
+
+-- Make sure that the extension doesn't produce an invalid term by accidentally unifying `?n` with
+-- `0` because of the `hf` assumption
+set_option linter.unusedVariables false in
+example (f : ℕ → ℕ) (hf : 0 ≤ f 0) : 0 ≤ ∏ n in Finset.range 10, f n := by positivity
+
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index a3f3d96975b64..bc1e0650e01ce 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -339,9 +339,7 @@ the norms of the relevant bits of `q` and `p`. -/
 theorem compAlongComposition_norm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
     (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
     ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖ :=
-  ContinuousMultilinearMap.opNorm_le_bound _
-    (mul_nonneg (norm_nonneg _) (Finset.prod_nonneg fun _i _hi => norm_nonneg _))
-    (compAlongComposition_bound _ _ _)
+  ContinuousMultilinearMap.opNorm_le_bound _ (by positivity) (compAlongComposition_bound _ _ _)
 #align formal_multilinear_series.comp_along_composition_norm FormalMultilinearSeries.compAlongComposition_norm
 
 theorem compAlongComposition_nnnorm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean
index 665e5757eddd0..9c0079b2f6073 100644
--- a/Mathlib/Analysis/Analytic/Inverse.lean
+++ b/Mathlib/Analysis/Analytic/Inverse.lean
@@ -477,8 +477,7 @@ theorem radius_rightInv_pos_of_radius_pos_aux2 {n : ℕ} (hn : 2 ≤ n + 1)
       gcongr
       apply (compAlongComposition_norm _ _ _).trans
       gcongr
-      · exact prod_nonneg fun j _ => norm_nonneg _
-      · apply hp
+      apply hp
     _ =
         I * a +
           I * C *
diff --git a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean b/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
index 4001c02042efd..52716cb9174a1 100644
--- a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
+++ b/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
@@ -215,24 +215,18 @@ operation. -/
 theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)]
     [∀ i, NormedSpace 𝕜 (E i)] :
     IsBoundedLinearMap 𝕜 fun p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G =>
-      p.1.prod p.2 :=
-  { map_add := fun p₁ p₂ => by
-      ext1 m
-      rfl
-    map_smul := fun c p => by
-      ext1 m
-      rfl
-    bound :=
-      ⟨1, zero_lt_one, fun p => by
-        rw [one_mul]
-        apply ContinuousMultilinearMap.opNorm_le_bound _ (norm_nonneg _) _
-        intro m
-        rw [ContinuousMultilinearMap.prod_apply, norm_prod_le_iff]
-        constructor
-        · exact (p.1.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_fst_le p)
-            (Finset.prod_nonneg fun i _ => norm_nonneg _))
-        · exact (p.2.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_snd_le p)
-            (Finset.prod_nonneg fun i _ => norm_nonneg _))⟩ }
+      p.1.prod p.2 where
+  map_add p₁ p₂ := by ext : 1; rfl
+  map_smul c p := by ext : 1; rfl
+  bound := by
+    refine ⟨1, zero_lt_one, fun p ↦ ?_⟩
+    rw [one_mul]
+    apply ContinuousMultilinearMap.opNorm_le_bound _ (norm_nonneg _) _
+    intro m
+    rw [ContinuousMultilinearMap.prod_apply, norm_prod_le_iff]
+    constructor
+    · exact (p.1.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_fst_le p) $ by positivity)
+    · exact (p.2.le_opNorm m).trans (mul_le_mul_of_nonneg_right (norm_snd_le p) $ by positivity)
 #align is_bounded_linear_map_prod_multilinear isBoundedLinearMap_prod_multilinear
 
 /-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
index 28b8d17ee0235..2b1057b198dab 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -258,8 +258,7 @@ theorem continuous_of_bound (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m
   have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
   replace H : ∀ m, ‖f m‖ ≤ D * ∏ i, ‖m i‖
   · intro m
-    apply le_trans (H m) (mul_le_mul_of_nonneg_right (le_max_left _ _) _)
-    exact prod_nonneg fun (i : ι) _ => norm_nonneg (m i)
+    apply le_trans (H m) (mul_le_mul_of_nonneg_right (le_max_left _ _) $ by positivity)
   refine' continuous_iff_continuousAt.2 fun m => _
   refine'
     continuousAt_of_locally_lipschitz zero_lt_one
@@ -383,7 +382,7 @@ variable {f m}
 theorem le_mul_prod_of_le_opNorm_of_le {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) :
     ‖f m‖ ≤ C * ∏ i, b i :=
   (f.le_opNorm m).trans <| mul_le_mul hC (prod_le_prod (fun _ _ ↦ norm_nonneg _) fun _ _ ↦ hm _)
-    (prod_nonneg fun _ _ ↦ norm_nonneg _) ((opNorm_nonneg _).trans hC)
+    (by positivity) ((opNorm_nonneg _).trans hC)
 
 @[deprecated]
 alias le_mul_prod_of_le_op_norm_of_le :=
@@ -431,8 +430,7 @@ alias le_of_op_norm_le :=
 variable (f)
 
 theorem ratio_le_opNorm : (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖ :=
-  div_le_of_nonneg_of_le_mul (prod_nonneg fun _ _ => norm_nonneg _) (opNorm_nonneg _)
-    (f.le_opNorm m)
+  div_le_of_nonneg_of_le_mul (by positivity) (opNorm_nonneg _) (f.le_opNorm m)
 #align continuous_multilinear_map.ratio_le_op_norm ContinuousMultilinearMap.ratio_le_opNorm
 
 @[deprecated]
@@ -819,9 +817,8 @@ theorem MultilinearMap.mkContinuous_norm_le (f : MultilinearMap 𝕜 E G) {C : 
 nonnegative. -/
 theorem MultilinearMap.mkContinuous_norm_le' (f : MultilinearMap 𝕜 E G) {C : ℝ}
     (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0 :=
-  ContinuousMultilinearMap.opNorm_le_bound _ (le_max_right _ _) fun m =>
-    (H m).trans <|
-      mul_le_mul_of_nonneg_right (le_max_left _ _) (prod_nonneg fun _ _ => norm_nonneg _)
+  ContinuousMultilinearMap.opNorm_le_bound _ (le_max_right _ _) fun m ↦ (H m).trans $
+    mul_le_mul_of_nonneg_right (le_max_left _ _) $ by positivity
 #align multilinear_map.mk_continuous_norm_le' MultilinearMap.mkContinuous_norm_le'
 
 namespace ContinuousMultilinearMap
@@ -1051,8 +1048,7 @@ def flipMultilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :
           LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk] }
     ‖f‖ fun m => by
       dsimp only [MultilinearMap.coe_mk]
-      refine LinearMap.mkContinuous_norm_le _
-        (mul_nonneg (norm_nonneg f) (prod_nonneg fun i _ => norm_nonneg (m i))) _
+      exact LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_linear_map.flip_multilinear ContinuousLinearMap.flipMultilinear
 #align continuous_linear_map.flip_multilinear_apply_apply ContinuousLinearMap.flipMultilinear_apply_apply
 
@@ -1125,7 +1121,7 @@ def mkContinuousMultilinear (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G
       simp only [coe_mk]
       refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
       rw [max_mul_of_nonneg, zero_mul]
-      exact prod_nonneg fun _ _ => norm_nonneg _
+      positivity
 #align multilinear_map.mk_continuous_multilinear MultilinearMap.mkContinuousMultilinear
 
 @[simp]
@@ -1156,7 +1152,7 @@ set_option linter.uppercaseLean3 false
 
 theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
     (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
-  opNorm_le_bound _ (mul_nonneg (norm_nonneg _) <| prod_nonneg fun i _ => norm_nonneg _) fun m =>
+  opNorm_le_bound _ (by positivity) fun m =>
     calc
       ‖g fun i => f i (m i)‖ ≤ ‖g‖ * ∏ i, ‖f i (m i)‖ := g.le_opNorm _
       _ ≤ ‖g‖ * ∏ i, ‖f i‖ * ‖m i‖ :=
@@ -1215,7 +1211,7 @@ variable (G)
 
 theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
     ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
-  LinearMap.mkContinuous_norm_le _ (prod_nonneg fun _ _ => norm_nonneg _) _
+  LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_multilinear_map.norm_comp_continuous_linear_mapL_le ContinuousMultilinearMap.norm_compContinuousLinearMapL_le
 
 variable (𝕜 E E₁)
@@ -1372,8 +1368,6 @@ addition of `Finset.prod` where needed. The duplication could be avoided by dedu
 case from the multilinear case via a currying isomorphism. However, this would mess up imports,
 and it is more satisfactory to have the simplest case as a standalone proof. -/
 instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearMap 𝕜 E G) := by
-  have nonneg : ∀ v : ∀ i, E i, 0 ≤ ∏ i, ‖v i‖ := fun v =>
-    Finset.prod_nonneg fun i _ => norm_nonneg _
   -- We show that every Cauchy sequence converges.
   refine' Metric.complete_of_cauchySeq_tendsto fun f hf => _
   -- We now expand out the definition of a Cauchy sequence,
@@ -1382,12 +1376,13 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
   have cau : ∀ v, CauchySeq fun n => f n v := by
     intro v
     apply cauchySeq_iff_le_tendsto_0.2 ⟨fun n => b n * ∏ i, ‖v i‖, _, _, _⟩
-    · intro
-      exact mul_nonneg (b0 _) (nonneg v)
+    · intro n
+      have := b0 n
+      positivity
     · intro n m N hn hm
       rw [dist_eq_norm]
       apply le_trans ((f n - f m).le_opNorm v) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m N hn hm) (nonneg v)
+      exact mul_le_mul_of_nonneg_right (b_bound n m N hn hm) $ by positivity
     · simpa using b_lim.mul tendsto_const_nhds
   -- We assemble the limits points of those Cauchy sequences
   -- (which exist as `G` is complete)
@@ -1414,7 +1409,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
     have A : ∀ n, ‖f n v‖ ≤ (b 0 + ‖f 0‖) * ∏ i, ‖v i‖ := by
       intro n
       apply le_trans ((f n).le_opNorm _) _
-      apply mul_le_mul_of_nonneg_right _ (nonneg v)
+      apply mul_le_mul_of_nonneg_right _ $ by positivity
       calc
         ‖f n‖ = ‖f n - f 0 + f 0‖ := by
           congr 1
@@ -1434,7 +1429,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
     have A : ∀ᶠ m in atTop, ‖(f n - f m) v‖ ≤ b n * ∏ i, ‖v i‖ := by
       refine' eventually_atTop.2 ⟨n, fun m hm => _⟩
       apply le_trans ((f n - f m).le_opNorm _) _
-      exact mul_le_mul_of_nonneg_right (b_bound n m n le_rfl hm) (nonneg v)
+      exact mul_le_mul_of_nonneg_right (b_bound n m n le_rfl hm) $ by positivity
     have B : Tendsto (fun m => ‖(f n - f m) v‖) atTop (𝓝 ‖(f n - Fcont) v‖) :=
       Tendsto.norm (tendsto_const_nhds.sub (hF v))
     exact le_of_tendsto B A
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
index b7ca31521d76c..d8c1ba853e03b 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
@@ -63,8 +63,7 @@ theorem ContinuousLinearMap.norm_map_tail_le
     ‖f (m 0) (tail m)‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
   calc
     ‖f (m 0) (tail m)‖ ≤ ‖f (m 0)‖ * ∏ i, ‖(tail m) i‖ := (f (m 0)).le_opNorm _
-    _ ≤ ‖f‖ * ‖m 0‖ * ∏ i, ‖(tail m) i‖ :=
-      (mul_le_mul_of_nonneg_right (f.le_opNorm _) (prod_nonneg fun _ _ => norm_nonneg _))
+    _ ≤ ‖f‖ * ‖m 0‖ * ∏ i, ‖tail m i‖ := mul_le_mul_of_nonneg_right (f.le_opNorm _) $ by positivity
     _ = ‖f‖ * (‖m 0‖ * ∏ i, ‖(tail m) i‖) := by ring
     _ = ‖f‖ * ∏ i, ‖m i‖ := by
       rw [prod_univ_succ]
@@ -269,8 +268,7 @@ def ContinuousMultilinearMap.curryRight (f : ContinuousMultilinearMap 𝕜 Ei G)
         simp }
   f'.mkContinuous ‖f‖ fun m => by
     simp only [MultilinearMap.coe_mk]
-    exact LinearMap.mkContinuous_norm_le _
-      (mul_nonneg (norm_nonneg _) (prod_nonneg fun _ _ => norm_nonneg _)) _
+    exact LinearMap.mkContinuous_norm_le _ (by positivity) _
 #align continuous_multilinear_map.curry_right ContinuousMultilinearMap.curryRight
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean
index cf08da5dca7ed..4588938b2232a 100644
--- a/Mathlib/Data/Nat/Choose/Multinomial.lean
+++ b/Mathlib/Data/Nat/Choose/Multinomial.lean
@@ -66,7 +66,7 @@ lemma multinomial_cons (ha : a ∉ s) (f : α → ℕ) :
     multinomial, mul_assoc, mul_left_comm _ (f a)!,
     Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
     Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
-  exact prod_pos fun i _ ↦ by positivity
+  positivity
 
 lemma multinomial_insert [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) :
     multinomial (insert a s) f = (f a + ∑ i in s, f i).choose (f a) * multinomial s f := by
diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
index bfb6a8406ef8b..08894cd287ad3 100644
--- a/Mathlib/Data/Nat/Factorial/BigOperators.lean
+++ b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -25,8 +25,7 @@ namespace Nat
 
 variable {α : Type*} (s : Finset α) (f : α → ℕ)
 
-theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! :=
-  Finset.prod_pos fun i _ => factorial_pos (f i)
+theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! := by positivity
 #align nat.prod_factorial_pos Nat.prod_factorial_pos
 
 theorem prod_factorial_dvd_factorial_sum : (∏ i in s, (f i)!) ∣ (∑ i in s, f i)! := by
diff --git a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
index 641792e939b2a..319f47858d6db 100644
--- a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
@@ -200,8 +200,7 @@ theorem norm_torusIntegral_le_of_norm_le_const {C : ℝ} (hf : ∀ θ, ‖f (tor
           ‖(∏ i : Fin n, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)‖ =
               (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖ :=
             by simp [norm_smul]
-          _ ≤ (∏ i : Fin n, |R i|) * C :=
-            mul_le_mul_of_nonneg_left (hf _) (Finset.prod_nonneg fun _ _ => abs_nonneg _)
+          _ ≤ (∏ i : Fin n, |R i|) * C := mul_le_mul_of_nonneg_left (hf _) $ by positivity
     _ = ((2 * π) ^ (n : ℕ) * ∏ i, |R i|) * C := by
       simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero,
         Fin.prod_const, mul_assoc, mul_comm ((2 * π) ^ (n : ℕ))]