From 64fa1c5f8275e6f39cc06e682f35968d893f30d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 30 Dec 2023 22:35:49 +0100
Subject: [PATCH 01/20] feat: Positivity extension for `Finset.sum` Note this
 extension is pretty unopinionated about deriving `Finset.Nonempty`
 assumptions. We might want to buff it up in the future but it's already a big
 improvement over the nothing we currently have.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>
---
 Mathlib/Algebra/BigOperators/Order.lean | 49 +++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index e3f0dedb9ff23..29f0af258f744 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -830,3 +830,52 @@ theorem IsAbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedC
 #align is_absolute_value.map_prod IsAbsoluteValue.map_prod
 
 end AbsoluteValue
+
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
+
+/-- The `positivity` extension which proves that `∑ i in s, f i` is nonnegative if `f` is, and
+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
+TC inference. -/
+@[positivity Finset.sum _ _]
+def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.sum _ $ι $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      pure (.nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i))
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      pure (.positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi))
+    | _, _ => pure .none
+  | _ => throwError "not Finset.sum"
+
+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
+
+end Mathlib.Meta.Positivity

From eb70e941c1358dcbab1207cebbe94309de1a5093 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 31 Dec 2023 09:54:36 +0000
Subject: [PATCH 02/20] remove unused instance synthesis

---
 Mathlib/Algebra/BigOperators/Order.lean        | 13 +++++++------
 Mathlib/Computability/AkraBazzi/AkraBazzi.lean |  3 ---
 2 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 29f0af258f744..2d6e53e4f0e3e 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -846,13 +846,14 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   match e with
   | ~q(@Finset.sum _ $ι $instα $s $f) =>
     let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
-    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+     -- TODO: The following annotation is ignored. See leanprover/lean4#3126
+    let so : Option Q(Finset.Nonempty $s) ← do
       try
-        let _fi ← synthInstanceQ q(Fintype $ι)
         let _no ← synthInstanceQ q(Nonempty $ι)
         match s with
-        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
-        | _ => pure none
+        | ~q(@univ _ $fi) => do
+          return some q(Finset.univ_nonempty (α := $ι))
+        | _ => throwError "`s` is not `univ`"
       catch _ => do
         let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
         pure (some (.fvar fv))
@@ -861,12 +862,12 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
       assertInstancesCommute
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
-      pure (.nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i))
+      return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
     | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
       let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
-      pure (.positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi))
+      return .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi)
     | _, _ => pure .none
   | _ => throwError "not Finset.sum"
 
diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
index 1c4adb124c365..2b5086548dd60 100644
--- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
+++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@@ -1243,9 +1243,6 @@ lemma T_isBigO_smoothingFn_mul_asympBound :
                 * ((1 + (∑ u in range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
             · have := R.a_pos i
               positivity
-            · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
-              rw [div_nonneg_iff]
-              exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
             · exact bound1 n hn i
         _ = (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
                 * ((1 + ((∑ u in range n, g u / u ^ ((p a b) + 1))

From 5aa5b0ea95b9bfb5a3295ad785a7e87773897d62 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 31 Dec 2023 10:54:30 +0000
Subject: [PATCH 03/20] golf downstream

---
 Mathlib/Analysis/Analytic/Inverse.lean         |  2 --
 Mathlib/Analysis/Calculus/ContDiff/Bounds.lean | 12 ++++--------
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean
index 594ec3620e7e9..665e5757eddd0 100644
--- a/Mathlib/Analysis/Analytic/Inverse.lean
+++ b/Mathlib/Analysis/Analytic/Inverse.lean
@@ -535,8 +535,6 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F)
       exact mul_nonneg (add_nonneg (norm_nonneg _) zero_le_one) apos.le
     · intro n one_le_n hn
       have In : 2 ≤ n + 1 := by linarith only [one_le_n]
-      have Snonneg : 0 ≤ S n :=
-        sum_nonneg fun x _ => mul_nonneg (pow_nonneg apos.le _) (norm_nonneg _)
       have rSn : r * S n ≤ 1 / 2 :=
         calc
           r * S n ≤ r * ((I + 1) * a) := by gcongr
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
index 492c3d2771bb1..96df1b6469952 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
@@ -67,8 +67,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
           IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
         _ ≤ ‖B‖ * ∑ i : ℕ in Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
               ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
-          (mul_le_mul_of_nonneg_right (B.norm_precompR_le Du)
-            (Finset.sum_nonneg' fun i => by positivity))
+            mul_le_mul_of_nonneg_right (B.norm_precompR_le Du) (by positivity)
         _ = _ := by
           congr 1
           apply Finset.sum_congr rfl fun i hi => ?_
@@ -90,8 +89,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
         _ ≤ ‖B‖ * ∑ i : ℕ in Finset.range (n + 1),
             n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
               ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
-          (mul_le_mul_of_nonneg_right (B.norm_precompL_le Du)
-            (Finset.sum_nonneg' fun i => by positivity))
+            mul_le_mul_of_nonneg_right (B.norm_precompL_le Du) (by positivity)
         _ = _ := by
           congr 1
           apply Finset.sum_congr rfl fun i _ => ?_
@@ -222,8 +220,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
         ‖iteratedFDerivWithin 𝕜 (n - i) gu su xu‖ :=
     Bu.norm_iteratedFDerivWithin_le_of_bilinear_aux hfu hgu hsu hxu
   simp only [Nfu, Ngu, NBu] at this
-  apply this.trans (mul_le_mul_of_nonneg_right Bu_le ?_)
-  exact Finset.sum_nonneg' fun i => by positivity
+  exact this.trans (mul_le_mul_of_nonneg_right Bu_le (by positivity))
 #align continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear
 
 /-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the
@@ -249,8 +246,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
       ∑ i in Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
         ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ := by
   apply (B.norm_iteratedFDerivWithin_le_of_bilinear hf hg hs hx hn).trans
-  apply mul_le_of_le_one_left (Finset.sum_nonneg' fun i => ?_) hB
-  positivity
+  exact mul_le_of_le_one_left (by positivity) hB
 #align continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear_of_le_one ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
 
 /-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the

From e964bfde200ae9a74d16e9180ac240ff054a3ada Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 31 Dec 2023 13:11:13 +0000
Subject: [PATCH 04/20] hack

---
 Mathlib/Algebra/BigOperators/Order.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 2d6e53e4f0e3e..b70190e700898 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -849,9 +849,11 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
      -- TODO: The following annotation is ignored. See leanprover/lean4#3126
     let so : Option Q(Finset.Nonempty $s) ← do
       try
-        let _no ← synthInstanceQ q(Nonempty $ι)
         match s with
         | ~q(@univ _ $fi) => do
+          -- TODO(Qq): doesn't type-check without explicit `u`, even though it works outside the
+          -- `match`.
+          let _no ← synthInstanceQ (u := 0) q(Nonempty $ι)
           return some q(Finset.univ_nonempty (α := $ι))
         | _ => throwError "`s` is not `univ`"
       catch _ => do

From 695ea5254f6e04fe8b002b8ffc27759f75c5b220 Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Sun, 31 Dec 2023 15:01:58 +0000
Subject: [PATCH 05/20] beta expand if needed

---
 Mathlib/Algebra/BigOperators/Order.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index b70190e700898..af0773cd71821 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -845,7 +845,7 @@ TC inference. -/
 def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   match e with
   | ~q(@Finset.sum _ $ι $instα $s $f) =>
-    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope (if f.isLambda then f else q(fun x => $f x))
      -- TODO: The following annotation is ignored. See leanprover/lean4#3126
     let so : Option Q(Finset.Nonempty $s) ← do
       try
@@ -880,5 +880,7 @@ example (n : ℕ) (a : ℕ → ℤ) : 0 < ∑ j : Fin (n + 1), (a j^2 + 1) := by
 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
 
 end Mathlib.Meta.Positivity

From c3d02ea50482d1535f3b7dc184d68a4c8b1f31d9 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 12 Feb 2024 10:46:40 +0000
Subject: [PATCH 06/20] simplify logic

---
 Mathlib/Algebra/BigOperators/Order.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 8d8e38589f0b9..7377e923942e7 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -831,30 +831,28 @@ TC inference. -/
 def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   match e with
   | ~q(@Finset.sum _ $ι $instα $s $f) =>
-    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope (if f.isLambda then f else q(fun x => $f x))
-     -- TODO: The following annotation is ignored. See leanprover/lean4#3126
+    let i : Q($ι) ← mkFreshExprMVarQ q($ι)
+    have body : Q($α) := Expr.betaRev f #[i]
     let so : Option Q(Finset.Nonempty $s) ← do
       try
         match s with
         | ~q(@univ _ $fi) => do
-          -- TODO(Qq): doesn't type-check without explicit `u`, even though it works outside the
-          -- `match`.
-          let _no ← synthInstanceQ (u := 0) q(Nonempty $ι)
+          let _no ← synthInstanceQ q(Nonempty $ι)
           return some q(Finset.univ_nonempty (α := $ι))
         | _ => throwError "`s` is not `univ`"
       catch _ => do
         let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
         pure (some (.fvar fv))
-    match ← core zα pα rhs, so with
+    match ← core zα pα body, so with
     | .nonnegative pb, _ => do
       let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
       assertInstancesCommute
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pb
       return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
     | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
       let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
       assertInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pb
       return .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi)
     | _, _ => pure .none
   | _ => throwError "not Finset.sum"

From 738c7cc7209c7e3ae897393ea4b294bfec13b788 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 12 Feb 2024 12:17:19 +0000
Subject: [PATCH 07/20] better logic

---
 Mathlib/Algebra/BigOperators/Order.lean | 50 ++++++++++++++-----------
 1 file changed, 29 insertions(+), 21 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 7377e923942e7..55bd254192013 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -833,28 +833,35 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   | ~q(@Finset.sum _ $ι $instα $s $f) =>
     let i : Q($ι) ← mkFreshExprMVarQ q($ι)
     have body : Q($α) := Expr.betaRev f #[i]
-    let so : Option Q(Finset.Nonempty $s) ← do
-      try
-        match s with
-        | ~q(@univ _ $fi) => do
-          let _no ← synthInstanceQ q(Nonempty $ι)
-          return some q(Finset.univ_nonempty (α := $ι))
-        | _ => throwError "`s` is not `univ`"
-      catch _ => do
-        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-        pure (some (.fvar fv))
-    match ← core zα pα body, so with
-    | .nonnegative pb, _ => do
+    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 positive
+      -- TODO: If we replace the next line by
+      -- let rs : Option Q(Finset.Nonempty $s) ← do
+      -- then the type-ascription is ignored
+      let (.some ps : Option Q(Finset.Nonempty $s)) ← do
+        try
+          match s with
+          | ~q(@univ _ $fi) => do
+            let _no ← synthInstanceQ q(Nonempty $ι)
+            return some q(Finset.univ_nonempty (α := $ι))
+          | _ => throwError "`s` is not `univ`"
+        catch _ => do
+          let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+          pure (some (.fvar fv))
+        | failure -- Fail if the body is not nonempty
+      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)
+    -- 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 pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pb
       return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
-    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-      let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
-      assertInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pb
-      return .positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi)
-    | _, _ => pure .none
   | _ => throwError "not Finset.sum"
 
 example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∑ j in range n, a j^2 := by positivity
@@ -864,7 +871,8 @@ example (n : ℕ) (a : ℕ → ℤ) : 0 < ∑ j : Fin (n + 1), (a j^2 + 1) := by
 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 ℕ) : 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
 
 end Mathlib.Meta.Positivity

From 4c0225b54a8a4a5db597c52561462e2916ee2749 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 12 Feb 2024 12:20:27 +0000
Subject: [PATCH 08/20] check for debug

---
 Mathlib/Algebra/BigOperators/Order.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 55bd254192013..ba13041f99d1c 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -839,7 +839,7 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       let .positive pbody := rbody | failure -- Fail if the body is not positive
       -- TODO: If we replace the next line by
       -- let rs : Option Q(Finset.Nonempty $s) ← do
-      -- then the type-ascription is ignored
+      -- then the type-ascription is ignored. See leanprover/lean4#3126
       let (.some ps : Option Q(Finset.Nonempty $s)) ← do
         try
           match s with
@@ -861,7 +861,9 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
       let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
       assertInstancesCommute
-      return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
+      let proof := q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
+      proof.check
+      return .nonnegative proof
   | _ => throwError "not Finset.sum"
 
 example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∑ j in range n, a j^2 := by positivity

From 22856978f2387cc73c780e2a1c793d8209e5549d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 12 Feb 2024 14:40:25 +0000
Subject: [PATCH 09/20] fix

---
 Mathlib/Algebra/BigOperators/Order.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index ba13041f99d1c..a37b00ac27575 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -831,7 +831,7 @@ TC inference. -/
 def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   match e with
   | ~q(@Finset.sum _ $ι $instα $s $f) =>
-    let i : Q($ι) ← mkFreshExprMVarQ q($ι)
+    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
@@ -876,5 +876,6 @@ example (a : ℕ → ℤ) : 0 < ∑ j in ({1} : Finset ℕ), (a j^2 + 1) := by
 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
+example (f : ℕ → ℕ) (hf₀ : 0 ≤ f 0) : 0 ≤ ∑ n in Finset.range 10, f n := by positivity
 
 end Mathlib.Meta.Positivity

From d7456a33c1d4026143cbf28b62a3759a118986b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 12 Feb 2024 14:48:29 +0000
Subject: [PATCH 10/20] remove unreachable failure

---
 Mathlib/Algebra/BigOperators/Order.lean | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index a37b00ac27575..f230967bfb85d 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -836,21 +836,21 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
     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 positive
+      let .positive pbody := rbody | failure -- Fail if the body is not provably positive
       -- TODO: If we replace the next line by
-      -- let rs : Option Q(Finset.Nonempty $s) ← do
+      -- let ps : Q(Finset.Nonempty $s) ← do
       -- then the type-ascription is ignored. See leanprover/lean4#3126
-      let (.some ps : Option Q(Finset.Nonempty $s)) ← do
+      let (ps : Q(Finset.Nonempty $s)) ← do
         try
           match s with
           | ~q(@univ _ $fi) => do
             let _no ← synthInstanceQ q(Nonempty $ι)
-            return some q(Finset.univ_nonempty (α := $ι))
+            return q(Finset.univ_nonempty (α := $ι))
           | _ => throwError "`s` is not `univ`"
         catch _ => do
-          let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-          pure (some (.fvar fv))
-        | failure -- Fail if the body is not nonempty
+          let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s)
+            | failure -- Fail if the set is not provably nonempty
+          pure (.fvar fv)
       let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
@@ -876,6 +876,10 @@ example (a : ℕ → ℤ) : 0 < ∑ j in ({1} : Finset ℕ), (a j^2 + 1) := by
 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
-example (f : ℕ → ℕ) (hf₀ : 0 ≤ f 0) : 0 ≤ ∑ n in Finset.range 10, f n := 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

From 6161d23cd32a7d5d7c7b098bb23808de81e5fff5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 12 Feb 2024 14:50:12 +0000
Subject: [PATCH 11/20] add todo

---
 Mathlib/Algebra/BigOperators/Order.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index f230967bfb85d..ee9515038917d 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -826,7 +826,14 @@ 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
-TC inference. -/
+TC inference.
+
+TODO: The following example does not work
+```
+example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum f := by positivity
+```
+because `compareHyp` can't look for assumptions behind binders.
+-/
 @[positivity Finset.sum _ _]
 def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
   match e with

From 92ec7dc00257659d5f445313e9e2cfec6ec35904 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Mon, 12 Feb 2024 14:55:21 +0000
Subject: [PATCH 12/20] revert AkraBazzi

---
 Mathlib/Computability/AkraBazzi/AkraBazzi.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
index 61a292bbee622..3dcd562e6a66c 100644
--- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
+++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@@ -1237,6 +1237,9 @@ lemma T_isBigO_smoothingFn_mul_asympBound :
                 * ((1 + (∑ u in range (r i n), g u / u ^ ((p a b) + 1)))))) + g n with i
             · have := R.a_pos i
               positivity
+            · refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_
+              rw [div_nonneg_iff]
+              exact Or.inl ⟨R.g_nonneg j (by positivity), by positivity⟩
             · exact bound1 n hn i
         _ = (∑ i, C * a i * ((b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)
                 * ((1 + ((∑ u in range n, g u / u ^ ((p a b) + 1))

From 5e8424fd358f7de00fa00d18c534082076f9c5f3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 13 Feb 2024 08:34:29 +0000
Subject: [PATCH 13/20] feat: Positivity extension for `Finset.prod` Followup
 to #9365

---
 Mathlib/Algebra/BigOperators/Order.lean | 165 ++++++++++++++++++------
 1 file changed, 122 insertions(+), 43 deletions(-)

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

From 72d04bdb23e90a254e96854ed8fefae5dc60afd9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 13 Feb 2024 21:36:46 +0000
Subject: [PATCH 14/20] golfs

---
 Mathlib/Analysis/Analytic/Composition.lean    |  4 +--
 Mathlib/Analysis/Analytic/Inverse.lean        |  3 +-
 .../NormedSpace/BoundedLinearMaps.lean        | 30 +++++++---------
 .../NormedSpace/Multilinear/Basic.lean        | 35 ++++++++-----------
 .../NormedSpace/Multilinear/Curry.lean        |  6 ++--
 Mathlib/Data/Nat/Choose/Multinomial.lean      |  2 +-
 Mathlib/Data/Nat/Factorial/BigOperators.lean  |  3 +-
 .../MeasureTheory/Integral/TorusIntegral.lean |  3 +-
 8 files changed, 34 insertions(+), 52 deletions(-)

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 : ℕ))]

From 4091f23e6955c142e795098373fbb22692336ae1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 22 Feb 2024 15:08:17 +0000
Subject: [PATCH 15/20] tests

---
 test/positivity.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test/positivity.lean b/test/positivity.lean
index 9afdc92492734..fcf3f409aa19c 100644
--- a/test/positivity.lean
+++ b/test/positivity.lean
@@ -355,6 +355,23 @@ 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
 
+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
+
 /- ## Other extensions -/
 
 example [Zero β] [PartialOrder β] [FunLike F α β] [NonnegHomClass F α β]

From e27d6525e6d52c452316d5f5d043632434471a5b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 23 Feb 2024 09:03:21 +0000
Subject: [PATCH 16/20] don't use @

---
 Mathlib/Algebra/BigOperators/Order.lean | 36 ++++++++++++-------------
 1 file changed, 17 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index bfa2d0ff4044d..185788e391c0b 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -868,9 +868,7 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
-/-- 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
+private alias ⟨_, prod_ne_zero⟩ := prod_ne_zero_iff
 
 /-- The `positivity` extension which proves that `∏ i in s, f i` is nonnegative if `f` is, and
 positive if each `f i` is.
@@ -891,33 +889,33 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
     -- 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 $α)
+      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      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)
+      pure $ .positive q(prod_pos 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 $α)
+      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      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)
+      pure $ .nonnegative q(prod_nonneg 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 $α)
+      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      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)
+      pure $ .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
   | _ => throwError "not Finset.prod"
 
 end Mathlib.Meta.Positivity

From 65e659322b808303e603c347a5e2ccc0fa6c9e41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 6 Mar 2024 12:18:56 +0000
Subject: [PATCH 17/20] Eric's no-monadic-failure paradigm

---
 Mathlib/Algebra/BigOperators/Order.lean | 38 +++++++++++++------------
 test/positivity.lean                    |  4 +++
 2 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 0dd56e0c3d0af..e778e8ad2f98b 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -885,36 +885,38 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
     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 p_pos : Option Q(0 < $e) := ← (do
+      let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
       -- TODO: We must name the following, else `assertInstancesCommute` loops.
-      let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
-      let _instαzeroone ← synthInstanceQ q(ZeroLEOneClass $α)
-      let _instαposmul ← synthInstanceQ q(PosMulStrictMono $α)
-      let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
+      let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      pure $ .positive q(prod_pos fun i _ ↦ $pr i)
-    -- Try to show that the sum is nonnegative
-    catch _ => try
-      let pbody ← rbody.toNonneg
+      return some q(prod_pos fun i _ ↦ $pr i))
+    -- Try to show that the product is positive
+    if let some p_pos := p_pos then return .positive p_pos
+    let p_nonneg : Option Q(0 ≤ $e) := ← (do
+      let .some pbody := rbody.toNonneg
+        | return none -- Fail if the body is not provably nonnegative
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
       -- TODO: We must name the following, else `assertInstancesCommute` loops.
-      let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
-      let _instαzeroone ← synthInstanceQ q(ZeroLEOneClass $α)
-      let _instαposmul ← synthInstanceQ q(PosMulMono $α)
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
       assertInstancesCommute
-      pure $ .nonnegative q(prod_nonneg fun i _ ↦ $pr i)
-    catch _ =>
+      return some q(prod_nonneg fun i _ ↦ $pr i))
+    -- Try to show that the product is nonnegative
+    if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
+    -- Fall back to showing that the product is nonzero
+    else
       let pbody ← rbody.toNonzero
       let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody
       -- TODO: We must name the following, else `assertInstancesCommute` loops.
-      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 fun i _ ↦ $pr i)
+      return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
   | _ => throwError "not Finset.prod"
 
 end Mathlib.Meta.Positivity
diff --git a/test/positivity.lean b/test/positivity.lean
index c99f20c2508f3..70682e4daa3c3 100644
--- a/test/positivity.lean
+++ b/test/positivity.lean
@@ -382,6 +382,10 @@ 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
 
+-- Make sure that `positivity` isn't too greedy by trying to prove that a product is positive
+-- because its body is even if multiplication isn't strictly monotone
+example [OrderedCommSemiring α] {a : α} (ha : 0 < a) : 0 ≤ ∏ _i in {(0 : α)}, a := by positivity
+
 /- ## Other extensions -/
 
 example [Zero β] [PartialOrder β] [FunLike F α β] [NonnegHomClass F α β]

From 700321489a26c0376c507795e1bddcd3a4270eef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 3 Apr 2024 20:15:33 +0000
Subject: [PATCH 18/20] suggestions

---
 Mathlib/Algebra/BigOperators/Order.lean       | 22 +++++++++----------
 .../NormedSpace/BoundedLinearMaps.lean        |  4 ++--
 .../NormedSpace/Multilinear/Basic.lean        | 12 +++++-----
 .../NormedSpace/Multilinear/Curry.lean        |  2 +-
 .../MeasureTheory/Integral/TorusIntegral.lean |  2 +-
 5 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index b9731324bb869..743f8ca6de7e8 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -891,38 +891,38 @@ 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) =>
+  | ~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
     let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
-    let p_pos : Option Q(0 < $e) := ← (do
+    let p_pos : Option Q(0 < $e) := ← do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
-      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
       let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
       let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
       let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
       assertInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      return some q(prod_pos fun i _ ↦ $pr i))
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      return some q(prod_pos fun i _ ↦ $pr i)
     -- Try to show that the product is positive
     if let some p_pos := p_pos then return .positive p_pos
-    let p_nonneg : Option Q(0 ≤ $e) := ← (do
+    let p_nonneg : Option Q(0 ≤ $e) := ← do
       let .some pbody := rbody.toNonneg
         | return none -- Fail if the body is not provably nonnegative
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
-      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
       let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
       let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
       assertInstancesCommute
-      return some q(prod_nonneg fun i _ ↦ $pr i))
+      return some q(prod_nonneg fun i _ ↦ $pr i)
     -- Try to show that the product is nonnegative
     if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
     -- Fall back to showing that the product is nonzero
     else
       let pbody ← rbody.toNonzero
-      let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody
-      -- TODO: We must name the following, else `assertInstancesCommute` loops.
+      let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
       let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
       let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
       assertInstancesCommute
diff --git a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean b/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
index b8c2ee5a7e338..7b3d216eabc67 100644
--- a/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
+++ b/Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
@@ -227,8 +227,8 @@ theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, NormedAdd
     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)
+    · 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 6dcb53903056f..a528ee6fa99ea 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -247,7 +247,7 @@ theorem continuous_of_bound (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m
   let D := max C 1
   have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
   replace H (m) : ‖f m‖ ≤ D * ∏ i, ‖m i‖ :=
-    (H m).trans (mul_le_mul_of_nonneg_right (le_max_left _ _) $ by positivity)
+    (H m).trans (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
@@ -804,8 +804,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 _ _) $ by positivity
+  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
@@ -1420,7 +1420,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
     · 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) $ by positivity
+      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)
@@ -1445,7 +1445,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 _ $ by positivity
+      apply mul_le_mul_of_nonneg_right _ <| by positivity
       calc
         ‖f n‖ = ‖f n - f 0 + f 0‖ := by
           congr 1
@@ -1465,7 +1465,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) $ by positivity
+      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 4a3ae43904233..7d8dfae58f146 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
@@ -63,7 +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 _) $ by positivity
+    _ ≤ ‖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]
diff --git a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
index 962f7a5f421c5..b27b7db6b8f65 100644
--- a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
@@ -199,7 +199,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 _) $ by positivity
+          _ ≤ (∏ 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 : ℕ))]

From bc25cf0021bf97471f75ccfd41dbbdf8b70620f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 4 Apr 2024 12:14:47 +0200
Subject: [PATCH 19/20] whitespace for clarity

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
---
 Mathlib/Algebra/BigOperators/Order.lean | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
index 743f8ca6de7e8..7bdb279c04ac5 100644
--- a/Mathlib/Algebra/BigOperators/Order.lean
+++ b/Mathlib/Algebra/BigOperators/Order.lean
@@ -896,6 +896,8 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
     have body : Q($α) := Expr.betaRev f #[i]
     let rbody ← core zα pα body
     let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+
+    -- Try to show that the product is positive
     let p_pos : Option Q(0 < $e) := ← do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
       -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
@@ -905,8 +907,9 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
       return some q(prod_pos fun i _ ↦ $pr i)
-    -- Try to show that the product is positive
     if let some p_pos := p_pos then return .positive p_pos
+
+    -- Try to show that the product is nonnegative
     let p_nonneg : Option Q(0 ≤ $e) := ← do
       let .some pbody := rbody.toNonneg
         | return none -- Fail if the body is not provably nonnegative
@@ -916,17 +919,15 @@ def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do
       let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
       assertInstancesCommute
       return some q(prod_nonneg fun i _ ↦ $pr i)
-    -- Try to show that the product is nonnegative
     if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
+
     -- Fall back to showing that the product is nonzero
-    else
-      let pbody ← rbody.toNonzero
-      let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
-      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
-      let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
-      let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
-      assertInstancesCommute
-      return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
-  | _ => throwError "not Finset.prod"
+    let pbody ← rbody.toNonzero
+    let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+    -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+    let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
+    let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
+    assertInstancesCommute
+    return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
 
 end Mathlib.Meta.Positivity

From e6a642de1e8d994d20324763198ae24a3358e86e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 5 Apr 2024 17:57:52 +0000
Subject: [PATCH 20/20] bump

---
 .../Order/BigOperators/Group/Finset.lean      | 53 -----------------
 .../Order/BigOperators/Ring/Finset.lean       | 58 +++++++++++++++++++
 2 files changed, 58 insertions(+), 53 deletions(-)

diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
index 99f3622fe68c1..bf023ad30ce61 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@@ -716,57 +716,4 @@ def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
       return .nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
-private alias ⟨_, prod_ne_zero⟩ := prod_ne_zero_iff
-
-/-- The `positivity` extension which proves that `∏ i in s, f i` is nonnegative if `f` is, and
-positive if each `f i` is.
-
-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
-    let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
-
-    -- Try to show that the product is positive
-    let p_pos : Option Q(0 < $e) := ← do
-      let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
-      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
-      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
-      let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
-      let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
-      assertInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
-      return some q(prod_pos fun i _ ↦ $pr i)
-    if let some p_pos := p_pos then return .positive p_pos
-
-    -- Try to show that the product is nonnegative
-    let p_nonneg : Option Q(0 ≤ $e) := ← do
-      let .some pbody := rbody.toNonneg
-        | return none -- Fail if the body is not provably nonnegative
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
-      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
-      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
-      let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
-      assertInstancesCommute
-      return some q(prod_nonneg fun i _ ↦ $pr i)
-    if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
-
-    -- Fall back to showing that the product is nonzero
-    let pbody ← rbody.toNonzero
-    let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
-    -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
-    let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
-    let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
-    assertInstancesCommute
-    return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
-
 end Mathlib.Meta.Positivity
diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
index c6236f42648f7..1182741966237 100644
--- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
@@ -207,3 +207,61 @@ lemma IsAbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCom
 #align is_absolute_value.map_prod IsAbsoluteValue.map_prod
 
 end AbsoluteValue
+
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
+
+private alias ⟨_, prod_ne_zero⟩ := prod_ne_zero_iff
+
+/-- The `positivity` extension which proves that `∏ i in s, f i` is nonnegative if `f` is, and
+positive if each `f i` is.
+
+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
+    let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
+
+    -- Try to show that the product is positive
+    let p_pos : Option Q(0 < $e) := ← do
+      let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulStrictMono $α) | pure none
+      let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      return some q(prod_pos fun i _ ↦ $pr i)
+    if let some p_pos := p_pos then return .positive p_pos
+
+    -- Try to show that the product is nonnegative
+    let p_nonneg : Option Q(0 ≤ $e) := ← do
+      let .some pbody := rbody.toNonneg
+        | return none -- Fail if the body is not provably nonnegative
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+      -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+      let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
+      let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
+      assertInstancesCommute
+      return some q(prod_nonneg fun i _ ↦ $pr i)
+    if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
+
+    -- Fall back to showing that the product is nonzero
+    let pbody ← rbody.toNonzero
+    let pr : Q(∀ i, $f i ≠ 0) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
+    -- TODO(quote4#38): We must name the following, else `assertInstancesCommute` loops.
+    let _instαnontriv ← synthInstanceQ q(Nontrivial $α)
+    let _instαnozerodiv ← synthInstanceQ q(NoZeroDivisors $α)
+    assertInstancesCommute
+    return .nonzero q(prod_ne_zero fun i _ ↦ $pr i)
+
+end Mathlib.Meta.Positivity