chore(Algebra): generalise prod_le_prod_of_subset_of_one_le

Author: YaelDillies

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -129,37 +129,40 @@ theorem prod_le_one' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s,
   (prod_le_prod' h).trans_eq (by rw [prod_const_one])
 
 @[to_additive (attr := gcongr) sum_le_sum_of_subset_of_nonneg]
-theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t)
-    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
+lemma prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hg : ∀ i ∈ t, i ∉ s → 1 ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, g i := by
   classical calc
-      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
-      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
-      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
+    ∏ i ∈ s, f i
+    _ ≤ ∏ i ∈ s, g i := by gcongr with i hi; exact hfg i hi
+    _ ≤ (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i :=
+      le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
+    _ = ∏ i ∈ t \ s ∪ s, g i := (prod_union sdiff_disjoint).symm
+    _ = ∏ i ∈ t, g i := by rw [sdiff_union_of_subset h]
 
 @[to_additive]
 theorem prod_le_prod_of_subset_of_le_one'
     {ι : Type u_1} {N : Type u_5} [CommMonoid N] [Preorder N]
-    {f : ι → N} {s t : Finset ι} [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
-    ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i :=
-  prod_le_prod_of_subset_of_one_le' (N := Nᵒᵈ) h hf
+    {f g : ι → N} {s t : Finset ι} [MulLeftMono N] (h : s ⊆ t) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
+    ∏ i ∈ t, f i ≤ ∏ i ∈ s, g i :=
+  prod_le_prod_of_subset_of_one_le' (N := Nᵒᵈ) h hfg hf
 
 @[to_additive sum_mono_set_of_nonneg]
 theorem prod_mono_set_of_one_le' [MulLeftMono N] (hf : ∀ x, 1 ≤ f x) :
     Monotone fun s ↦ ∏ x ∈ s, f x :=
-  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le' hst fun x _ _ ↦ hf x
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le' hst (by simp) fun x _ _ ↦ hf x
 
 @[to_additive]
 theorem prod_anti_set_of_le_one'
     {ι : Type u_1} {N : Type u_5} [CommMonoid N] [Preorder N]
     {f : ι → N} [MulLeftMono N] (hf : ∀ (x : ι), f x ≤ 1) :
     Antitone fun (s : Finset ι) => ∏ x ∈ s, f x :=
-  fun _ _ hst ↦ prod_le_prod_of_subset_of_le_one' hst (by simp [hf])
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_le_one' hst (by simp) (by simp [hf])
 
 @[to_additive sum_le_univ_sum_of_nonneg]
 theorem prod_le_univ_prod_of_one_le' [MulLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) :
     ∏ x ∈ s, f x ≤ ∏ x, f x :=
-  prod_le_prod_of_subset_of_one_le' (subset_univ s) fun a _ _ ↦ w a
+  prod_le_prod_of_subset_of_one_le' (subset_univ s) (by simp) fun a _ _ ↦ w a
 
 @[to_additive sum_eq_zero_iff_of_nonneg]
 theorem prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
@@ -199,7 +202,7 @@ theorem single_le_prod' [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a
   calc
     f a = ∏ i ∈ {a}, f i := (prod_singleton _ _).symm
     _ ≤ ∏ i ∈ s, f i :=
-      prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hi
+      prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) (by simp) fun i hi _ ↦ hf i hi
 
 @[to_additive]
 lemma mul_le_prod [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s)
@@ -208,7 +211,7 @@ lemma mul_le_prod [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi :
   calc
     f i * f j = ∏ k ∈ .cons i {j} (by simpa), f k := by rw [prod_cons, prod_singleton]
     _ ≤ ∏ k ∈ s, f k := by
-      refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
+      refine prod_le_prod_of_subset_of_one_le' ?_ (by simp) fun k hk _ ↦ hf k hk
       simp [cons_subset, *]
 
 @[to_additive sum_le_card_nsmul]
@@ -235,7 +238,7 @@ theorem prod_fiberwise_le_prod_of_one_le_prod_fiber' [MulLeftMono N] {t : Finset
   calc
     (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤
         ∏ y ∈ t ∪ s.image g, ∏ x ∈ s with g x = y, f x :=
-      prod_le_prod_of_subset_of_one_le' subset_union_left fun y _ ↦ h y
+      prod_le_prod_of_subset_of_one_le' subset_union_left (by simp) fun y _ ↦ h y
     _ = ∏ x ∈ s, f x :=
       prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _
 
@@ -418,7 +421,7 @@ lemma single_le_prod_of_canonicallyOrdered {i : ι} (hi : i ∈ s) :
 @[to_additive sum_le_sum_of_subset]
 theorem prod_le_prod_of_subset' (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-  prod_le_prod_of_subset_of_one_le' h fun _ _ _ ↦ one_le
+  prod_le_prod_of_subset_of_one_le' h (by simp) fun _ _ _ ↦ one_le
 
 @[to_additive sum_mono_set]
 theorem prod_mono_set' (f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hs ↦
@@ -478,7 +481,7 @@ theorem prod_lt_prod_of_subset' [MulLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht
       rw [prod_insert hs]
       exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
     _ ≤ ∏ j ∈ t, f j := by
-      apply prod_le_prod_of_subset_of_one_le'
+      refine prod_le_prod_of_subset_of_one_le' ?_ (by simp) ?_
       · simp [Finset.insert_subset_iff, h, ht]
       · intro x hx h'x
         simp only [mem_insert, not_or] at h'x

Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean

@@ -68,15 +68,18 @@ lemma le_prod_max_one {M : Type*} [CommMonoidWithZero M] [LinearOrder M] [ZeroLE
 
 @[gcongr]
 theorem prod_le_prod_of_subset_of_one_le (h : s ⊆ t)
-    (hf0 : ∀ i ∈ s, 0 ≤ f i)
-    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
+    (hf0 : ∀ i ∈ s, 0 ≤ f i) (hfg : ∀ i ∈ s, f i ≤ g i)
+    (hf : ∀ i ∈ t, i ∉ s → 1 ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, g i := by
   have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
   classical
   calc
-      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
-      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
-      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
+      ∏ i ∈ s, f i
+    _ ≤ ∏ i ∈ s, g i := by gcongr with i hi; exacts [hf0, hfg i hi]
+    _ ≤ (∏ i ∈ t \ s, g i) * ∏ i ∈ s, g i :=
+      le_mul_of_one_le_left (prod_nonneg fun i hi ↦ (hf0 i hi).trans (hfg i hi)) <|
+        one_le_prod <| by simpa only [mem_sdiff, and_imp]
+    _ = ∏ i ∈ t \ s ∪ s, g i := (prod_union sdiff_disjoint).symm
+    _ = ∏ i ∈ t, g i := by rw [sdiff_union_of_subset h]
 
 theorem prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤ f i)
     (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
@@ -92,7 +95,7 @@ theorem prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤
 theorem prod_mono_set_of_one_le (hf : ∀ x, 1 ≤ f x) :
     Monotone fun s ↦ ∏ x ∈ s, f x :=
   fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le hst
-    (fun i _ ↦ zero_le_one.trans (hf i)) (fun x _ _ ↦ hf x)
+    (fun i _ ↦ zero_le_one.trans (hf i)) (by simp) (fun x _ _ ↦ hf x)
 
 theorem prod_anti_set_of_le_one (hf0 : ∀ (x : ι), 0 ≤ f x) (hf : ∀ (x : ι), f x ≤ 1) :
     Antitone fun (s : Finset ι) => ∏ x ∈ s, f x :=

Mathlib/Analysis/Complex/Exponential.lean

@@ -247,8 +247,7 @@ theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i ∈ rang
       refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
       simp only [exp', const_apply, re_sum]
       norm_cast
-      refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_
-      positivity
+      gcongr
     _ = exp x := by rw [exp, Complex.exp, ← cauSeqRe, lim_re]
 
 lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=

Mathlib/NumberTheory/Primorial.lean

@@ -53,7 +53,7 @@ theorem primorial_pos (n : ℕ) : 0 < n# :=
   prod_pos fun _p hp ↦ (mem_filter.1 hp).2.pos
 
 theorem primorial_mono {m n : ℕ} (h : m ≤ n) : m# ≤ n# :=
-  prod_le_prod_of_subset_of_one_le' (by gcongr) (by grind)
+  prod_le_prod_of_subset_of_one_le' (by gcongr) (by simp) (by grind)
 
 theorem primorial_monotone : Monotone primorial := fun _ _ ↦ primorial_mono
 

Mathlib/Topology/Algebra/InfiniteSum/Order.lean

@@ -93,7 +93,7 @@ protected lemma Multipliable.tprod_subtype_le {κ γ : Type*} [CommGroup γ] [Pa
 theorem prod_le_hasProd [L.NeBot] [L.LeAtTop] (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i)
     (hf : HasProd f a L) : ∏ i ∈ s, f i ≤ a := by
   refine ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_
-  exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩
+  exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst (by simp) fun i _ hbs ↦ hs i hbs⟩
 
 @[to_additive]
 theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (hf : HasProd f a) :