feat(data/list/big_operators): add list.sublist.prod_le_prod' etc (#…

…13879)

* add `list.forall₂.prod_le_prod'`, `list.sublist.prod_le_prod'`, and `list.sublist_forall₂.prod_le_prod'`;
* add their additive versions;
* upgrade `list.forall₂_same` to an `iff`.

src/data/list/big_operators.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import algebra.group_power
-import data.list.basic
+import data.list.forall2
 
 /-!
 # Sums and products from lists
@@ -193,15 +193,46 @@ lemma _root_.commute.list_sum_left [non_unital_non_assoc_semiring R] (b : R) (l
   commute l.sum b :=
 (commute.list_sum_right _ _ $ λ x hx, (h _ hx).symm).symm
 
+@[to_additive sum_le_sum] lemma forall₂.prod_le_prod' [preorder M]
+  [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
+  {l₁ l₂ : list M} (h : forall₂ (≤) l₁ l₂) : l₁.prod ≤ l₂.prod :=
+begin
+  induction h with a b la lb hab ih ih',
+  { refl },
+  { simpa only [prod_cons] using mul_le_mul' hab ih' }
+end
+
+/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
+`l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
+of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/
+@[to_additive sum_le_sum "If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
+then `l₁.sum ≤ l₂.sum`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead
+of `∀ a ∈ l₂, 0 ≤ a` but this lemma is not yet in `mathlib`."]
+lemma sublist.prod_le_prod' [preorder M] [covariant_class M M (function.swap (*)) (≤)]
+  [covariant_class M M (*) (≤)] {l₁ l₂ : list M} (h : l₁ <+ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) :
+  l₁.prod ≤ l₂.prod :=
+begin
+  induction h, { refl },
+  case cons : l₁ l₂ a ih ih'
+  { simp only [prod_cons, forall_mem_cons] at h₁ ⊢,
+    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1) },
+  case cons2 : l₁ l₂ a ih ih'
+  { simp only [prod_cons, forall_mem_cons] at h₁ ⊢,
+    exact mul_le_mul_left' (ih' h₁.2) _ }
+end
+
+@[to_additive sum_le_sum] lemma sublist_forall₂.prod_le_prod' [preorder M]
+  [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
+  {l₁ l₂ : list M} (h : sublist_forall₂ (≤) l₁ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) :
+  l₁.prod ≤ l₂.prod :=
+let ⟨l, hall, hsub⟩ := sublist_forall₂_iff.1 h
+in hall.prod_le_prod'.trans $ hsub.prod_le_prod' h₁
+
 @[to_additive sum_le_sum] lemma prod_le_prod' [preorder M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
   {l : list ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :
   (l.map f).prod ≤ (l.map g).prod :=
-begin
-  induction l with i l ihl, { refl },
-  rw forall_mem_cons at h,
-  simpa using mul_le_mul' h.1 (ihl h.2)
-end
+forall₂.prod_le_prod' $ by simpa
 
 @[to_additive sum_lt_sum] lemma prod_lt_prod'
   [preorder M] [covariant_class M M (*) (<)] [covariant_class M M (*) (≤)]
@@ -401,14 +432,7 @@ le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)
 @[to_additive] lemma prod_eq_one_iff [canonically_ordered_monoid M] (l : list M) :
   l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
 ⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
-begin
-  induction l,
-  { simp },
-  { intro h,
-    rw [prod_cons, mul_eq_one_iff],
-    rw forall_mem_cons at h,
-    exact ⟨h.1, l_ih h.2⟩ },
-end⟩
+  λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
 
 /-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
 by the sum of the elements. -/

src/data/list/forall2.lean

@@ -40,16 +40,14 @@ lemma forall₂.flip : ∀ {a b}, forall₂ (flip r) b a → forall₂ r a b
 | _ _                 forall₂.nil          := forall₂.nil
 | (a :: as) (b :: bs) (forall₂.cons h₁ h₂) := forall₂.cons h₁ h₂.flip
 
-lemma forall₂_same {r : α → α → Prop} : ∀ {l}, (∀ x∈l, r x x) → forall₂ r l l
-| []        _ := forall₂.nil
-| (a :: as) h := forall₂.cons
-    (h _ (mem_cons_self _ _))
-    (forall₂_same $ λ a ha, h a $ mem_cons_of_mem _ ha)
+@[simp] lemma forall₂_same {r : α → α → Prop} : ∀ {l : list α}, forall₂ r l l ↔ ∀ x ∈ l, r x x
+| [] := by simp
+| (a :: l) := by simp [@forall₂_same l]
 
 lemma forall₂_refl {r} [is_refl α r] (l : list α) : forall₂ r l l :=
-forall₂_same $ λ a h, is_refl.refl _
+forall₂_same.2 $ λ a h, refl _
 
-lemma forall₂_eq_eq_eq : forall₂ ((=) : α → α → Prop) = (=) :=
+@[simp] lemma forall₂_eq_eq_eq : forall₂ ((=) : α → α → Prop) = (=) :=
 begin
   funext a b, apply propext,
   split,

src/data/multiset/powerset.lean

@@ -125,8 +125,8 @@ theorem revzip_powerset_aux_lemma [decidable_eq α] (l : list α)
 begin
   have : forall₂ (λ (p : multiset α × multiset α) (s : multiset α), p = (s, ↑l - s))
     (revzip l') ((revzip l').map prod.fst),
-  { rw forall₂_map_right_iff,
-    apply forall₂_same, rintro ⟨s, t⟩ h,
+  { rw [forall₂_map_right_iff, forall₂_same],
+    rintro ⟨s, t⟩ h,
     dsimp, rw [← H h, add_tsub_cancel_left] },
   rw [← forall₂_eq_eq_eq, forall₂_map_right_iff], simpa
 end

src/order/well_founded_set.lean

@@ -684,19 +684,7 @@ begin
     { exact hl _ hy },
     { exact hl' _ hy } },
   apply ((h.partially_well_ordered_on_sublist_forall₂ (≤)).image_of_monotone_on _).mono hl,
-  intros l1 l2 hl1 hl2 h12,
-  obtain ⟨l, hll1, hll2⟩ := list.sublist_forall₂_iff.1 h12,
-  refine le_trans (list.rel_prod (le_refl 1) (λ a b ab c d cd, mul_le_mul' ab cd) hll1) _,
-  obtain ⟨l', hl'⟩ := hll2.exists_perm_append,
-  rw [hl'.prod_eq, list.prod_append, ← mul_one l.prod, mul_assoc, one_mul],
-  apply mul_le_mul_left',
-  have hl's := λ x hx, hl2 x (list.subset.trans (l.subset_append_right _) hl'.symm.subset hx),
-  clear hl',
-  induction l' with x1 x2 x3 x4 x5,
-  { refl },
-  rw [list.prod_cons, ← one_mul (1 : α)],
-  exact mul_le_mul' (hpos x1 (hl's x1 (list.mem_cons_self x1 x2)))
-    (x3 (λ x hx, hl's x (list.mem_cons_of_mem _ hx)))
+  exact λ l1 l2 hl1 hl2 h12, h12.prod_le_prod' (λ x hx, hpos x $ hl2 x hx)
 end
 
 end is_pwo