feat(data/{list,multiset,finset}/*): attach and filter lemmas (leanprover-community#18087)

Left commutativity and cardinality of `list.filter`/`multiset.filter`/`finset.filter`. Interaction of `count`/`countp` and `attach`.

Author: YaelDillies

src/algebra/big_operators/basic.lean

@@ -106,6 +106,9 @@ variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 @[to_additive] lemma prod_eq_multiset_prod [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = (s.1.map f).prod := rfl
 
+@[simp, to_additive] lemma prod_map_val [comm_monoid β] (s : finset α) (f : α → β) :
+  (s.1.map f).prod = ∏ a in s, f a := rfl
+
 @[to_additive]
 theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = s.fold (*) 1 f :=
@@ -1418,16 +1421,19 @@ begin
   apply sum_congr rfl h₁
 end
 
+lemma nat_cast_card_filter [add_comm_monoid_with_one β] (p) [decidable_pred p] (s : finset α) :
+  ((filter p s).card : β) = ∑ a in s, if p a then 1 else 0 :=
+by simp only [add_zero, sum_const, nsmul_eq_mul, eq_self_iff_true, sum_const_zero, sum_ite,
+  nsmul_one]
+
+lemma card_filter (p) [decidable_pred p] (s : finset α) :
+  (filter p s).card = ∑ a in s, ite (p a) 1 0 :=
+nat_cast_card_filter _ _
+
 @[simp]
-lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp : decidable_pred p} :
-  (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
-by simp only [add_zero,
- mul_one,
- finset.sum_const,
- nsmul_eq_mul,
- eq_self_iff_true,
- finset.sum_const_zero,
- finset.sum_ite]
+lemma sum_boole {s : finset α} {p : α → Prop} [add_comm_monoid_with_one β] {hp : decidable_pred p} :
+  (∑ x in s, if p x then 1 else 0 : β) = (s.filter p).card :=
+(nat_cast_card_filter _ _).symm
 
 lemma _root_.commute.sum_right [non_unital_non_assoc_semiring β] (s : finset α)
   (f : α → β) (b : β) (h : ∀ i ∈ s, commute b (f i)) :

src/algebra/big_operators/order.lean

@@ -174,7 +174,7 @@ lemma prod_le_pow_card (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s,
 begin
   refine (multiset.prod_le_pow_card (s.val.map f) n _).trans _,
   { simpa using h },
-  { simpa }
+  { simp }
 end
 
 @[to_additive card_nsmul_le_sum]

src/data/finset/card.lean

@@ -42,6 +42,7 @@ variables {s t : finset α} {a b : α}
 def card (s : finset α) : ℕ := s.1.card
 
 lemma card_def (s : finset α) : s.card = s.1.card := rfl
+@[simp] lemma card_val (s : finset α) : s.1.card = s.card := rfl
 
 @[simp] lemma card_mk {m nodup} : (⟨m, nodup⟩ : finset α).card = m.card := rfl
 

src/data/finset/image.lean

@@ -127,6 +127,22 @@ lemma filter_map {p : β → Prop} [decidable_pred p] :
   (s.map f).filter p = (s.filter (p ∘ f)).map f :=
 eq_of_veq (map_filter _ _ _)
 
+lemma map_filter' (p : α → Prop) [decidable_pred p] (f : α ↪ β) (s : finset α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (s.filter p).map f = (s.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), filter_map, f.injective.eq_iff]
+
+lemma filter_attach' [decidable_eq α] (s : finset α) (p : s → Prop) [decidable_pred p] :
+  s.attach.filter p =
+    (s.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map ⟨subtype.map id $ filter_subset _ _,
+      subtype.map_injective _ injective_id⟩ :=
+eq_of_veq $ multiset.filter_attach' _ _
+
+@[simp] lemma filter_attach (p : α → Prop) [decidable_pred p]  (s : finset α) :
+  (s.attach.filter (λ x, p ↑x)) =
+    (s.filter p).attach.map ((embedding.refl _).subtype_map mem_of_mem_filter) :=
+eq_of_veq $ multiset.filter_attach _ _
+
 lemma map_filter {f : α ≃ β} {p : α → Prop} [decidable_pred p] :
   (s.filter p).map f.to_embedding = (s.map f.to_embedding).filter (p ∘ f.symm) :=
 by simp only [filter_map, function.comp, equiv.to_embedding_apply, equiv.symm_apply_apply]

src/data/list/basic.lean

@@ -2716,6 +2716,8 @@ end split_at_on
   with the same elements but in the type `{x // x ∈ l}`. -/
 def attach (l : list α) : list {x // x ∈ l} := pmap subtype.mk l (λ a, id)
 
+@[simp] lemma attach_nil : ([] : list α).attach = [] := rfl
+
 theorem sizeof_lt_sizeof_of_mem [has_sizeof α] {x : α} {l : list α} (hx : x ∈ l) :
   sizeof x < sizeof l :=
 begin
@@ -3250,12 +3252,35 @@ theorem map_filter (f : β → α) (l : list β) :
   filter p (map f l) = map f (filter (p ∘ f) l) :=
 by rw [← filter_map_eq_map, filter_filter_map, filter_map_filter]; refl
 
+lemma map_filter' {f : α → β} (hf : injective f) (l : list α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (l.filter p).map f = (l.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), map_filter, hf.eq_iff]
+
+lemma filter_attach' (l : list α) (p : {a // a ∈ l} → Prop) [decidable_eq α] [decidable_pred p] :
+  l.attach.filter p = (l.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map
+    (subtype.map id $ λ x hx, let ⟨h, _⟩ := of_mem_filter hx in h) :=
+begin
+  classical,
+  refine map_injective_iff.2 subtype.coe_injective _,
+  simp [(∘), map_filter' _ subtype.coe_injective],
+end
+
+@[simp] lemma filter_attach (l : list α) (p : α → Prop) [decidable_pred p] :
+  l.attach.filter (λ x, p ↑x) = (l.filter p).attach.map (subtype.map id $ λ _, mem_of_mem_filter) :=
+map_injective_iff.2 subtype.coe_injective $ by
+  simp_rw [map_map, (∘), subtype.map, subtype.coe_mk, id.def, ←map_filter, attach_map_coe]
+
 @[simp] theorem filter_filter (q) [decidable_pred q] : ∀ l,
   filter p (filter q l) = filter (λ a, p a ∧ q a) l
 | [] := rfl
 | (a :: l) := by by_cases hp : p a; by_cases hq : q a; simp only [hp, hq, filter, if_true, if_false,
     true_and, false_and, filter_filter l, eq_self_iff_true]
 
+lemma filter_comm (q) [decidable_pred q] (l : list α) :
+  filter p (filter q l) = filter q (filter p l) :=
+by simp [and_comm]
+
 @[simp] lemma filter_true {h : decidable_pred (λ a : α, true)} (l : list α) :
   @filter α (λ _, true) h l = l :=
 by convert filter_eq_self.2 (λ _ _, trivial)

src/data/list/count.lean

@@ -84,6 +84,9 @@ by simp only [countp_eq_length_filter, filter_filter]
 | [] := rfl
 | (a::l) := by rw [map_cons, countp_cons, countp_cons, countp_map]
 
+@[simp] lemma countp_attach (l : list α) : l.attach.countp (λ a, p ↑a) = l.countp p :=
+by rw [←countp_map, attach_map_coe]
+
 variables {p q}
 
 lemma countp_mono_left (h : ∀ x ∈ l, p x → q x) : countp p l ≤ countp q l :=
@@ -197,6 +200,9 @@ lemma count_bind {α β} [decidable_eq β] (l : list α) (f : α → list β) (x
   count x (l.bind f) = sum (map (count x ∘ f) l) :=
 by rw [list.bind, count_join, map_map]
 
+@[simp] lemma count_attach (a : {x // x ∈ l}) : l.attach.count a = l.count a :=
+eq.trans (countp_congr $ λ _ _, subtype.ext_iff) $ countp_attach _ _
+
 @[simp] lemma count_map_of_injective {α β} [decidable_eq α] [decidable_eq β]
   (l : list α) (f : α → β) (hf : function.injective f) (x : α) :
   count (f x) (map f l) = count x l :=

src/data/list/perm.lean

@@ -396,7 +396,7 @@ theorem subperm.countp_le (p : α → Prop) [decidable_pred p]
 | ⟨l, p', s⟩ := p'.countp_eq p ▸ s.countp_le p
 
 theorem perm.countp_congr (s : l₁ ~ l₂) {p p' : α → Prop} [decidable_pred p] [decidable_pred p']
-  (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countp p = l₂.countp p' :=
+  (hp : ∀ x ∈ l₁, p x ↔ p' x) : l₁.countp p = l₂.countp p' :=
 begin
   rw ← s.countp_eq p',
   clear s,

src/data/multiset/basic.lean

@@ -16,7 +16,7 @@ These are implemented as the quotient of a list by permutations.
 We define the global infix notation `::ₘ` for `multiset.cons`.
 -/
 
-open list subtype nat
+open function list nat subtype
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 
@@ -1543,6 +1543,10 @@ le_antisymm (le_inter
   filter p (filter q s) = filter (λ a, p a ∧ q a) s :=
 quot.induction_on s $ λ l, congr_arg coe $ filter_filter p q l
 
+lemma filter_comm (q) [decidable_pred q] (s : multiset α) :
+  filter p (filter q s) = filter q (filter p s) :=
+by simp [and_comm]
+
 theorem filter_add_filter (q) [decidable_pred q] (s : multiset α) :
   filter p s + filter q s = filter (λ a, p a ∨ q a) s + filter (λ a, p a ∧ q a) s :=
 multiset.induction_on s rfl $ λ a s IH,
@@ -1556,6 +1560,11 @@ theorem map_filter (f : β → α) (s : multiset β) :
   filter p (map f s) = map f (filter (p ∘ f) s) :=
 quot.induction_on s (λ l, by simp [map_filter])
 
+lemma map_filter' {f : α → β} (hf : injective f) (s : multiset α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (s.filter p).map f = (s.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), map_filter, hf.eq_iff]
+
 /-! ### Simultaneously filter and map elements of a multiset -/
 
 /-- `filter_map f s` is a combination filter/map operation on `s`.
@@ -1704,6 +1713,18 @@ begin
       card_singleton, add_comm] },
 end
 
+@[simp] lemma countp_attach (s : multiset α) : s.attach.countp (λ a, p ↑a) = s.countp p :=
+quotient.induction_on s $ λ l, begin
+  simp only [quot_mk_to_coe, coe_countp],
+  rw [quot_mk_to_coe, coe_attach, coe_countp],
+  exact list.countp_attach _ _,
+end
+
+@[simp] lemma filter_attach (m : multiset α) (p : α → Prop) [decidable_pred p] :
+  (m.attach.filter (λ x, p ↑x)) =
+    (m.filter p).attach.map (subtype.map id $ λ _, multiset.mem_of_mem_filter) :=
+quotient.induction_on m $ λ l, congr_arg coe (list.filter_attach l p)
+
 variable {p}
 
 theorem countp_pos {s} : 0 < countp p s ↔ ∃ a ∈ s, p a :=
@@ -1720,7 +1741,7 @@ countp_pos.2 ⟨_, h, pa⟩
 
 theorem countp_congr {s s' : multiset α} (hs : s = s')
   {p p' : α → Prop} [decidable_pred p] [decidable_pred p']
-  (hp : ∀ x ∈ s, p x = p' x) : s.countp p = s'.countp p' :=
+  (hp : ∀ x ∈ s, p x ↔ p' x) : s.countp p = s'.countp p' :=
 quot.induction_on₂ s s' (λ l l' hs hp, begin
   simp only [quot_mk_to_coe'', coe_eq_coe] at hs,
   exact hs.countp_congr hp,
@@ -1731,7 +1752,7 @@ end
 /-! ### Multiplicity of an element -/
 
 section
-variable [decidable_eq α]
+variables [decidable_eq α] {s : multiset α}
 
 /-- `count a s` is the multiplicity of `a` in `s`. -/
 def count (a : α) : multiset α → ℕ := countp (eq a)
@@ -1778,6 +1799,9 @@ def count_add_monoid_hom (a : α) : multiset α →+ ℕ := countp_add_monoid_ho
 @[simp] theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s :=
 by induction n; simp [*, succ_nsmul', succ_mul, zero_nsmul]
 
+@[simp] lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count a :=
+eq.trans (countp_congr rfl $ λ _ _, subtype.ext_iff) $ countp_attach _ _
+
 theorem count_pos {a : α} {s : multiset α} : 0 < count a s ↔ a ∈ s :=
 by simp [count, countp_pos]
 
@@ -1901,13 +1925,6 @@ begin
     contradiction }
 end
 
-@[simp]
-lemma attach_count_eq_count_coe (m : multiset α) (a) : m.attach.count a = m.count (a : α) :=
-calc m.attach.count a
-    = (m.attach.map (coe : _ → α)).count (a : α) :
-  (multiset.count_map_eq_count' _ _ subtype.coe_injective _).symm
-... = m.count (a : α) : congr_arg _ m.attach_map_coe
-
 lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = replicate (count b s) b :=
 quotient.induction_on s $ λ l, congr_arg coe $ filter_eq' l b
 
@@ -2174,6 +2191,19 @@ theorem map_injective {f : α → β} (hf : function.injective f) :
   function.injective (multiset.map f) :=
 assume x y, (map_eq_map hf).1
 
+lemma filter_attach' (s : multiset α) (p : {a // a ∈ s} → Prop) [decidable_eq α]
+  [decidable_pred p] :
+  s.attach.filter p =
+    (s.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map (subtype.map id $ λ x hx,
+      let ⟨h, _⟩ := of_mem_filter hx in h) :=
+begin
+  classical,
+  refine multiset.map_injective subtype.coe_injective _,
+  simp only [function.comp, map_filter' _ subtype.coe_injective, subtype.exists, coe_mk,
+    exists_and_distrib_right, exists_eq_right, attach_map_coe, map_map, map_coe, id.def],
+  rw attach_map_coe,
+end
+
 end map
 
 section quot

src/data/multiset/lattice.lean

@@ -39,7 +39,7 @@ sup_bot_eq
 @[simp] lemma sup_add (s₁ s₂ : multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup :=
 eq.trans (by simp [sup]) (fold_add _ _ _ _ _)
 
-lemma sup_le {s : multiset α} {a : α} : s.sup ≤ a ↔ (∀b ∈ s, b ≤ a) :=
+@[simp] lemma sup_le {s : multiset α} {a : α} : s.sup ≤ a ↔ (∀b ∈ s, b ≤ a) :=
 multiset.induction_on s (by simp)
   (by simp [or_imp_distrib, forall_and_distrib] {contextual := tt})
 

src/data/set/finite.lean

@@ -927,8 +927,7 @@ eq.trans (by congr) empty_card
 
 theorem card_fintype_insert_of_not_mem {a : α} (s : set α) [fintype s] (h : a ∉ s) :
   @fintype.card _ (fintype_insert_of_not_mem s h) = fintype.card s + 1 :=
-by rw [fintype_insert_of_not_mem, fintype.card_of_finset];
-   simp [finset.card, to_finset]; refl
+by simp [fintype_insert_of_not_mem, fintype.card_of_finset]
 
 @[simp] theorem card_insert {a : α} (s : set α)
   [fintype s] (h : a ∉ s) {d : fintype.{u} (insert a s : set α)} :