feat(*): some simple lemmas about sets and finite sets

src/algebra/big_operators.lean

@@ -177,6 +177,13 @@ have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1),
   from prod_congr rfl $ by simpa only [mem_sdiff, and_imp],
 by rw [←prod_sdiff h]; simp only [this, prod_const_one, one_mul]
 
+-- If we use `decidable_eq β` here, some rewrites fail because they find a wrong `decidable`
+-- instance first
+@[to_additive]
+lemma prod_filter_ne_one [∀ x, decidable (f x ≠ 1)] : (s.filter $ λx, f x ≠ 1).prod f = s.prod f :=
+prod_subset (filter_subset _) $ λ x,
+  by { classical, rw [not_imp_comm, mem_filter], exact and.intro }
+
 @[to_additive]
 lemma prod_filter (p : α → Prop) [decidable_pred p] (f : α → β) :
   (s.filter p).prod f = s.prod (λa, if p a then f a else 1) :=
@@ -252,9 +259,8 @@ lemma prod_bij_ne_one {s : finset α} {t : finset γ} {f : α → β} {g : γ 
   (hi₃ : ∀b∈t, g b ≠ 1 → ∃a h₁ h₂, b = i a h₁ h₂)
   (h : ∀a h₁ h₂, f a = g (i a h₁ h₂)) :
   s.prod f = t.prod g :=
-by haveI := classical.prop_decidable; exact
-calc s.prod f = (s.filter $ λx, f x ≠ 1).prod f :
-    (prod_subset (filter_subset _) $ by simp only [not_imp_comm, mem_filter]; exact λ _, and.intro).symm
+by classical; exact
+calc s.prod f = (s.filter $ λx, f x ≠ 1).prod f : prod_filter_ne_one.symm
   ... = (t.filter $ λx, g x ≠ 1).prod g :
     prod_bij (assume a ha, i a (mem_filter.mp ha).1 (mem_filter.mp ha).2)
       (assume a ha, (mem_filter.mp ha).elim $ λh₁ h₂, mem_filter.mpr
@@ -264,19 +270,20 @@ calc s.prod f = (s.filter $ λx, f x ≠ 1).prod f :
         (mem_filter.mp ha₁).elim $ λha₁₁ ha₁₂, (mem_filter.mp ha₂).elim $ λha₂₁ ha₂₂, hi₂ a₁ a₂ _ _ _ _)
       (assume b hb, (mem_filter.mp hb).elim $ λh₁ h₂,
         let ⟨a, ha₁, ha₂, eq⟩ := hi₃ b h₁ h₂ in ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩)
-  ... = t.prod g :
-    (prod_subset (filter_subset _) $ by simp only [not_imp_comm, mem_filter]; exact λ _, and.intro)
+  ... = t.prod g : prod_filter_ne_one
 
 @[to_additive]
-lemma exists_ne_one_of_prod_ne_one : s.prod f ≠ 1 → ∃a∈s, f a ≠ 1 :=
-by haveI := classical.dec_eq α; exact
-finset.induction_on s (λ H, (H rfl).elim) (assume a s has ih h,
-  classical.by_cases
-    (assume ha : f a = 1,
-      let ⟨a, ha, hfa⟩ := ih (by rwa [prod_insert has, ha, one_mul] at h) in
-      ⟨a, mem_insert_of_mem ha, hfa⟩)
-    (assume hna : f a ≠ 1,
-      ⟨a, mem_insert_self _ _, hna⟩))
+lemma nonempty_of_prod_ne_one : s.prod f ≠ 1 → ∃ x, x ∈ s :=
+by { refine λ h, exists_mem_of_ne_empty $ mt _ h, exact λ hs, hs.symm ▸ prod_empty }
+
+@[to_additive]
+lemma exists_ne_one_of_prod_ne_one (h : s.prod f ≠ 1) : ∃a∈s, f a ≠ 1 :=
+begin
+  classical,
+  rw ← prod_filter_ne_one at h,
+  rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩,
+  exact ⟨x, (mem_filter.1 hx).1, (mem_filter.1 hx).2⟩
+end
 
 @[to_additive]
 lemma prod_range_succ (f : ℕ → β) (n : ℕ) :
@@ -654,6 +661,36 @@ calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x 
 
 end canonically_ordered_monoid
 
+section ordered_cancel_comm_monoid
+
+variables [ordered_cancel_comm_monoid β]
+
+theorem sum_lt_sum (Hle : ∀ i ∈ s, f i ≤ g i) (Hlt : ∃ i ∈ s, f i < g i) :
+  s.sum f < s.sum g :=
+begin
+  classical,
+  rcases Hlt with ⟨i, hi, hlt⟩,
+  rw [← insert_erase hi, sum_insert (not_mem_erase _ _), sum_insert (not_mem_erase _ _)],
+  exact add_lt_add_of_lt_of_le hlt (sum_le_sum $ λ j hj, Hle j  $ mem_of_mem_erase hj)
+end
+
+end ordered_cancel_comm_monoid
+
+section decidable_linear_ordered_cancel_comm_monoid
+
+variables [decidable_linear_ordered_cancel_comm_monoid β]
+
+theorem exists_le_of_sum_le (hs : s ≠ ∅) (Hle : s.sum f ≤ s.sum g) :
+  ∃ i ∈ s, f i ≤ g i :=
+begin
+  classical,
+  contrapose! Hle with Hlt,
+  rcases exists_mem_of_ne_empty hs with ⟨i, hi⟩,
+  exact sum_lt_sum (λ i hi, le_of_lt (Hlt i hi)) ⟨i, hi, Hlt i hi⟩
+end
+
+end decidable_linear_ordered_cancel_comm_monoid
+
 section linear_ordered_comm_ring
 variables [decidable_eq α] [linear_ordered_comm_ring β]
 
@@ -704,16 +741,10 @@ calc s.card = (s.image f).sum (λ a, (s.filter (λ x, f x = a)).card) :
 ... ≤ (s.image f).sum (λ _, n) : sum_le_sum hn
 ... = _ : by simp [mul_comm]
 
-@[simp] lemma prod_Ico_id_eq_fact (n : ℕ) : (Ico 1 n.succ).prod (λ x, x) = nat.fact n :=
-calc (Ico 1 n.succ).prod (λ x, x) = (range n).prod nat.succ :
-eq.symm (prod_bij (λ x _, nat.succ x)
-  (λ a h₁, by simp [*, nat.lt_succ_iff, nat.succ_le_iff] at *)
-  (by simp) (λ _ _ _ _, nat.succ_inj)
-  (λ b h,
-    have b.pred.succ = b, from nat.succ_pred_eq_of_pos $
-      by simp [nat.pos_iff_ne_zero, nat.succ_le_iff] at *; tauto,
-    ⟨nat.pred b, mem_range.2 $ nat.lt_of_succ_lt_succ (by simp [*] at *), this.symm⟩))
-... = nat.fact n : by induction n; simp [*, range_succ]
+@[simp] lemma prod_Ico_id_eq_fact : ∀ n : ℕ, (Ico 1 n.succ).prod (λ x, x) = nat.fact n
+| 0 := rfl
+| (n+1) := by rw [prod_Ico_succ_top $ nat.succ_le_succ $ zero_le n,
+  nat.fact_succ, prod_Ico_id_eq_fact n, nat.succ_eq_add_one, mul_comm]
 
 end finset
 

src/algebra/module.lean

@@ -460,7 +460,31 @@ begin
     rw [add_smul, add_smul, one_smul, ih, one_smul] }
 end
 
-lemma finset.sum_const' {α : Type*} (R : Type*) [ring R] {β : Type*}
+namespace finset
+
+lemma sum_const' {α : Type*} (R : Type*) [ring R] {β : Type*}
   [add_comm_group β] [module R β] {s : finset α} (b : β) :
   finset.sum s (λ (a : α), b) = (finset.card s : R) • b :=
 by rw [finset.sum_const, ← module.smul_eq_smul]; refl
+
+variables {M : Type*} [decidable_linear_ordered_cancel_comm_monoid M]
+  {s : finset α} (f : α → M)
+
+theorem exists_card_smul_le_sum (hs : s ≠ ∅) :
+  ∃ i ∈ s, s.card • f i ≤ s.sum f :=
+begin
+  apply exists_le_of_sum_le hs,
+  simp only [sum_smul, sum_const],
+  refl
+end
+
+theorem exists_card_smul_ge_sum (hs : s ≠ ∅) :
+  ∃ i ∈ s, s.sum f ≤ s.card • f i :=
+begin
+  apply exists_le_of_sum_le hs,
+  simp only [sum_smul, sum_const],
+  refl
+end
+
+end finset
+

src/data/fintype.lean

@@ -221,6 +221,28 @@ instance (n : ℕ) : fintype (fin n) :=
 @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
 list.length_fin_range n
 
+lemma fin.univ_succ (n : ℕ) :
+  (univ : finset (fin $ n+1)) = insert 0 (univ.image fin.succ) :=
+begin
+  ext m,
+  simp only [mem_univ, mem_insert, true_iff, mem_image, exists_prop],
+  exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m
+end
+
+theorem fin.prod_univ_succ [comm_monoid β] {n} (f : fin (n+1) → β) :
+  univ.prod f = f 0 * univ.prod (λ i:fin n, f i.succ) :=
+begin
+  rw [fin.univ_succ, prod_insert, prod_image],
+  { intros x _ y _ hxy, exact fin.succ.inj hxy },
+  { simpa using fin.succ_ne_zero }
+end
+
+theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : univ.prod f = 1 := rfl
+
+theorem fin.sum_univ_succ [add_comm_monoid β] {n} (f : fin (n+1) → β) :
+  univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
+by apply @fin.prod_univ_succ (multiplicative β)
+
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
 

src/data/set/lattice.lean

@@ -11,8 +11,8 @@ import tactic.finish data.sigma.basic order.galois_connection
 
 open function tactic set lattice auto
 
-universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
+universes u v w x y
+variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {ι' : Sort y}
 
 namespace set
 
@@ -92,20 +92,32 @@ theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (
 -- TODO: should be simpler when sets' order is based on lattices
 @supr_le (set β) _ set.lattice_set _ _ h
 
-theorem Union_subset_iff {α : Sort u} {s : α → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t) :=
+theorem Union_subset_iff {s : ι → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t) :=
 ⟨assume h i, subset.trans (le_supr s _) h, Union_subset⟩
 
-theorem mem_Inter_of_mem {α : Sort u} {x : β} {s : α → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
+theorem mem_Inter_of_mem {x : β} {s : ι → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
 mem_Inter.2
 
-theorem subset_Inter {t : set β} {s : α → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
+theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
 -- TODO: should be simpler when sets' order is based on lattices
 @le_infi (set β) _ set.lattice_set _ _ h
 
 theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
 
 theorem Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le
 
+lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι)
+  (h : s i ⊆ t) : (⋂ i, s i) ⊆ t :=
+set.subset.trans (set.Inter_subset s i) h
+
+lemma Inter_subset_Inter {s t : ι → set α} (h : ∀ i, s i ⊆ t i) :
+  (⋂ i, s i) ⊆ (⋂ i, t i) :=
+set.subset_Inter $ λ i, set.Inter_subset_of_subset i (h i)
+
+lemma Inter_subset_Inter2 {s : ι → set α} {t : ι' → set α} (h : ∀ j, ∃ i, s i ⊆ t j) :
+  (⋂ i, s i) ⊆ (⋂ j, t j) :=
+set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi
+
 theorem Union_const [inhabited ι] (s : set β) : (⋃ i:ι, s) = s :=
 ext $ by simp
 
@@ -200,8 +212,7 @@ show (⨆ x ∈ s, u x) ≤ t, -- TODO: should not be necessary when sets' order
 
 theorem subset_bInter {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, t ⊆ u x) :
   t ⊆ (⋂ x ∈ s, u x) :=
-show t ≤ (⨅ x ∈ s, u x), -- TODO: should not be necessary when sets' order is based on lattices
-  from le_infi $ assume x, le_infi (h x)
+subset_Inter $ assume x, subset_Inter $ h x
 
 theorem subset_bUnion_of_mem {s : set α} {u : α → set β} {x : α} (xs : x ∈ s) :
   u x ⊆ (⋃ x ∈ s, u x) :=