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; `{∀x, decidable (f x ≠ 1)}` doesn't work with `rw ← prod_filter_ne_one`
+@[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 (h : s.prod f ≠ 1) : s.nonempty :=
+s.eq_empty_or_nonempty.elim (λ H, false.elim $ h $ H.symm ▸ prod_empty) id
+
+@[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 : ℕ) :
@@ -388,8 +395,8 @@ by haveI := classical.dec_eq α;
 haveI := classical.dec_eq β; exact
 finset.strong_induction_on s
   (λ s ih g h₁ h₂ h₃ h₄,
-    if hs : s = ∅ then hs.symm ▸ rfl
-    else let ⟨x, hx⟩ := exists_mem_of_ne_empty hs in
+    s.eq_empty_or_nonempty.elim (λ hs, hs.symm ▸ rfl)
+      (λ ⟨x, hx⟩,
       have hmem : ∀ y ∈ (s.erase x).erase (g x hx), y ∈ s,
         from λ y hy, (mem_of_mem_erase (mem_of_mem_erase hy)),
       have g_inj : ∀ {x hx y hy}, g x hx = g y hy → x = y,
@@ -414,7 +421,7 @@ finset.strong_induction_on s
             (λ h, h₁ x hx ▸ h ▸ hx1.symm ▸ (one_mul _).symm)))
       else by rw [← insert_erase hx, prod_insert (not_mem_erase _ _),
         ← insert_erase (mem_erase.2 ⟨h₂ x hx hx1, h₃ x hx⟩),
-        prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx])
+        prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx]))
 
 @[to_additive]
 lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 :=
@@ -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.nonempty) (Hle : s.sum f ≤ s.sum g) :
+  ∃ i ∈ s, f i ≤ g i :=
+begin
+  classical,
+  contrapose! Hle with Hlt,
+  rcases 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.nonempty) :
+  ∃ 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.nonempty) :
+  ∃ 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/finset.lean

@@ -112,6 +112,17 @@ show (↑s₁ : set α) ⊂ ↑s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁,
 @[simp] theorem val_lt_iff {s₁ s₂ : finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
 and_congr val_le_iff $ not_congr val_le_iff
 
+/-! ### Nonempty -/
+
+protected def nonempty (s : finset α) : Prop := ∃ x:α, x ∈ s
+
+@[elim_cast] lemma coe_nonempty {s : finset α} : (↑s:set α).nonempty ↔ s.nonempty := iff.rfl
+
+lemma nonempty.bex {s : finset α} (h : s.nonempty) : ∃ x:α, x ∈ s := h
+
+lemma nonempty.mono {s t : finset α} (hst : s ⊆ t) (hs : s.nonempty) : t.nonempty :=
+set.nonempty.of_subset hst hs
+
 /- empty -/
 protected def empty : finset α := ⟨0, nodup_zero⟩
 
@@ -138,19 +149,16 @@ lemma eq_empty_iff_forall_not_mem {s : finset α} : s = ∅ ↔ ∀ x, x ∉ s :
 
 theorem subset_empty {s : finset α} : s ⊆ ∅ ↔ s = ∅ := subset_zero.trans val_eq_zero
 
-theorem exists_mem_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a : α, a ∈ s :=
+theorem nonempty_of_ne_empty {s : finset α} (h : s ≠ ∅) : s.nonempty :=
 exists_mem_of_ne_zero (mt val_eq_zero.1 h)
 
-theorem exists_mem_iff_ne_empty {s : finset α} : (∃ a : α, a ∈ s) ↔ ¬s = ∅ :=
-⟨λ ⟨a, ha⟩, ne_empty_of_mem ha, exists_mem_of_ne_empty⟩
+theorem nonempty_iff_ne_empty {s : finset α} : s.nonempty ↔ s ≠ ∅ :=
+⟨λ ⟨a, ha⟩, ne_empty_of_mem ha, nonempty_of_ne_empty⟩
 
-@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl
+theorem eq_empty_or_nonempty (s : finset α) : s = ∅ ∨ s.nonempty :=
+classical.by_cases or.inl (λ h, or.inr (nonempty_of_ne_empty h))
 
-lemma nonempty_iff_ne_empty (s : finset α) : nonempty (↑s : set α) ↔ s ≠ ∅  :=
-begin
-  rw [set.coe_nonempty_iff_ne_empty, ←coe_empty],
-  apply not_congr, apply function.injective.eq_iff, exact to_set_injective
-end
+@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl
 
 /-- `singleton a` is the set `{a}` containing `a` and nothing else. -/
 def singleton (a : α) : finset α := ⟨_, nodup_singleton a⟩
@@ -967,6 +975,9 @@ mem_image.2 ⟨_, h, rfl⟩
 @[simp] lemma coe_image {f : α → β} : ↑(s.image f) = f '' ↑s :=
 set.ext $ λ _, mem_image.trans $ by simp only [exists_prop]; refl
 
+lemma nonempty.image (h : s.nonempty) (f : α → β) : (s.image f).nonempty :=
+let ⟨a, ha⟩ := h in ⟨f a, mem_image_of_mem f ha⟩
+
 theorem image_to_finset [decidable_eq α] {s : multiset α} : s.to_finset.image f = (s.map f).to_finset :=
 ext.2 $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
 
@@ -1023,9 +1034,9 @@ ext.2 $ λ ⟨x, hx⟩, ⟨or.cases_on (mem_insert.1 hx)
 theorem map_eq_image (f : α ↪ β) (s : finset α) : s.map f = s.image f :=
 eq_of_veq $ (multiset.erase_dup_eq_self.2 (s.map f).2).symm
 
-lemma image_const {s : finset α} (h : s ≠ ∅) (b : β) : s.image (λa, b) = singleton b :=
+lemma image_const {s : finset α} (h : s.nonempty) (b : β) : s.image (λa, b) = singleton b :=
 ext.2 $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,
-  exists_mem_of_ne_empty h, true_and, mem_singleton, eq_comm]
+  h.bex, true_and, mem_singleton, eq_comm]
 
 protected def subtype {α} (p : α → Prop) [decidable_pred p] (s : finset α) : finset (subtype p) :=
 (s.filter p).attach.map ⟨λ x, ⟨x.1, (finset.mem_filter.1 x.2).2⟩,
@@ -1065,8 +1076,8 @@ theorem card_def (s : finset α) : s.card = s.1.card := rfl
 @[simp] theorem card_eq_zero {s : finset α} : card s = 0 ↔ s = ∅ :=
 card_eq_zero.trans val_eq_zero
 
-theorem card_pos {s : finset α} : 0 < card s ↔ s ≠ ∅ :=
-pos_iff_ne_zero.trans $ not_congr card_eq_zero
+theorem card_pos {s : finset α} : 0 < card s ↔ s.nonempty :=
+pos_iff_ne_zero.trans $ (not_congr card_eq_zero).trans nonempty_iff_ne_empty.symm
 
 theorem card_ne_zero_of_mem {s : finset α} {a : α} (h : a ∈ s) : card s ≠ 0 :=
 (not_congr card_eq_zero).2 (ne_empty_of_mem h)
@@ -1129,7 +1140,7 @@ lemma card_eq_succ [decidable_eq α] {s : finset α} {n : ℕ} :
 iff.intro
   (assume eq,
     have 0 < card s, from eq.symm ▸ nat.zero_lt_succ _,
-    let ⟨a, has⟩ := finset.exists_mem_of_ne_empty $ card_pos.mp this in
+    let ⟨a, has⟩ := card_pos.mp this in
     ⟨a, s.erase a, s.not_mem_erase a, insert_erase has, by simp only [eq, card_erase_of_mem has, pred_succ]⟩)
   (assume ⟨a, t, hat, s_eq, n_eq⟩, s_eq ▸ n_eq ▸ card_insert_of_not_mem hat)
 
@@ -1762,13 +1773,13 @@ theorem max_eq_sup_with_bot (s : finset α) :
 theorem max_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.max :=
 (@le_sup (with_bot α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
-theorem max_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a, a ∈ s.max :=
-let ⟨a, ha⟩ := exists_mem_of_ne_empty h in max_of_mem ha
+theorem max_of_nonempty {s : finset α} (h : s.nonempty) : ∃ a, a ∈ s.max :=
+let ⟨a, ha⟩ := h in max_of_mem ha
 
 theorem max_eq_none {s : finset α} : s.max = none ↔ s = ∅ :=
-⟨λ h, by_contradiction $
-  λ hs, let ⟨a, ha⟩ := max_of_ne_empty hs in by rw [h] at ha; cases ha,
-λ h, h.symm ▸ max_empty⟩
+⟨λ h, s.eq_empty_or_nonempty.elim id
+  (λ H, let ⟨a, ha⟩ := max_of_nonempty H in by rw h at ha; cases ha),
+  λ h, h.symm ▸ max_empty⟩
 
 theorem mem_of_max {s : finset α} : ∀ {a : α}, a ∈ s.max → a ∈ s :=
 finset.induction_on s (λ _ H, by cases H)
@@ -1803,13 +1814,13 @@ fold_insert_idem
 theorem min_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.min :=
 (@inf_le (with_top α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
-theorem min_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a, a ∈ s.min :=
-let ⟨a, ha⟩ := exists_mem_of_ne_empty h in min_of_mem ha
+theorem min_of_nonempty {s : finset α} (h : s.nonempty) : ∃ a, a ∈ s.min :=
+let ⟨a, ha⟩ := h in min_of_mem ha
 
 theorem min_eq_none {s : finset α} : s.min = none ↔ s = ∅ :=
-⟨λ h, by_contradiction $
-  λ hs, let ⟨a, ha⟩ := min_of_ne_empty hs in by rw [h] at ha; cases ha,
-λ h, h.symm ▸ min_empty⟩
+⟨λ h, s.eq_empty_or_nonempty.elim id
+  (λ H, let ⟨a, ha⟩ := min_of_nonempty H in by rw h at ha; cases ha),
+  λ h, h.symm ▸ min_empty⟩
 
 theorem mem_of_min {s : finset α} : ∀ {a : α}, a ∈ s.min → a ∈ s :=
 finset.induction_on s (λ _ H, by cases H) $
@@ -1827,12 +1838,9 @@ theorem min_le_of_mem {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : a ∈
 by rcases @inf_le (with_top α) _ _ _ _ _ h₁ _ rfl with ⟨b', hb, ab⟩;
    cases h₂.symm.trans hb; assumption
 
-lemma exists_min (s : finset β) (f : β → α)
-  (h : nonempty ↥(↑s : set β)) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x' :=
+lemma exists_min (s : finset β) (f : β → α) (h : s.nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x' :=
 begin
-  have : s.image f ≠ ∅,
-    rwa [ne, image_eq_empty, ← ne.def, ← nonempty_iff_ne_empty],
-  cases min_of_ne_empty this with y hy,
+  cases min_of_nonempty (h.image f) with y hy,
   rcases mem_image.mp (mem_of_min hy) with ⟨x, hx, rfl⟩,
   exact ⟨x, hx, λ x' hx', min_le_of_mem (mem_image_of_mem f hx') hy⟩
 end
@@ -1996,17 +2004,17 @@ section decidable_linear_order
 
 variables {α} [decidable_linear_order α]
 
-def min' (S : finset α) (H : S ≠ ∅) : α :=
+def min' (S : finset α) (H : S.nonempty) : α :=
 @option.get _ S.min $
-  let ⟨k, hk⟩ := exists_mem_of_ne_empty H in
+  let ⟨k, hk⟩ := H in
   let ⟨b, hb⟩ := min_of_mem hk in by simp at hb; simp [hb]
 
-def max' (S : finset α) (H : S ≠ ∅) : α :=
+def max' (S : finset α) (H : S.nonempty) : α :=
 @option.get _ S.max $
-  let ⟨k, hk⟩ := exists_mem_of_ne_empty H in
+  let ⟨k, hk⟩ := H in
   let ⟨b, hb⟩ := max_of_mem hk in by simp at hb; simp [hb]
 
-variables (S : finset α) (H : S ≠ ∅)
+variables (S : finset α) (H : S.nonempty)
 
 theorem min'_mem : S.min' H ∈ S := mem_of_min $ by simp [min']
 

src/data/finsupp.lean

@@ -1367,14 +1367,14 @@ begin
  rw comap_domain_apply
 end
 
-def split_support : finset ι := finset.image (sigma.fst) l.support
+def split_support : finset ι := l.support.image sigma.fst
 
 lemma mem_split_support_iff_nonzero (i : ι) :
   i ∈ split_support l ↔ split l i ≠ 0 :=
 begin
   classical,
-  rw [split_support, mem_image, ne.def, ← support_eq_empty,
-    ← exists_mem_iff_ne_empty, split, comap_domain],
+  rw [split_support, mem_image, ne.def, ← support_eq_empty, ← ne.def,
+    ← finset.nonempty_iff_ne_empty, split, comap_domain, finset.nonempty],
   simp
 end
 

src/data/fintype.lean

@@ -221,6 +221,30 @@ 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.succ → β) :
+  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
+
+@[simp, to_additive] 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.succ → β) :
+  univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
+by apply @fin.prod_univ_succ (multiplicative β)
+
+attribute [to_additive] fin.prod_univ_succ
+
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
 

src/data/nat/totient.lean

@@ -20,8 +20,7 @@ calc totient n ≤ (range n).card : card_le_of_subset (filter_subset _)
 lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
 | 0 := dec_trivial
 | 1 := dec_trivial
-| (n+2) := λ h, card_pos.2 (mt eq_empty_iff_forall_not_mem.1
-(not_forall_of_exists_not ⟨1, not_not.2 $ mem_filter.2 ⟨mem_range.2 dec_trivial, by simp [coprime]⟩⟩))
+| (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩
 
 lemma sum_totient (n : ℕ) : ((range n.succ).filter (∣ n)).sum φ = n :=
 if hn0 : n = 0 then by rw hn0; refl