feat(data/[fin]set): add some more basic properties of (finite) sets (#948)

* feat(data/[fin]set): add some more basic properties of (finite) sets

* update after reviews

* fix error, move pairwise_disjoint to lattice as well

* fix error

Author: fpvandoorn

src/data/equiv/basic.lean

@@ -136,7 +136,7 @@ protected lemma subset_image {α β} (e : α ≃ β) (s : set α) (t : set β) :
 by rw [set.image_subset_iff, e.image_eq_preimage]
 
 lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f '' s) = s :=
-by rw [← set.image_comp]; simpa using set.image_id s
+by { rw [← set.image_comp], simp }
 
 protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
   f '' -s = -(f '' s) :=

src/data/finset.lean

@@ -65,6 +65,9 @@ ext.2
 @[simp] theorem coe_inj {s₁ s₂ : finset α} : (↑s₁ : set α) = ↑s₂ ↔ s₁ = s₂ :=
 (set.ext_iff _ _).trans ext.symm
 
+lemma to_set_injective {α} : function.injective (finset.to_set : finset α → set α) :=
+λ s t, coe_inj.1
+
 /- subset -/
 
 instance : has_subset (finset α) := ⟨λ s₁ s₂, ∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂⟩
@@ -140,6 +143,12 @@ exists_mem_of_ne_zero (mt val_eq_zero.1 h)
 
 @[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl
 
+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
+
 /-- `singleton a` is the set `{a}` containing `a` and nothing else. -/
 def singleton (a : α) : finset α := ⟨_, nodup_singleton a⟩
 local prefix `ι`:90 := singleton
@@ -509,6 +518,9 @@ by simpa only [subset_iff, mem_sdiff, and_imp] using λ a m₁ m₂, and.intro (
 @[simp] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (↑s₁ \ ↑s₂ : set α) :=
 set.ext $ λ _, mem_sdiff
 
+@[simp] lemma to_set_sdiff (s t : finset α) : (s \ t).to_set = s.to_set \ t.to_set :=
+by apply finset.coe_sdiff
+
 end decidable_eq
 
 /- attach -/
@@ -580,6 +592,10 @@ theorem filter_union (s₁ s₂ : finset α) :
   (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
 ext.2 $ λ _, by simp only [mem_filter, mem_union, or_and_distrib_right]
 
+theorem filter_union_right (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
+  s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
+ext.2 $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
+
 theorem filter_or (s : finset α) : s.filter (λ a, p a ∨ q a) = s.filter p ∪ s.filter q :=
 ext.2 $ λ _, by simp only [mem_filter, mem_union, and_or_distrib_left]
 
@@ -602,6 +618,15 @@ by simp only [filter_not, inter_sdiff_self]
 @[simp] lemma coe_filter (s : finset α) : ↑(s.filter p) = ({x ∈ ↑s | p x} : set α) :=
 set.ext $ λ _, mem_filter
 
+lemma subset_union_elim {s : finset α} {t₁ t₂ : set α} [decidable_pred (∈ t₁)] (h : ↑s ⊆ t₁ ∪ t₂) :
+  ∃s₁ s₂ : finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁ :=
+begin
+  refine ⟨s.filter (∈ t₁), s.filter (∉ t₁), _, _ , _⟩,
+  { simp [filter_union_right, classical.or_not] },
+  { intro x, simp },
+  { intro x, simp, intros hx hx₂, refine ⟨or.resolve_left (h hx) hx₂, hx₂⟩ }
+end
+
 end filter
 
 /- range -/
@@ -912,6 +937,21 @@ protected def subtype {α} (p : α → Prop) [decidable_pred p] (s : finset α)
   ∀{a : subtype p}, a ∈ s.subtype p ↔ a.val ∈ s
 | ⟨a, ha⟩ := by simp [finset.subtype, ha]
 
+lemma subset_image_iff [decidable_eq α] [decidable_eq β] {f : α → β}
+  {s : finset β} {t : set α} : ↑s ⊆ f '' t ↔ ∃s' : finset α, ↑s' ⊆ t ∧ s'.image f = s :=
+begin
+  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,
+  { exact ⟨∅, set.empty_subset _, 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]
+end
+
 end image
 
 /- card -/

src/data/set/basic.lean

@@ -284,6 +284,12 @@ union_subset_union h (by refl)
 theorem union_subset_union_right (s) {t₁ t₂ : set α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂ :=
 union_subset_union (by refl) h
 
+lemma subset_union_of_subset_left {s t : set α} (h : s ⊆ t) (u : set α) : s ⊆ t ∪ u :=
+subset.trans h (subset_union_left t u)
+
+lemma subset_union_of_subset_right {s u : set α} (h : s ⊆ u) (t : set α) : s ⊆ t ∪ u :=
+subset.trans h (subset_union_right t u)
+
 @[simp] theorem union_empty_iff {s t : set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ :=
 ⟨by finish [ext_iff], by finish [ext_iff]⟩
 
@@ -496,6 +502,9 @@ by simp [eq_empty_iff_forall_not_mem]
 theorem inter_singleton_eq_empty : s ∩ {a} = ∅ ↔ a ∉ s :=
 by rw [inter_comm, singleton_inter_eq_empty]
 
+lemma nmem_singleton_empty {s : set α} : s ∉ ({∅} : set (set α)) ↔ nonempty s :=
+by simp [coe_nonempty_iff_ne_empty]
+
 /- separation -/
 
 theorem mem_sep {s : set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) : x ∈ {x ∈ s | p x} :=
@@ -553,6 +562,17 @@ by finish [ext_iff]
 @[simp] theorem compl_univ : -(univ : set α) = ∅ :=
 by finish [ext_iff]
 
+lemma compl_empty_iff {s : set α} : -s = ∅ ↔ s = univ :=
+by { split, intro h, rw [←compl_compl s, h, compl_empty], intro h, rw [h, compl_univ] }
+
+lemma compl_univ_iff {s : set α} : -s = univ ↔ s = ∅ :=
+by rw [←compl_empty_iff, compl_compl]
+
+lemma nonempty_compl {s : set α} : nonempty (-s : set α) ↔ s ≠ univ :=
+by { symmetry, rw [coe_nonempty_iff_ne_empty], apply not_congr,
+     split, intro h, rw [h, compl_univ],
+     intro h, rw [←compl_compl s, h, compl_empty] }
+
 theorem union_eq_compl_compl_inter_compl (s t : set α) : s ∪ t = -(-s ∩ -t) :=
 by simp [compl_inter, compl_compl]
 
@@ -667,6 +687,15 @@ lemma diff_subset_iff {s t u : set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u :=
 ⟨assume h x xs, classical.by_cases or.inl (assume nxt, or.inr (h ⟨xs, nxt⟩)),
  assume h x ⟨xs, nxt⟩, or.resolve_left (h xs) nxt⟩
 
+lemma subset_insert_diff (s t : set α) : s ⊆ (s \ t) ∪ t :=
+by rw [union_comm, ←diff_subset_iff]
+
+@[simp] lemma diff_singleton_subset_iff {x : α} {s t : set α} : s \ {x} ⊆ t ↔ s ⊆ insert x t :=
+by { rw [←union_singleton, union_comm], apply diff_subset_iff }
+
+lemma subset_insert_diff_singleton (x : α) (s : set α) : s ⊆ insert x (s \ {x}) :=
+by rw [←diff_singleton_subset_iff]
+
 lemma diff_subset_comm {s t u : set α} : s \ t ⊆ u ↔ s \ u ⊆ t :=
 by rw [diff_subset_iff, diff_subset_iff, union_comm]
 
@@ -694,6 +723,13 @@ by simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
 
 @[simp] lemma diff_self {s : set α} : s \ s = ∅ := ext $ by simp
 
+lemma mem_diff_singleton {s s' : set α} {t : set (set α)} : s ∈ t \ {s'} ↔ (s ∈ t ∧ s ≠ s') :=
+by simp
+
+lemma mem_diff_singleton_empty {s : set α} {t : set (set α)} :
+  s ∈ t \ {∅} ↔ (s ∈ t ∧ nonempty s) :=
+by simp [coe_nonempty_iff_ne_empty]
+
 /- powerset -/
 
 theorem mem_powerset {x s : set α} (h : x ⊆ s) : x ∈ powerset s := h
@@ -799,6 +835,10 @@ mem_image_elim h h_y
   (h : ∀a∈s, f a = g a) : f '' s = g '' s :=
 by safe [ext_iff, iff_def]
 
+/- A common special case of `image_congr` -/
+lemma image_congr' {f g : α → β} {s : set α} (h : ∀ (x : α), f x = g x) : f '' s = g '' s :=
+image_congr (λx _, h x)
+
 theorem image_eq_image_of_eq_on {f₁ f₂ : α → β} {s : set α} (heq : eq_on f₁ f₂ s) :
   f₁ '' s = f₂ '' s :=
 image_congr heq
@@ -815,6 +855,11 @@ begin
   finish
 end -/
 
+/-- A variant of `image_comp`, useful for rewriting -/
+lemma image_image (g : β → γ) (f : α → β) (s : set α) : g '' (f '' s) = (λ x, g (f x)) '' s :=
+(image_comp g f s).symm
+
+
 theorem image_subset {a b : set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b :=
 by finish [subset_def, mem_image_eq]
 
@@ -861,6 +906,9 @@ end
 
 @[simp] theorem image_id (s : set α) : id '' s = s := ext $ by simp
 
+/-- A variant of `image_id` -/
+@[simp] lemma image_id' (s : set α) : (λx, x) '' s = s := image_id s
+
 theorem compl_compl_image (S : set (set α)) :
   compl '' (compl '' S) = S :=
 by rw [← image_comp, compl_comp_compl, image_id]
@@ -899,6 +947,9 @@ by rw ← image_union; simp [image_univ_of_surjective H]
 theorem image_compl_eq {f : α → β} {s : set α} (H : bijective f) : f '' -s = -(f '' s) :=
 subset.antisymm (image_compl_subset H.1) (subset_image_compl H.2)
 
+lemma nonempty_image (f : α → β) {s : set α} : nonempty s → nonempty (f '' s)
+| ⟨⟨x, hx⟩⟩ := ⟨⟨f x, mem_image_of_mem f hx⟩⟩
+
 /- image and preimage are a Galois connection -/
 theorem image_subset_iff {s : set α} {t : set β} {f : α → β} :
   f '' s ⊆ t ↔ s ⊆ f ⁻¹' t :=
@@ -1051,6 +1102,23 @@ lemma image_preimage_eq_of_subset {f : α → β} {s : set β} (hs : s ⊆ range
   f '' (f ⁻¹' s) = s :=
 by rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
 
+lemma preimage_subset_preimage_iff {s t : set α} {f : β → α} (hs : s ⊆ range f) :
+  f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t :=
+begin
+  split,
+  { intros h x hx, rcases hs hx with ⟨y, rfl⟩, exact h hx },
+  intros h x, apply h
+end
+
+lemma preimage_eq_preimage' {s t : set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) :
+  f ⁻¹' s = f ⁻¹' t ↔ s = t :=
+begin
+  split,
+  { intro h, apply subset.antisymm, rw [←preimage_subset_preimage_iff hs, h],
+    rw [←preimage_subset_preimage_iff ht, h] },
+  rintro rfl, refl
+end
+
 theorem preimage_inter_range {f : α → β} {s : set β} : f ⁻¹' (s ∩ range f) = f ⁻¹' s :=
 set.ext $ λ x, and_iff_left ⟨x, rfl⟩
 
@@ -1082,6 +1150,9 @@ funext $ λ i, rfl
 lemma surjective_onto_range : surjective (range_factorization f) :=
 λ ⟨_, ⟨i, rfl⟩⟩, ⟨i, rfl⟩
 
+lemma image_eq_range (f : α → β) (s : set α) : f '' s = range (λ(x : s), f x.1) :=
+by { ext, split, rintro ⟨x, h1, h2⟩, exact ⟨⟨x, h1⟩, h2⟩, rintro ⟨⟨x, h1⟩, h2⟩, exact ⟨x, h1, h2⟩ }
+
 end range
 
 /-- The set `s` is pairwise `r` if `r x y` for all *distinct* `x y ∈ s`. -/
@@ -1096,6 +1167,7 @@ theorem pairwise_on.mono' {s : set α} {r r' : α → α → Prop}
 λ x xs y ys h, H _ _ (hp x xs y ys h)
 
 end set
+open set
 
 /- image and preimage on subtypes -/
 
@@ -1112,6 +1184,10 @@ set.ext $ assume a,
 @[simp] lemma val_range {p : α → Prop} :
   set.range (@subtype.val _ p) = {x | p x} :=
 by rw ← set.image_univ; simp [-set.image_univ, val_image]
+
+@[simp] lemma range_val (s : set α) : range (subtype.val : s → α) = s :=
+val_range
+
 theorem val_image_subset (s : set α) (t : set (subtype s)) : t.image val ⊆ s :=
 λ x ⟨y, yt, yvaleq⟩, by rw ←yvaleq; exact y.property
 
@@ -1133,6 +1209,16 @@ begin
   split, { intro h, rw h },
   intro h, exact set.injective_image (val_injective) h
 end
+
+lemma exists_set_subtype {t : set α} (p : set α → Prop) :
+(∃(s : set t), p (subtype.val '' s)) ↔ ∃(s : set α), s ⊆ t ∧ p s :=
+begin
+  split,
+  { rintro ⟨s, hs⟩, refine ⟨subtype.val '' s, _, hs⟩,
+    convert image_subset_range _ _, rw [range_val] },
+  rintro ⟨s, hs₁, hs₂⟩, refine ⟨subtype.val ⁻¹' s, _⟩,
+  rw [image_preimage_eq_of_subset], exact hs₂, rw [range_val], exact hs₁
+end
 end subtype
 
 namespace set

src/data/set/finite.lean

@@ -55,6 +55,12 @@ noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
 @[simp] theorem finite.mem_to_finset {s : set α} {h : finite s} {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
 @mem_to_finset _ _ (finite.fintype h) _
 
+lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
+by { ext, apply mem_to_finset }
+
+lemma exists_finset_of_finite {s : set α} (h : finite s) : ∃(s' : finset α), ↑s' = s :=
+⟨h.to_finset, h.coe_to_finset⟩
+
 theorem finite.exists_finset {s : set α} : finite s →
   ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
 | ⟨h⟩ := by exactI ⟨to_finset s, λ _, mem_to_finset⟩
@@ -260,6 +266,10 @@ theorem finite_bUnion {α} {ι : Type*} {s : set ι} {f : ι → set α} :
   finite s → (∀i, finite (f i)) → finite (⋃ i∈s, f i)
 | ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _)
 
+theorem finite_bUnion' {α} {ι : Type*} {s : set ι} (f : ι → set α) :
+  finite s → (∀i ∈ s, finite (f i)) → finite (⋃ i∈s, f i)
+| ⟨hs⟩ h := by { rw [bUnion_eq_Union], exactI finite_Union (λ i, h i.1 i.2) }
+
 instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
 fintype_of_finset (finset.range n) $ by simp
 

src/data/set/function.lean

@@ -62,19 +62,23 @@ theorem inj_on_of_eq_on {f1 f2 : α → β} {a : set α} (h₁ : eq_on f1 f2 a)
   inj_on f2 a :=
 λ _ _ h₁' h₂' heq, by apply h₂ h₁' h₂'; rw [h₁, heq, ←h₁]; repeat {assumption}
 
-theorem inj_on_comp {g : β → γ} {f : α → β} {a : set α} {b : set β}
-    (h₁ : maps_to f a b) (h₂ : inj_on g b) (h₃: inj_on f a) :
-  inj_on (g ∘ f) a :=
-λ _ _ h₁' h₂' heq,
-by apply h₃ h₁' h₂'; apply h₂; repeat {apply h₁, assumption}; assumption
-
 theorem inj_on_of_inj_on_of_subset {f : α → β} {a b : set α} (h₁ : inj_on f b) (h₂ : a ⊆ b) :
   inj_on f a :=
 λ _ _ h₁' h₂' heq, h₁ (h₂ h₁') (h₂ h₂') heq
 
 lemma injective_iff_inj_on_univ {f : α → β} : injective f ↔ inj_on f univ :=
 iff.intro (λ h _ _ _ _ heq, h heq) (λ h _ _ heq, h trivial trivial heq)
 
+theorem inj_on_comp {g : β → γ} {f : α → β} {a : set α} {b : set β}
+    (h₁ : maps_to f a b) (h₂ : inj_on g b) (h₃: inj_on f a) :
+  inj_on (g ∘ f) a :=
+λ _ _ h₁' h₂' heq,
+by apply h₃ h₁' h₂'; apply h₂; repeat {apply h₁, assumption}; assumption
+
+lemma inj_on_comp_of_injective_left {g : β → γ} {f : α → β} {a : set α} (hg : injective g)
+  (hf : inj_on f a) : inj_on (g ∘ f) a :=
+inj_on_comp (maps_to_univ _ _) (injective_iff_inj_on_univ.mp hg) hf
+
 lemma inj_on_iff_injective {f : α → β} {s : set α} : inj_on f s ↔ injective (λ x:s, f x.1) :=
 ⟨λ H a b h, subtype.eq $ H a.2 b.2 h,
  λ H a b as bs h, congr_arg subtype.val $ @H ⟨a, as⟩ ⟨b, bs⟩ h⟩
@@ -88,6 +92,13 @@ begin
   simp [A] {contextual := tt}
 end
 
+lemma inj_on_preimage {f : α → β} {B : set (set β)} (hB : B ⊆ powerset (range f)) :
+  inj_on (preimage f) B :=
+begin
+  intros s t hs ht hst,
+  rw [←image_preimage_eq_of_subset (hB hs), ←image_preimage_eq_of_subset (hB ht), hst]
+end
+
 lemma subset_image_iff {s : set α} {t : set β} (f : α → β) :
   t ⊆ f '' s ↔ ∃u⊆s, t = f '' u ∧ inj_on f u :=
 begin