feat(data/finset,data/fintype,algebra/big_operators): some more lemmas (#3124)

Add some `finset`, `fintype` and `algebra.big_operators` lemmas that
were found useful in proving things related to affine independent
families.  (In all cases where results are proved for products, and
then derived for sums where possible using `to_additive`, it was the
result for sums that I actually had a use for.  In the case of
`eq_one_of_card_le_one_of_prod_eq_one` and
`eq_zero_of_card_le_one_of_sum_eq_zero`, `to_additive` couldn't be
used because it also tries to convert the `1` in `s.card ≤ 1` to `0`.)

Author: jsm28

src/algebra/big_operators.lean

@@ -752,6 +752,77 @@ lemma prod_update_of_mem [decidable_eq α] {s : finset α} {i : α} (h : i ∈ s
   (∏ x in s, function.update f i b x) = b * (∏ x in s \ (singleton i), f x) :=
 by { rw [update_eq_piecewise, prod_piecewise], simp [h] }
 
+/-- If a product of a `finset` of size at most 1 has a given value, so
+do the terms in that product. -/
+lemma eq_of_card_le_one_of_prod_eq {s : finset α} (hc : s.card ≤ 1) {f : α → β} {b : β}
+    (h : ∏ x in s, f x = b) : ∀ x ∈ s, f x = b :=
+begin
+  intros x hx,
+  by_cases hc0 : s.card = 0,
+  { exact false.elim (card_ne_zero_of_mem hx hc0) },
+  { have h1 : s.card = 1 := le_antisymm hc (nat.one_le_of_lt (nat.pos_of_ne_zero hc0)),
+    rw card_eq_one at h1,
+    cases h1 with x2 hx2,
+    rw [hx2, mem_singleton] at hx,
+    simp_rw hx2 at h,
+    rw hx,
+    rw prod_singleton at h,
+    exact h }
+end
+
+/-- If a sum of a `finset` of size at most 1 has a given value, so do
+the terms in that sum. -/
+lemma eq_of_card_le_one_of_sum_eq [add_comm_monoid γ] {s : finset α} (hc : s.card ≤ 1)
+    {f : α → γ} {b : γ} (h : ∑ x in s, f x = b) : ∀ x ∈ s, f x = b :=
+begin
+  intros x hx,
+  by_cases hc0 : s.card = 0,
+  { exact false.elim (card_ne_zero_of_mem hx hc0) },
+  { have h1 : s.card = 1 := le_antisymm hc (nat.one_le_of_lt (nat.pos_of_ne_zero hc0)),
+    rw card_eq_one at h1,
+    cases h1 with x2 hx2,
+    rw [hx2, mem_singleton] at hx,
+    simp_rw hx2 at h,
+    rw hx,
+    rw sum_singleton at h,
+    exact h }
+end
+
+attribute [to_additive eq_of_card_le_one_of_sum_eq] eq_of_card_le_one_of_prod_eq
+
+/-- If a function applied at a point is 1, a product is unchanged by
+removing that point, if present, from a `finset`. -/
+@[to_additive "If a function applied at a point is 0, a sum is unchanged by
+removing that point, if present, from a `finset`."]
+lemma prod_erase [decidable_eq α] (s : finset α) {f : α → β} {a : α} (h : f a = 1) :
+  ∏ x in s.erase a, f x = ∏ x in s, f x :=
+begin
+  rw ←sdiff_singleton_eq_erase,
+  apply prod_subset sdiff_subset_self,
+  intros x hx hnx,
+  rw sdiff_singleton_eq_erase at hnx,
+  rwa eq_of_mem_of_not_mem_erase hx hnx
+end
+
+/-- If a product is 1 and the function is 1 except possibly at one
+point, it is 1 everywhere on the `finset`. -/
+@[to_additive "If a sum is 0 and the function is 0 except possibly at one
+point, it is 0 everywhere on the `finset`."]
+lemma eq_one_of_prod_eq_one {s : finset α} {f : α → β} {a : α} (hp : ∏ x in s, f x = 1)
+    (h1 : ∀ x ∈ s, x ≠ a → f x = 1) : ∀ x ∈ s, f x = 1 :=
+begin
+  intros x hx,
+  classical,
+  by_cases h : x = a,
+  { rw h,
+    rw h at hx,
+    rw [←prod_subset (singleton_subset_iff.2 hx)
+                      (λ t ht ha, h1 t ht (not_mem_singleton.1 ha)),
+        prod_singleton] at hp,
+    exact hp },
+  { exact h1 x hx h }
+end
+
 end comm_monoid
 
 lemma sum_update_of_mem [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α}

src/data/finset.lean

@@ -580,6 +580,15 @@ theorem mem_of_mem_erase {a b : α} {s : finset α} : b ∈ erase s a → b ∈
 theorem mem_erase_of_ne_of_mem {a b : α} {s : finset α} : a ≠ b → a ∈ s → a ∈ erase s b :=
 by simp only [mem_erase]; exact and.intro
 
+/-- An element of `s` that is not an element of `erase s a` must be
+`a`. -/
+lemma eq_of_mem_of_not_mem_erase {a b : α} {s : finset α} (hs : b ∈ s)
+    (hsa : b ∉ s.erase a) : b = a :=
+begin
+  rw [mem_erase, not_and] at hsa,
+  exact not_imp_not.mp hsa hs
+end
+
 theorem erase_insert {a : α} {s : finset α} (h : a ∉ s) : erase (insert a s) a = s :=
 ext $ assume x, by simp only [mem_erase, mem_insert, and_or_distrib_left, not_and_self, false_or];
 apply and_iff_right_of_imp; rintro H rfl; exact h H

src/data/fintype/basic.lean

@@ -521,6 +521,10 @@ begin
     exact subtype.eq (H x.2 y.2) }
 end
 
+/-- A `finset` of a subsingleton type has cardinality at most one. -/
+lemma finset.card_le_one_of_subsingleton [subsingleton α] (s : finset α) : s.card ≤ 1 :=
+finset.card_le_one_iff.2 $ λ _ _ _ _, subsingleton.elim _ _
+
 lemma finset.one_lt_card_iff {s : finset α} :
   1 < s.card ↔ ∃ x y, (x ∈ s) ∧ (y ∈ s) ∧ x ≠ y :=
 begin

src/data/fintype/card.lean

@@ -58,6 +58,14 @@ lemma prod_unique [unique β] (f : β → M) :
   (∏ x, f x) = f (default β) :=
 by simp only [finset.prod_singleton, univ_unique]
 
+/-- If a product of a `finset` of a subsingleton type has a given
+value, so do the terms in that product. -/
+@[to_additive "If a sum of a `finset` of a subsingleton type has a given
+value, so do the terms in that sum."]
+lemma eq_of_subsingleton_of_prod_eq {ι : Type*} [subsingleton ι] {s : finset ι}
+    {f : ι → M} {b : M} (h : ∏ i in s, f i = b) : ∀ i ∈ s, f i = b :=
+finset.eq_of_card_le_one_of_prod_eq (finset.card_le_one_of_subsingleton s) h
+
 end
 
 end fintype