[Merged by Bors] - feat(data/{finset,set}/basic): More insert and erase lemmas

src/algebra/big_operators/finprod.lean

@@ -785,7 +785,7 @@ begin
   rw [← bUnion_univ, ← finset.coe_univ, ← finset.coe_bUnion,
     finprod_mem_coe_finset, finset.prod_bUnion],
   { simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype] },
-  { exact λ x _ y _ hxy, finset.disjoint_iff_disjoint_coe.2 (h x y hxy) }
+  { exact λ x _ y _ hxy, finset.disjoint_coe.1 (h x y hxy) }
 end
 
 /-- Given a family of sets `t : ι → set α`, a finite set `I` in the index type such that all sets

src/data/finset/basic.lean

@@ -579,7 +579,7 @@ instance : is_lawful_singleton α (finset α) := ⟨λ a, by { ext, simp }⟩
 
 @[simp] lemma insert_eq_of_mem (h : a ∈ s) : insert a s = s := eq_of_veq $ ndinsert_of_mem h
 
-@[simp] theorem pair_self_eq (a : α) : ({a, a} : finset α) = {a} :=
+@[simp] theorem pair_eq_singleton (a : α) : ({a, a} : finset α) = {a} :=
 insert_eq_of_mem $ mem_singleton_self _
 
 theorem insert.comm (a b : α) (s : finset α) : insert a (insert b s) = insert b (insert a s) :=
@@ -1058,6 +1058,9 @@ begin
   exact ⟨a, ht, subset_erase.2 ⟨h.1, hs⟩⟩,
 end
 
+lemma erase_ssubset_insert (s : finset α) (a : α) : s.erase a ⊂ insert a s :=
+ssubset_iff_exists_subset_erase.2 ⟨a, mem_insert_self _ _, erase_subset_erase _ $ subset_insert _ _⟩
+
 @[simp]
 theorem erase_eq_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : erase s a = s :=
 eq_of_veq $ erase_of_not_mem h
@@ -1066,6 +1069,9 @@ eq_of_veq $ erase_of_not_mem h
   (insert a s).erase a = s.erase a :=
 by by_cases ha : a ∈ s; { simp [ha, erase_insert] }
 
+lemma erase_cons {s : finset α} {a : α} (h : a ∉ s) : (s.cons a h).erase a = s :=
+by rw [cons_eq_insert, erase_insert_eq_erase, erase_eq_of_not_mem h]
+
 lemma erase_idem {a : α} {s : finset α} : erase (erase s a) a = erase s a :=
 by simp
 
@@ -1082,6 +1088,12 @@ subset_insert_iff.1 $ subset.rfl
 theorem insert_erase_subset (a : α) (s : finset α) : s ⊆ insert a (erase s a) :=
 subset_insert_iff.2 $ subset.rfl
 
+lemma subset_insert_iff_of_not_mem (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t :=
+by rw [subset_insert_iff, erase_eq_of_not_mem h]
+
+lemma erase_subset_iff_of_mem (h : a ∈ t) : s.erase a ⊆ t ↔ s ⊆ t :=
+by rw [←subset_insert_iff, insert_eq_of_mem h]
+
 lemma erase_inj {x y : α} (s : finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y :=
 begin
   refine ⟨λ h, _, congr_arg _⟩,
@@ -1092,6 +1104,9 @@ end
 
 lemma erase_inj_on (s : finset α) : set.inj_on s.erase s := λ _ _ _ _, (erase_inj s ‹_›).mp
 
+lemma erase_inj_on' (a : α) : {s : finset α | a ∈ s}.inj_on (λ s, erase s a) :=
+λ s hs t ht (h : s.erase a =  _), by rw [←insert_erase hs, ←insert_erase ht, h]
+
 /-! ### sdiff -/
 
 /-- `s \ t` is the set consisting of the elements of `s` that are not in `t`. -/
@@ -1495,6 +1510,9 @@ lemma filter_mem_eq_inter {s t : finset α} [Π i, decidable (i ∈ t)] :
   s.filter (λ i, i ∈ t) = s ∩ t :=
 ext $ λ i, by rw [mem_filter, mem_inter]
 
+lemma filter_inter_distrib (s t : finset α) : (s ∩ t).filter p = s.filter p ∩ t.filter p :=
+by { ext, simp only [mem_filter, mem_inter], exact and_and_distrib_right _ _ _ }
+
 theorem filter_inter (s t : finset α) : filter p s ∩ t = filter p (s ∩ t) :=
 by { ext, simp only [mem_inter, mem_filter, and.right_comm] }
 
@@ -2057,11 +2075,18 @@ lemma image_inter_subset [decidable_eq α] (f : α → β) (s t : finset α) :
 subset_inter (image_subset_image $ inter_subset_left _ _) $
   image_subset_image $ inter_subset_right _ _
 
-lemma image_inter [decidable_eq α] (s₁ s₂ : finset α) (hf : ∀ x y, f x = f y → x = y) :
+lemma image_inter_of_inj_on [decidable_eq α] {f : α → β} (s t : finset α)
+  (hf : set.inj_on f (s ∪ t)) :
+  (s ∩ t).image f = s.image f ∩ t.image f :=
+(image_inter_subset _ _ _).antisymm $ λ x, begin
+  simp only [mem_inter, mem_image],
+  rintro ⟨⟨a, ha, rfl⟩, b, hb, h⟩,
+  exact ⟨a, ⟨ha, by rwa ←hf (or.inr hb) (or.inl ha) h⟩, rfl⟩,
+end
+
+lemma image_inter [decidable_eq α] (s₁ s₂ : finset α) (hf : injective f) :
   (s₁ ∩ s₂).image f = s₁.image f ∩ s₂.image f :=
-ext $ by simp only [mem_image, exists_prop, mem_inter]; exact λ b,
-⟨λ ⟨a, ⟨m₁, m₂⟩, e⟩, ⟨⟨a, m₁, e⟩, ⟨a, m₂, e⟩⟩,
- λ ⟨⟨a, m₁, e₁⟩, ⟨a', m₂, e₂⟩⟩, ⟨a, ⟨m₁, hf _ _ (e₂.trans e₁.symm) ▸ m₂⟩, e₁⟩⟩.
+image_inter_of_inj_on _ _ $ hf.inj_on _
 
 @[simp] theorem image_singleton (f : α → β) (a : α) : image f {a} = {f a} :=
 ext $ λ x, by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm
@@ -2070,16 +2095,21 @@ ext $ λ x, by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left
   (insert a s).image f = insert (f a) (s.image f) :=
 by simp only [insert_eq, image_singleton, image_union]
 
+lemma erase_image_subset_image_erase [decidable_eq α] (f : α → β) (s : finset α) (a : α) :
+  (s.image f).erase (f a) ⊆ (s.erase a).image f :=
+begin
+  simp only [subset_iff, and_imp, exists_prop, mem_image, exists_imp_distrib, mem_erase],
+  rintro b hb x hx rfl,
+  exact ⟨_, ⟨ne_of_apply_ne f hb, hx⟩, rfl⟩,
+end
+
 @[simp] lemma image_erase [decidable_eq α] {f : α → β} (hf : injective f) (s : finset α) (a : α) :
   (s.erase a).image f = (s.image f).erase (f a) :=
 begin
-  ext b,
+  refine (erase_image_subset_image_erase _ _ _).antisymm' (λ b, _),
   simp only [mem_image, exists_prop, mem_erase],
-  split,
-  { rintro ⟨a', ⟨haa', ha'⟩, rfl⟩,
-    exact ⟨hf.ne haa', a', ha', rfl⟩ },
-  { rintro ⟨h, a', ha', rfl⟩,
-    exact ⟨a', ⟨ne_of_apply_ne _ h, ha'⟩, rfl⟩ }
+  rintro ⟨a', ⟨haa', ha'⟩, rfl⟩,
+  exact ⟨hf.ne haa', a', ha', rfl⟩,
 end
 
 @[simp] theorem image_eq_empty : s.image f = ∅ ↔ s = ∅ :=
@@ -2490,9 +2520,13 @@ lemma disjoint_filter_filter_neg (s : finset α) (p : α → Prop) [decidable_pr
   disjoint (s.filter p) (s.filter $ λ a, ¬ p a) :=
 (disjoint_filter.2 $ λ a _, id).symm
 
-lemma disjoint_iff_disjoint_coe : disjoint s t ↔ disjoint (s : set α) (t : set α) :=
+@[simp, norm_cast] lemma disjoint_coe : disjoint (s : set α) t ↔ disjoint s t :=
 by { rw [finset.disjoint_left, set.disjoint_left], refl }
 
+@[simp, norm_cast] lemma pairwise_disjoint_coe {ι : Type*} {s : set ι} {f : ι → finset α} :
+  s.pairwise_disjoint (λ i, f i : ι → set α) ↔ s.pairwise_disjoint f :=
+forall₅_congr $ λ _ _ _ _ _, disjoint_coe
+
 @[simp] lemma _root_.disjoint.of_image_finset (h : disjoint (s.image f) (t.image f)) :
   disjoint s t :=
 disjoint_iff_ne.2 $ λ a ha b hb, ne_of_apply_ne f $ h.forall_ne_finset

src/data/finset/pointwise.lean

@@ -503,7 +503,7 @@ variables [group α] [division_monoid β] [monoid_hom_class F α β] (m : F) {s
 /-! Note that `finset` is not a `group` because `s / s ≠ 1` in general. -/
 
 @[simp, to_additive] lemma one_mem_div_iff : (1 : α) ∈ s / t ↔ ¬ disjoint s t :=
-by rw [←mem_coe, disjoint_iff_disjoint_coe, coe_div, set.one_mem_div_iff]
+by rw [←mem_coe, ←disjoint_coe, coe_div, set.one_mem_div_iff]
 
 @[to_additive] lemma not_one_mem_div_iff : (1 : α) ∉ s / t ↔ disjoint s t :=
 one_mem_div_iff.not_left

src/data/fintype/basic.lean

@@ -68,6 +68,7 @@ along with some machinery
   See `infinite.of_injective` and `infinite.of_surjective`.
 -/
 
+open function
 open_locale nat
 
 universes u v
@@ -83,7 +84,7 @@ class fintype (α : Type*) :=
 (complete : ∀ x : α, x ∈ elems)
 
 namespace finset
-variable [fintype α]
+variables [fintype α] {s : finset α}
 
 /-- `univ` is the universal finite set of type `finset α` implied from
   the assumption `fintype α`. -/
@@ -94,11 +95,15 @@ fintype.complete x
 
 @[simp] theorem mem_univ_val : ∀ x, x ∈ (univ : finset α).1 := mem_univ
 
-lemma eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s := by simp [ext_iff]
+lemma eq_univ_iff_forall : s = univ ↔ ∀ x, x ∈ s := by simp [ext_iff]
+lemma eq_univ_of_forall  : (∀ x, x ∈ s) → s = univ := eq_univ_iff_forall.2
 
 @[simp] lemma coe_univ : ↑(univ : finset α) = (set.univ : set α) :=
 by ext; simp
 
+@[simp, norm_cast] lemma coe_eq_univ : (s : set α) = set.univ ↔ s = univ :=
+by rw [←coe_univ, coe_inj]
+
 lemma univ_nonempty_iff : (univ : finset α).nonempty ↔ nonempty α :=
 by rw [← coe_nonempty, coe_univ, set.nonempty_iff_univ_nonempty]
 
@@ -120,7 +125,7 @@ instance : order_top (finset α) :=
   le_top := subset_univ }
 
 section boolean_algebra
-variables [decidable_eq α] {s : finset α} {a : α}
+variables [decidable_eq α] {a : α}
 
 instance : boolean_algebra (finset α) :=
 { compl := λ s, univ \ s,
@@ -172,6 +177,9 @@ by rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
 lemma insert_inj_on' (s : finset α) : set.inj_on (λ a, insert a s) (sᶜ : finset α) :=
 by { rw coe_compl, exact s.insert_inj_on }
 
+lemma image_univ_of_surjective [fintype β] {f : β → α} (hf : surjective f) : univ.image f = univ :=
+eq_univ_of_forall $ hf.forall.2 $ λ _, mem_image_of_mem _ $ mem_univ _
+
 end boolean_algebra
 
 @[simp] lemma univ_inter [decidable_eq α] (s : finset α) :
@@ -672,7 +680,7 @@ by simp only [finset.ssubset_def, to_finset_mono, ssubset_def]
 
 @[simp] theorem to_finset_disjoint_iff [decidable_eq α] {s t : set α} [fintype s] [fintype t] :
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
-by simp only [disjoint_iff_disjoint_coe, coe_to_finset]
+by simp only [←disjoint_coe, coe_to_finset]
 
 lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
   [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=

src/data/set/basic.lean

@@ -690,6 +690,9 @@ ssubset_iff_insert.2 ⟨a, h, subset.rfl⟩
 theorem insert_comm (a b : α) (s : set α) : insert a (insert b s) = insert b (insert a s) :=
 ext $ λ x, or.left_comm
 
+@[simp] lemma insert_idem (a : α) (s : set α) : insert a (insert a s) = insert a s :=
+insert_eq_of_mem $ mem_insert _ _
+
 theorem insert_union : insert a s ∪ t = insert a (s ∪ t) := ext $ λ x, or.assoc
 
 @[simp] theorem union_insert : s ∪ insert a t = insert a (s ∪ t) := ext $ λ x, or.left_comm

src/data/set/finite.lean

@@ -513,10 +513,19 @@ lemma univ_finite_iff_nonempty_fintype :
   (univ : set α).finite ↔ nonempty (fintype α) :=
 ⟨λ h, ⟨fintype_of_finite_univ h⟩, λ ⟨_i⟩, by exactI finite_univ⟩
 
-lemma finite.to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
-  (hs.insert a).to_finset = insert a hs.to_finset :=
+@[simp] lemma finite.to_finset_singleton {a : α} (ha : ({a} : set α).finite := finite_singleton _) :
+  ha.to_finset = {a} :=
+finset.ext $ by simp
+
+@[simp] lemma finite.to_finset_insert [decidable_eq α] {s : set α} {a : α}
+  (hs : (insert a s).finite) :
+  hs.to_finset = insert a (hs.subset $ subset_insert _ _).to_finset :=
 finset.ext $ by simp
 
+lemma finite.to_finset_insert' [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
+  (hs.insert a).to_finset = insert a hs.to_finset :=
+finite.to_finset_insert _
+
 lemma finite.fin_embedding {s : set α} (h : s.finite) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s :=
 ⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩
 

src/data/set/lattice.lean

@@ -549,13 +549,16 @@ theorem Inter_and {p q : Prop} (s : p ∧ q → set α) :
   (⋂ h, s h) = ⋂ hp hq, s ⟨hp, hq⟩ :=
 infi_and
 
-theorem Union_comm (s : ι → ι' → set α) :
-  (⋃ i i', s i i') = ⋃ i' i, s i i' :=
-supr_comm
+lemma Union_comm (s : ι → ι' → set α) : (⋃ i i', s i i') = ⋃ i' i, s i i' := supr_comm
+lemma Inter_comm (s : ι → ι' → set α) : (⋂ i i', s i i') = ⋂ i' i, s i i' := infi_comm
 
-theorem Inter_comm (s : ι → ι' → set α) :
-  (⋂ i i', s i i') = ⋂ i' i, s i i' :=
-infi_comm
+lemma Union₂_comm (s : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → set α) :
+  (⋃ i₁ j₁ i₂ j₂, s i₁ j₁ i₂ j₂) = ⋃ i₂ j₂ i₁ j₁, s i₁ j₁ i₂ j₂ :=
+supr₂_comm _
+
+lemma Inter₂_comm (s : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → set α) :
+  (⋂ i₁ j₁ i₂ j₂, s i₁ j₁ i₂ j₂) = ⋂ i₂ j₂ i₁ j₁, s i₁ j₁ i₂ j₂ :=
+infi₂_comm _
 
 @[simp] theorem bUnion_and (p : ι → Prop) (q : ι → ι' → Prop) (s : Π x y, p x ∧ q x y → set α) :
   (⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h) =

src/group_theory/perm/cycle/basic.lean

@@ -1388,8 +1388,8 @@ begin
   have hd1' := coe_inj.2 hd1.support_mul,
   have hd2' := coe_inj.2 hd2.support_mul,
   rw [coe_union] at *,
-  have hd1'' := disjoint_iff_disjoint_coe.1 (disjoint_iff_disjoint_support.1 hd1),
-  have hd2'' := disjoint_iff_disjoint_coe.1 (disjoint_iff_disjoint_support.1 hd2),
+  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1),
+  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2),
   refine is_conj_of_support_equiv _ _,
   { refine ((equiv.set.of_eq hd1').trans (equiv.set.union hd1'')).trans
       ((equiv.sum_congr (subtype_equiv f (λ a, _)) (subtype_equiv g (λ a, _))).trans

src/group_theory/perm/support.lean

@@ -381,7 +381,7 @@ lemma support_swap_iff (x y : α) :
 begin
   refine ⟨λ h H, _, support_swap⟩,
   subst H,
-  simp only [swap_self, support_refl, pair_self_eq] at h,
+  simp only [swap_self, support_refl, pair_eq_singleton] at h,
   have : x ∈ ∅,
   { rw h,
     exact mem_singleton.mpr rfl },

src/logic/basic.lean

@@ -1210,6 +1210,11 @@ by simp [@eq_comm _ a']
 theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ ∃ b a, p a b :=
 ⟨λ ⟨a, b, h⟩, ⟨b, a, h⟩, λ ⟨b, a, h⟩, ⟨a, b, h⟩⟩
 
+lemma exists₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
+  {p : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → Prop} :
+  (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ :=
+by simp only [@exists_comm (κ₁ _), @exists_comm ι₁]
+
 theorem and.exists {p q : Prop} {f : p ∧ q → Prop} : (∃ h, f h) ↔ ∃ hp hq, f ⟨hp, hq⟩ :=
 ⟨λ ⟨h, H⟩, ⟨h.1, h.2, H⟩, λ ⟨hp, hq, H⟩, ⟨⟨hp, hq⟩, H⟩⟩
 

src/order/complete_lattice.lean

@@ -743,6 +743,16 @@ le_antisymm
 -- TODO: should this be @[simp]?
 lemma infi_comm {f : ι → ι' → α} : (⨅ i j, f i j) = ⨅ j i, f i j := @supr_comm αᵒᵈ _ _ _ _
 
+lemma supr₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
+  (f : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → α) :
+  (⨆ i₁ j₁ i₂ j₂, f i₁ j₁ i₂ j₂) = ⨆ i₂ j₂ i₁ j₁, f i₁ j₁ i₂ j₂ :=
+by simp only [@supr_comm _ (κ₁ _), @supr_comm _ ι₁]
+
+lemma infi₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
+  (f : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → α) :
+  (⨅ i₁ j₁ i₂ j₂, f i₁ j₁ i₂ j₂) = ⨅ i₂ j₂ i₁ j₁, f i₁ j₁ i₂ j₂ :=
+by simp only [@infi_comm _ (κ₁ _), @infi_comm _ ι₁]
+
 /- TODO: this is strange. In the proof below, we get exactly the desired
    among the equalities, but close does not get it.
 begin