feat(data/finset): add finset.erase_none (#9630)

* move `option.to_finset` and `finset.insert_none` to a new file `data.finset.option`; redefine the latter in terms of `finset.cons`;
* define `finset.erase_none`, prove lemmas about it;
* add `finset.prod_cons`, `finset.sum_cons`, `finset.coe_cons`, `finset.cons_subset_cons`, `finset.card_cons`;
* add `finset.subtype_mono` and `finset.bUnion_congr`;
* add `set.insert_subset_insert_iff`;
* add `@[simp]` to `finset.map_subset_map`;
* upgrade `finset.map_embedding` to an `order_embedding`;
* add `@[simps]` to `equiv.option_is_some_equiv` and `function.embedding.some`;
* golf some proofs.

src/algebra/big_operators/basic.lean

@@ -165,6 +165,10 @@ variables [comm_monoid β]
 @[simp, to_additive]
 lemma prod_empty {f : α → β} : (∏ x in (∅:finset α), f x) = 1 := rfl
 
+@[simp, to_additive]
+lemma prod_cons (h : a ∉ s) : (∏ x in (cons a s h), f x) = f a * ∏ x in s, f x :=
+fold_cons h
+
 @[simp, to_additive]
 lemma prod_insert [decidable_eq α] : a ∉ s → (∏ x in (insert a s), f x) = f a * ∏ x in s, f x :=
 fold_insert
@@ -813,13 +817,13 @@ by { rw [range_one], apply @prod_singleton β ℕ 0 f }
 
 open multiset
 
-lemma prod_multiset_map_count [decidable_eq α] (s : multiset α)
+@[to_additive] lemma prod_multiset_map_count [decidable_eq α] (s : multiset α)
   {M : Type*} [comm_monoid M] (f : α → M) :
   (s.map f).prod = ∏ m in s.to_finset, (f m) ^ (s.count m) :=
 begin
-  apply s.induction_on, { simp only [prod_const_one, count_zero, prod_zero, pow_zero, map_zero] },
-  intros a s ih,
-  simp only [prod_cons, map_cons, to_finset_cons, ih],
+  induction s using multiset.induction_on with a s ih,
+  { simp only [prod_const_one, count_zero, prod_zero, pow_zero, map_zero] },
+  simp only [multiset.prod_cons, map_cons, to_finset_cons, ih],
   by_cases has : a ∈ s.to_finset,
   { rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (not_mem_erase _ _),
         prod_insert (not_mem_erase _ _), ← mul_assoc, count_cons_self, pow_succ],
@@ -831,12 +835,6 @@ begin
   rintro rfl, exact has hx
 end
 
-lemma sum_multiset_map_count [decidable_eq α] (s : multiset α)
-  {M : Type*} [add_comm_monoid M] (f : α → M) :
-  (s.map f).sum = ∑ m in s.to_finset, s.count m • f m :=
-@prod_multiset_map_count _ _ _ (multiplicative M) _ f
-attribute [to_additive] prod_multiset_map_count
-
 @[to_additive]
 lemma prod_multiset_count [decidable_eq α] [comm_monoid α] (s : multiset α) :
   s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=

src/algebra/big_operators/option.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+
+import algebra.big_operators.basic
+import data.finset.option
+
+/-!
+# Lemmas about products and sums over finite sets in `option α`
+
+In this file we prove formulas for products and sums over `finset.insert_none s` and
+`finset.erase_none s`.
+-/
+
+open_locale big_operators
+open function
+
+namespace finset
+
+variables {α M : Type*} [comm_monoid M]
+
+@[simp, to_additive] lemma prod_insert_none (f : option α → M) (s : finset α) :
+  ∏ x in s.insert_none, f x = f none * ∏ x in s, f (some x) :=
+by simp [insert_none]
+
+@[to_additive] lemma prod_erase_none (f : α → M) (s : finset (option α)) :
+  ∏ x in s.erase_none, f x = ∏ x in s, option.elim x 1 f :=
+by classical;
+calc ∏ x in s.erase_none, f x = ∏ x in s.erase_none.map embedding.some, option.elim x 1 f :
+  (prod_map s.erase_none embedding.some (λ x, option.elim x 1 f)).symm
+... = ∏ x in s.erase none, option.elim x 1 f : by rw map_some_erase_none
+... = ∏ x in s, option.elim x 1 f : prod_erase _ rfl
+
+end finset

src/algebra/polynomial/big_operators.lean

@@ -123,11 +123,9 @@ where this condition is automatically satisfied.
 lemma leading_coeff_multiset_prod' (h : (t.map leading_coeff).prod ≠ 0) :
   t.prod.leading_coeff = (t.map leading_coeff).prod :=
 begin
-  revert h,
-  refine multiset.induction_on t _ (λ a t ih ht, _), { simp },
-  rw [map_cons, prod_cons] at ht,
-  simp only [map_cons, prod_cons],
-  rw polynomial.leading_coeff_mul'; { rwa ih, apply right_ne_zero_of_mul ht }
+  induction t using multiset.induction_on with a t ih, { simp },
+  simp only [map_cons, multiset.prod_cons] at h ⊢,
+  rw polynomial.leading_coeff_mul'; { rwa ih, apply right_ne_zero_of_mul h }
 end
 
 /--
@@ -153,8 +151,8 @@ lemma nat_degree_multiset_prod' (h : (t.map (λ f, leading_coeff f)).prod ≠ 0)
 begin
   revert h,
   refine multiset.induction_on t _ (λ a t ih ht, _), { simp },
-  rw [map_cons, prod_cons] at ht ⊢,
-  rw [sum_cons, polynomial.nat_degree_mul', ih],
+  rw [map_cons, multiset.prod_cons] at ht ⊢,
+  rw [multiset.sum_cons, polynomial.nat_degree_mul', ih],
   { apply right_ne_zero_of_mul ht },
   { rwa polynomial.leading_coeff_multiset_prod', apply right_ne_zero_of_mul ht },
 end
@@ -210,7 +208,7 @@ lemma coeff_zero_multiset_prod :
   t.prod.coeff 0 = (t.map (λ f, coeff f 0)).prod :=
 begin
   refine multiset.induction_on t _ (λ a t ht, _), { simp },
-  rw [prod_cons, map_cons, prod_cons, polynomial.mul_coeff_zero, ht]
+  rw [multiset.prod_cons, map_cons, multiset.prod_cons, polynomial.mul_coeff_zero, ht]
 end
 
 lemma coeff_zero_prod :
@@ -294,7 +292,7 @@ lemma degree_multiset_prod [nontrivial R] :
   t.prod.degree = (t.map (λ f, degree f)).sum :=
 begin
   refine multiset.induction_on t _ (λ a t ht, _), { simp },
-  { rw [prod_cons, degree_mul, ht, map_cons, sum_cons] }
+  { rw [multiset.prod_cons, degree_mul, ht, map_cons, multiset.sum_cons] }
 end
 
 /--

src/data/equiv/basic.lean

@@ -725,7 +725,7 @@ rfl
 rfl
 
 /-- The set of `x : option α` such that `is_some x` is equivalent to `α`. -/
-def option_is_some_equiv (α : Type*) : {x : option α // x.is_some} ≃ α :=
+@[simps] def option_is_some_equiv (α : Type*) : {x : option α // x.is_some} ≃ α :=
 { to_fun := λ o, option.get o.2,
   inv_fun := λ x, ⟨some x, dec_trivial⟩,
   left_inv := λ o, subtype.eq $ option.some_get _,

src/data/finset/basic.lean

@@ -474,7 +474,7 @@ and the union is guaranteed to be disjoint. -/
 def cons {α} (a : α) (s : finset α) (h : a ∉ s) : finset α :=
 ⟨a ::ₘ s.1, multiset.nodup_cons.2 ⟨h, s.2⟩⟩
 
-@[simp] theorem mem_cons {α a s h b} : b ∈ @cons α a s h ↔ b = a ∨ b ∈ s :=
+@[simp] theorem mem_cons {a s h b} : b ∈ @cons α a s h ↔ b = a ∨ b ∈ s :=
 by rcases s with ⟨⟨s⟩⟩; apply list.mem_cons_iff
 
 @[simp] theorem cons_val {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1 := rfl
@@ -490,6 +490,12 @@ rfl
 | [] hl := by simp
 | (a::l) hl := by simp [← multiset.cons_coe]
 
+@[simp] lemma coe_cons {a s h} : (@cons α a s h : set α) = insert a s := by { ext, simp }
+
+@[simp] lemma cons_subset_cons {a s hs t ht} :
+  @cons α a s hs ⊆ cons a t ht ↔ s ⊆ t :=
+by rwa [← coe_subset, coe_cons, coe_cons, set.insert_subset_insert_iff, coe_subset]
+
 /-! ### disjoint union -/
 
 /-- `disj_union s t h` is the set such that `a ∈ disj_union s t h` iff `a ∈ s` or `a ∈ t`.
@@ -1650,22 +1656,6 @@ def not_mem_range_equiv (k : ℕ) : {n // n ∉ range k} ≃ ℕ :=
 @[simp] lemma coe_not_mem_range_equiv_symm (k : ℕ) :
   ((not_mem_range_equiv k).symm : ℕ → {n // n ∉ range k}) = λ j, ⟨j + k, by simp⟩ := rfl
 
-namespace option
-
-/-- Construct an empty or singleton finset from an `option` -/
-def to_finset : option α → finset α
-| none     := ∅
-| (some a) := {a}
-
-@[simp] theorem to_finset_none : none.to_finset = (∅ : finset α) := rfl
-
-@[simp] theorem to_finset_some {a : α} : (some a).to_finset = {a} := rfl
-
-@[simp] theorem mem_to_finset {a : α} {o : option α} : a ∈ o.to_finset ↔ a ∈ o :=
-by cases o; simp only [to_finset, finset.mem_singleton, option.mem_def, eq_comm]; refl
-
-end option
-
 /-! ### erase_dup on list and multiset -/
 
 namespace multiset
@@ -1849,16 +1839,17 @@ by { subst h, simp }
 theorem map_map {g : β ↪ γ} : (s.map f).map g = s.map (f.trans g) :=
 eq_of_veq $ by simp only [map_val, multiset.map_map]; refl
 
-theorem map_subset_map {s₁ s₂ : finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
+@[simp] theorem map_subset_map {s₁ s₂ : finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
 ⟨λ h x xs, (mem_map' _).1 $ h $ (mem_map' f).2 xs,
  λ h, by simp [subset_def, map_subset_map h]⟩
 
-theorem map_inj {s₁ s₂ : finset α} : s₁.map f = s₂.map f ↔ s₁ = s₂ :=
-by simp only [subset.antisymm_iff, map_subset_map]
+/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a finset to its
+image under `f`. -/
+def map_embedding (f : α ↪ β) : finset α ↪o finset β :=
+order_embedding.of_map_le_iff (map f) (λ _ _, map_subset_map)
 
-/-- Associate to an embedding `f` from `α` to `β` the embedding that maps a finset to its image
-under `f`. -/
-def map_embedding (f : α ↪ β) : finset α ↪ finset β := ⟨map f, λ s₁ s₂, map_inj.1⟩
+@[simp] theorem map_inj {s₁ s₂ : finset α} : s₁.map f = s₂.map f ↔ s₁ = s₂ :=
+(map_embedding f).injective.eq_iff
 
 @[simp] theorem map_embedding_apply : map_embedding f s = map f s := rfl
 
@@ -1868,16 +1859,14 @@ eq_of_veq (map_filter _ _ _)
 
 theorem map_union [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f :=
-ext $ λ _, by simp only [mem_map, mem_union, exists_prop, or_and_distrib_right, exists_or_distrib]
+coe_injective $ by simp only [coe_map, coe_union, set.image_union]
 
 theorem map_inter [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f :=
-ext $ λ b, by simp only [mem_map, mem_inter, exists_prop]; exact
-⟨by rintro ⟨a, ⟨m₁, m₂⟩, rfl⟩; exact ⟨⟨a, m₁, rfl⟩, ⟨a, m₂, rfl⟩⟩,
-by rintro ⟨⟨a, m₁, e⟩, ⟨a', m₂, rfl⟩⟩; cases f.2 e; exact ⟨_, ⟨m₁, m₂⟩, rfl⟩⟩
+coe_injective $ by simp only [coe_map, coe_inter, set.image_inter f.injective]
 
 @[simp] theorem map_singleton (f : α ↪ β) (a : α) : map f {a} = {f a} :=
-ext $ λ _, by simp only [mem_map, mem_singleton, exists_prop, exists_eq_left]; exact eq_comm
+coe_injective $ by simp only [coe_map, coe_singleton, set.image_singleton]
 
 @[simp] theorem map_insert [decidable_eq α] [decidable_eq β]
   (f : α ↪ β) (a : α) (s : finset α) :
@@ -2093,24 +2082,16 @@ lemma subtype_eq_empty {p : α → Prop} [decidable_pred p] {s : finset α} :
   s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s :=
 by simp [ext_iff, subtype.forall, subtype.coe_mk]; refl
 
+@[mono] lemma subtype_mono {p : α → Prop} [decidable_pred p] : monotone (finset.subtype p) :=
+λ s t h x hx, mem_subtype.2 $ h $ mem_subtype.1 hx
+
 /-- `s.subtype p` converts back to `s.filter p` with
 `embedding.subtype`. -/
 @[simp] lemma subtype_map (p : α → Prop) [decidable_pred p] :
   (s.subtype p).map (embedding.subtype _) = s.filter p :=
 begin
   ext x,
-  rw mem_map,
-  change (∃ a : {x // p x}, ∃ H, (a : α) = x) ↔ _,
-  split,
-  { rintros ⟨y, hy, hyval⟩,
-    rw [mem_subtype, hyval] at hy,
-    rw mem_filter,
-    use hy,
-    rw ← hyval,
-    use y.property },
-  { intro hx,
-    rw mem_filter at hx,
-    use ⟨⟨x, hx.2⟩, mem_subtype.2 hx.1, rfl⟩ }
+  simp [and_comm _ (_ = _), @and.left_comm _ (_ = _), and_comm (p x) (x ∈ s)]
 end
 
 /-- If all elements of a `finset` satisfy the predicate `p`,
@@ -2150,19 +2131,13 @@ end
 lemma subset_image_iff {f : α → β}
   {s : finset β} {t : set α} : ↑s ⊆ f '' t ↔ ∃s' : finset α, ↑s' ⊆ t ∧ s'.image f = s :=
 begin
-  classical,
   split, swap,
   { rintro ⟨s, hs, rfl⟩, rw [coe_image], exact set.image_subset f hs },
-  intro h, induction s using finset.induction with a s has ih h,
-  { refine ⟨∅, set.empty_subset _, _⟩,
-    convert finset.image_empty _ },
-  rw [finset.coe_insert, set.insert_subset] at h,
-  rcases ih h.2 with ⟨s', hst, hsi⟩,
-  rcases h.1 with ⟨x, hxt, rfl⟩,
-  refine ⟨insert x s', _, _⟩,
-  { rw [finset.coe_insert, set.insert_subset], exact ⟨hxt, hst⟩ },
-  rw [finset.image_insert, hsi],
-  congr
+  intro h,
+  letI : can_lift β t := ⟨f ∘ coe, λ y, y ∈ f '' t, λ y ⟨x, hxt, hy⟩, ⟨⟨x, hxt⟩, hy⟩⟩,
+  lift s to finset t using h,
+  refine ⟨s.map (embedding.subtype _), map_subtype_subset _, _⟩,
+  ext y, simp
 end
 
 end image
@@ -2249,10 +2224,12 @@ lemma one_lt_card_iff {s : finset α} :
   1 < s.card ↔ ∃ x y, (x ∈ s) ∧ (y ∈ s) ∧ x ≠ y :=
 by { rw one_lt_card, simp only [exists_prop, exists_and_distrib_left] }
 
+@[simp] theorem card_cons {a : α} {s : finset α} (h : a ∉ s) : card (cons a s h) = card s + 1 :=
+card_cons _ _
+
 @[simp] theorem card_insert_of_not_mem [decidable_eq α]
   {a : α} {s : finset α} (h : a ∉ s) : card (insert a s) = card s + 1 :=
-by simpa only [card_cons, card, insert_val] using
-congr_arg multiset.card (ndinsert_of_not_mem h)
+by rw [← cons_eq_insert _ _ h, card_cons]
 
 theorem card_insert_of_mem [decidable_eq α] {a : α} {s : finset α}
   (h : a ∈ s) : card (insert a s) = card s := by rw insert_eq_of_mem h
@@ -2610,6 +2587,11 @@ ext $ λ x, by simp only [mem_bUnion, exists_prop, mem_union, mem_insert,
   or_and_distrib_right, exists_or_distrib, exists_eq_left]
 -- ext $ λ x, by simp [or_and_distrib_right, exists_or_distrib]
 
+theorem bUnion_congr {s₁ s₂ : finset α} {t₁ t₂ : α → finset β}
+  (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) :
+  s₁.bUnion t₁ = s₂.bUnion t₂ :=
+ext $ λ x, by simp [hs, ht] { contextual := tt }
+
 @[simp] lemma singleton_bUnion {a : α} : finset.bUnion {a} t = t a :=
 begin
   classical,

src/data/finset/lattice.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.finset.fold
+import data.finset.option
 import data.multiset.lattice
 import order.order_dual
 import order.complete_lattice