feat(data/{set,finset}/basic): Convenience lemmas (#17957)

Add a few convenient corollaries to existing lemmas.

Author: YaelDillies

counterexamples/phillips.lean

@@ -283,7 +283,7 @@ begin
         by simp only [s, function.iterate_succ', union_comm, union_diff_self, subtype.coe_mk,
           union_diff_left],
       rw [nat.succ_eq_add_one, this, f.additive],
-      swap, { rw disjoint.comm, apply disjoint_diff },
+      swap, { exact disjoint_sdiff_self_left },
       calc ((n + 1 : ℕ) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) : by simp only [nat.cast_succ]; ring
       ... ≤ f (↑(s (n + 1 : ℕ)) \ ↑(s n)) + f (↑(s n)) :
         add_le_add (I1 n) IH } },
@@ -339,7 +339,7 @@ begin
   simp only [discrete_part, continuous_part, restrict_apply],
   rw [← f.additive, ← inter_distrib_right],
   { simp only [union_univ, union_diff_self, univ_inter] },
-  { have : disjoint f.discrete_support (univ \ f.discrete_support) := disjoint_diff,
+  { have : disjoint f.discrete_support (univ \ f.discrete_support) := disjoint_sdiff_self_right,
     exact this.mono (inter_subset_left _ _) (inter_subset_left _ _) }
 end
 
@@ -361,7 +361,7 @@ begin
   conv_rhs { rw ← diff_union_inter t s },
   rw [additive, self_eq_add_right],
   { exact continuous_part_apply_eq_zero_of_countable _ _ (hs.mono (inter_subset_right _ _)) },
-  { exact disjoint.mono_right (inter_subset_right _ _) (disjoint.comm.1 disjoint_diff) },
+  { exact disjoint.mono_right (inter_subset_right _ _) disjoint_sdiff_self_left },
 end
 
 end bounded_additive_measure
@@ -515,7 +515,7 @@ begin
   have : φ (f Hcont x) = ψ (spf Hcont x) := rfl,
   have U : univ = spf Hcont x ∪ (univ \ spf Hcont x), by simp only [union_univ, union_diff_self],
   rw [this, eq_add_parts, discrete_part_apply, hx, ψ.empty, zero_add, U,
-    ψ.continuous_part.additive _ _ (disjoint_diff),
+    ψ.continuous_part.additive _ _ disjoint_sdiff_self_right,
     ψ.continuous_part_apply_eq_zero_of_countable _ (countable_compl_spf Hcont x), add_zero],
 end
 

src/algebra/indicator_function.lean

@@ -364,8 +364,8 @@ by rw [sub_eq_add_neg, indicator_compl']
 
 @[to_additive indicator_diff'] lemma mul_indicator_diff (h : s ⊆ t) (f : α → G) :
   mul_indicator (t \ s) f = mul_indicator t f * (mul_indicator s f)⁻¹ :=
-eq_mul_inv_of_mul_eq $ by rw [pi.mul_def, ← mul_indicator_union_of_disjoint disjoint_diff.symm f,
-  diff_union_self, union_eq_self_of_subset_right h]
+eq_mul_inv_of_mul_eq $ by { rw [pi.mul_def, ←mul_indicator_union_of_disjoint, diff_union_self,
+  union_eq_self_of_subset_right h], exact disjoint_sdiff_self_left }
 
 lemma indicator_diff {G : Type*} [add_group G] {s t : set α} (h : s ⊆ t) (f : α → G) :
   indicator (t \ s) f = indicator t f - indicator s f :=

src/analysis/box_integral/partition/basic.lean

@@ -631,7 +631,7 @@ lemma Union_bUnion_partition (h : ∀ J ∈ π, (πi J).is_partition) : (π.bUni
   Union_congr_of_surjective id surjective_id $ λ hJ, (h J hJ).Union_eq
 
 lemma is_partition_disj_union_of_eq_diff (h : π₂.Union = I \ π₁.Union) :
-  is_partition (π₁.disj_union π₂ (h.symm ▸ disjoint_diff)) :=
+  is_partition (π₁.disj_union π₂ $ h.symm ▸ disjoint_sdiff_self_right) :=
 is_partition_iff_Union_eq.2 $ (Union_disj_union _).trans $ by simp [h, π₁.Union_subset]
 
 end prepartition

src/analysis/box_integral/partition/subbox_induction.lean

@@ -205,7 +205,7 @@ def union_compl_to_subordinate (π₁ : tagged_prepartition I) (π₂ : preparti
   (hU : π₂.Union = I \ π₁.Union) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
   tagged_prepartition I :=
 π₁.disj_union (π₂.to_subordinate r)
-  (((π₂.Union_to_subordinate r).trans hU).symm ▸ disjoint_diff)
+  (((π₂.Union_to_subordinate r).trans hU).symm ▸ disjoint_sdiff_self_right)
 
 lemma is_partition_union_compl_to_subordinate (π₁ : tagged_prepartition I) (π₂ : prepartition I)
   (hU : π₂.Union = I \ π₁.Union) (r : (ι → ℝ) → Ioi (0 : ℝ)) :

src/data/finset/basic.lean

@@ -276,8 +276,7 @@ theorem subset_iff {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x 
 theorem subset.antisymm_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ :=
 le_antisymm_iff
 
-theorem not_subset (s t : finset α) : ¬(s ⊆ t) ↔ ∃ x ∈ s, ¬(x ∈ t) :=
-by simp only [←finset.coe_subset, set.not_subset, exists_prop, finset.mem_coe]
+lemma not_subset : ¬ s ⊆ t ↔ ∃ x ∈ s, x ∉ t := by simp only [←coe_subset, set.not_subset, mem_coe]
 
 @[simp] theorem le_eq_subset : ((≤) : finset α → finset α → Prop) = (⊆) := rfl
 @[simp] theorem lt_eq_subset : ((<) : finset α → finset α → Prop) = (⊂) := rfl
@@ -438,7 +437,7 @@ end empty
 /-! ### singleton -/
 
 section singleton
-variables {s : finset α} {a : α}
+variables {s : finset α} {a b : α}
 
 /--
 `{a} : finset a` is the set `{a}` containing `a` and nothing else.
@@ -460,8 +459,7 @@ theorem mem_singleton_self (a : α) : a ∈ ({a} : finset α) := or.inl rfl
 lemma singleton_injective : injective (singleton : α → finset α) :=
 λ a b h, mem_singleton.1 (h ▸ mem_singleton_self _)
 
-theorem singleton_inj {a b : α} : ({a} : finset α) = {b} ↔ a = b :=
-singleton_injective.eq_iff
+@[simp] lemma singleton_inj : ({a} : finset α) = {b} ↔ a = b := singleton_injective.eq_iff
 
 @[simp] theorem singleton_nonempty (a : α) : ({a} : finset α).nonempty := ⟨a, mem_singleton_self a⟩
 
@@ -512,6 +510,8 @@ singleton_subset_set_iff
 @[simp] lemma subset_singleton_iff {s : finset α} {a : α} : s ⊆ {a} ↔ s = ∅ ∨ s = {a} :=
 by rw [←coe_subset, coe_singleton, set.subset_singleton_iff_eq, coe_eq_empty, coe_eq_singleton]
 
+lemma singleton_subset_singleton : ({a} : finset α) ⊆ {b} ↔ a = b := by simp
+
 protected lemma nonempty.subset_singleton_iff {s : finset α} {a : α} (h : s.nonempty) :
   s ⊆ {a} ↔ s = {a} :=
 subset_singleton_iff.trans $ or_iff_right h.ne_empty
@@ -529,6 +529,10 @@ ssubset_singleton_iff.1 hs
 lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ (s : set α).nontrivial :=
 by { rw ←coe_eq_singleton, exact set.eq_singleton_or_nontrivial ha }
 
+lemma nonempty.exists_eq_singleton_or_nontrivial :
+  s.nonempty → (∃ a, s = {a}) ∨ (s : set α).nontrivial :=
+λ ⟨a, ha⟩, (eq_singleton_or_nontrivial ha).imp_left $ exists.intro a
+
 instance [nonempty α] : nontrivial (finset α) :=
 ‹nonempty α›.elim $ λ a, ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩
 
@@ -576,7 +580,7 @@ by rwa [← coe_subset, coe_cons, coe_cons, set.insert_subset_insert_iff, coe_su
 lemma ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ a (h : a ∉ s), s.cons a h ⊆ t :=
 begin
   refine ⟨λ h, _, λ ⟨a, ha, h⟩, ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩,
-  obtain ⟨a, hs, ht⟩ := (not_subset _ _).1 h.2,
+  obtain ⟨a, hs, ht⟩ := not_subset.1 h.2,
   exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩,
 end
 
@@ -592,12 +596,12 @@ lemma disjoint_left : disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
   singleton_subset_iff.mp (h (singleton_subset_iff.mpr hs) (singleton_subset_iff.mpr ht)),
   λ h x hs ht a ha, h (hs ha) (ht ha)⟩
 
-lemma disjoint_val : disjoint s t ↔ s.1.disjoint t.1 := disjoint_left
-
 lemma disjoint_right : disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [disjoint.comm, disjoint_left]
 lemma disjoint_iff_ne : disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b :=
 by simp only [disjoint_left, imp_not_comm, forall_eq']
 
+@[simp] lemma disjoint_val : s.1.disjoint t.1 ↔ disjoint s t := disjoint_left.symm
+
 lemma _root_.disjoint.forall_ne_finset (h : disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b :=
 disjoint_iff_ne.1 h _ ha _ hb
 
@@ -639,7 +643,7 @@ end disjoint
 It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis
 ensures that the sets are disjoint. -/
 def disj_union (s t : finset α) (h : disjoint s t) : finset α :=
-⟨s.1 + t.1, multiset.nodup_add.2 ⟨s.2, t.2, disjoint_val.1 h⟩⟩
+⟨s.1 + t.1, multiset.nodup_add.2 ⟨s.2, t.2, disjoint_val.2 h⟩⟩
 
 @[simp] theorem mem_disj_union {α s t h a} :
   a ∈ @disj_union α s t h ↔ a ∈ s ∨ a ∈ t :=
@@ -1113,6 +1117,8 @@ end
 lemma inter_subset_inter_left (h : t ⊆ u) : s ∩ t ⊆ s ∩ u := inter_subset_inter subset.rfl h
 lemma inter_subset_inter_right (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := inter_subset_inter h subset.rfl
 
+lemma inter_subset_union : s ∩ t ⊆ s ∪ t := le_iff_subset.1 inf_le_sup
+
 instance : distrib_lattice (finset α) :=
 { le_sup_inf := assume a b c, show (a ∪ b) ∩ (a ∪ c) ⊆ a ∪ b ∩ c,
     by simp only [subset_iff, mem_inter, mem_union, and_imp, or_imp_distrib] {contextual:=tt};
@@ -1157,8 +1163,8 @@ lemma union_eq_empty_iff (A B : finset α) : A ∪ B = ∅ ↔ A = ∅ ∧ B = 
 lemma union_subset_iff : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u := (sup_le_iff : s ⊔ t ≤ u ↔ s ≤ u ∧ t ≤ u)
 lemma subset_inter_iff : s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u := (le_inf_iff : s ≤ t ⊓ u ↔ s ≤ t ∧ s ≤ u)
 
-lemma inter_eq_left_iff_subset (s t : finset α) : s ∩ t = s ↔ s ⊆ t := inf_eq_left
-lemma inter_eq_right_iff_subset (s t : finset α) : t ∩ s = s ↔ s ⊆ t := inf_eq_right
+@[simp] lemma inter_eq_left_iff_subset (s t : finset α) : s ∩ t = s ↔ s ⊆ t := inf_eq_left
+@[simp] lemma inter_eq_right_iff_subset (s t : finset α) : t ∩ s = s ↔ s ⊆ t := inf_eq_right
 
 lemma inter_congr_left (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u := inf_congr_left ht hu
 lemma inter_congr_right (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u := inf_congr_right hs ht
@@ -1172,6 +1178,14 @@ lemma ite_subset_union (s s' : finset α) (P : Prop) [decidable P] :
 lemma inter_subset_ite (s s' : finset α) (P : Prop) [decidable P] :
   s ∩ s' ⊆ ite P s s' := inf_le_ite s s' P
 
+lemma not_disjoint_iff_nonempty_inter : ¬disjoint s t ↔ (s ∩ t).nonempty :=
+not_disjoint_iff.trans $ by simp [finset.nonempty]
+
+alias not_disjoint_iff_nonempty_inter ↔ _ nonempty.not_disjoint
+
+lemma disjoint_or_nonempty_inter (s t : finset α) : disjoint s t ∨ (s ∩ t).nonempty :=
+by { rw ←not_disjoint_iff_nonempty_inter, exact em _ }
+
 end lattice
 
 /-! ### erase -/
@@ -1256,7 +1270,7 @@ calc s.erase a ⊂ insert a (s.erase a) : ssubset_insert $ not_mem_erase _ _
 lemma ssubset_iff_exists_subset_erase {s t : finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a :=
 begin
   refine ⟨λ h, _, λ ⟨a, ha, h⟩, ssubset_of_subset_of_ssubset h $ erase_ssubset ha⟩,
-  obtain ⟨a, ht, hs⟩ := (not_subset _ _).1 h.2,
+  obtain ⟨a, ht, hs⟩ := not_subset.1 h.2,
   exact ⟨a, ht, subset_erase.2 ⟨h.1, hs⟩⟩,
 end
 
@@ -1374,7 +1388,9 @@ lemma sdiff_union_inter (s t : finset α) : (s \ t) ∪ (s ∩ t) = s := sup_sdi
 
 @[simp] lemma sdiff_idem (s t : finset α) : s \ t \ t = s \ t := sdiff_idem
 
-lemma sdiff_eq_empty_iff_subset : s \ t = ∅ ↔ s ⊆ t := sdiff_eq_bot_iff
+lemma subset_sdiff : s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u := le_iff_subset.symm.trans le_sdiff
+
+@[simp] lemma sdiff_eq_empty_iff_subset : s \ t = ∅ ↔ s ⊆ t := sdiff_eq_bot_iff
 
 lemma sdiff_nonempty : (s \ t).nonempty ↔ ¬ s ⊆ t :=
 nonempty_iff_ne_empty.trans sdiff_eq_empty_iff_subset.not
@@ -2218,7 +2234,7 @@ hypothesis ensures that the sets are disjoint. -/
 def disj_Union (s : finset α) (t : α → finset β)
   (hf : (s : set α).pairwise_disjoint t) : finset β :=
 ⟨(s.val.bind (finset.val ∘ t)), multiset.nodup_bind.mpr
-  ⟨λ a ha, (t a).nodup, s.nodup.pairwise $ λ a ha b hb hab, finset.disjoint_val.1 $ hf ha hb hab⟩⟩
+  ⟨λ a ha, (t a).nodup, s.nodup.pairwise $ λ a ha b hb hab, disjoint_val.2 $ hf ha hb hab⟩⟩
 
 @[simp] theorem disj_Union_val (s : finset α) (t : α → finset β) (h) :
   (s.disj_Union t h).1 = (s.1.bind (λ a, (t a).1)) := rfl

src/data/finset/card.lean

@@ -184,6 +184,12 @@ card_le_of_subset $ filter_subset _ _
 lemma eq_of_subset_of_card_le {s t : finset α} (h : s ⊆ t) (h₂ : t.card ≤ s.card) : s = t :=
 eq_of_veq $ multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂
 
+lemma eq_of_superset_of_card_ge (hst : s ⊆ t) (hts : t.card ≤ s.card) : t = s :=
+(eq_of_subset_of_card_le hst hts).symm
+
+lemma subset_iff_eq_of_card_le (h : t.card ≤ s.card) : s ⊆ t ↔ s = t :=
+⟨λ hst, eq_of_subset_of_card_le hst h, eq.subset'⟩
+
 lemma map_eq_of_subset {f : α ↪ α} (hs : s.map f ⊆ s) : s.map f = s :=
 eq_of_subset_of_card_le hs (card_map _).ge
 
@@ -301,6 +307,9 @@ variables [decidable_eq α]
 lemma card_union_add_card_inter (s t : finset α) : (s ∪ t).card + (s ∩ t).card = s.card + t.card :=
 finset.induction_on t (by simp) $ λ a r har, by by_cases a ∈ s; simp *; cc
 
+lemma card_inter_add_card_union (s t : finset α) : (s ∩ t).card + (s ∪ t).card = s.card + t.card :=
+by rw [add_comm, card_union_add_card_inter]
+
 lemma card_union_le (s t : finset α) : (s ∪ t).card ≤ s.card + t.card :=
 card_union_add_card_inter s t ▸ nat.le_add_right _ _
 
@@ -323,6 +332,9 @@ calc card t - card s
   ... = card (t \ (s ∩ t)) : (card_sdiff (inter_subset_right s t)).symm
   ... ≤ card (t \ s) : by rw sdiff_inter_self_right t s
 
+lemma card_le_card_sdiff_add_card : s.card ≤ (s \ t).card + t.card :=
+tsub_le_iff_right.1 $ le_card_sdiff _ _
+
 lemma card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card :=
 by rw [←card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
 

src/data/finset/image.lean

@@ -239,6 +239,9 @@ by simp only [mem_def, image_val, mem_dedup, multiset.mem_map, exists_prop]
 
 lemma mem_image_of_mem (f : α → β) {a} (h : a ∈ s) : f a ∈ s.image f := mem_image.2 ⟨_, h, rfl⟩
 
+lemma forall_image {p : β → Prop} : (∀ b ∈ s.image f, p b) ↔ ∀ a ∈ s, p (f a) :=
+by simp only [mem_image, forall_exists_index, forall_apply_eq_imp_iff₂]
+
 @[simp] lemma mem_image_const : c ∈ s.image (const α b) ↔ s.nonempty ∧ b = c :=
 by { rw mem_image, simp only [exists_prop, const_apply, exists_and_distrib_right], refl }
 

src/data/finset/lattice.lean

@@ -26,7 +26,7 @@ variables [semilattice_sup α] [order_bot α]
 /-- Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c` -/
 def sup (s : finset β) (f : β → α) : α := s.fold (⊔) ⊥ f
 
-variables {s s₁ s₂ : finset β} {f g : β → α}
+variables {s s₁ s₂ : finset β} {f g : β → α} {a : α}
 
 lemma sup_def : s.sup f = (s.1.map f).sup := rfl
 
@@ -76,6 +76,8 @@ alias finset.sup_le_iff ↔ _ sup_le
 
 attribute [protected] sup_le
 
+lemma sup_const_le : s.sup (λ _, a) ≤ a := finset.sup_le $ λ _ _, le_rfl
+
 lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f := finset.sup_le_iff.1 le_rfl _ hb
 
 @[simp] lemma sup_bUnion [decidable_eq β] (s : finset γ) (t : γ → finset β) :
@@ -252,7 +254,7 @@ variables [semilattice_inf α] [order_top α]
 /-- Infimum of a finite set: `inf {a, b, c} f = f a ⊓ f b ⊓ f c` -/
 def inf (s : finset β) (f : β → α) : α := s.fold (⊓) ⊤ f
 
-variables {s s₁ s₂ : finset β} {f g : β → α}
+variables {s s₁ s₂ : finset β} {f g : β → α} {a : α}
 
 lemma inf_def : s.inf f = (s.1.map f).inf := rfl
 
@@ -301,6 +303,8 @@ alias finset.le_inf_iff ↔ _ le_inf
 
 attribute [protected] le_inf
 
+lemma le_inf_const_le : a ≤ s.inf (λ _, a) := finset.le_inf $ λ _ _, le_rfl
+
 lemma inf_le {b : β} (hb : b ∈ s) : s.inf f ≤ f b := finset.le_inf_iff.1 le_rfl _ hb
 
 lemma inf_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.inf f ≤ s.inf g :=

src/data/fintype/basic.lean

@@ -52,7 +52,7 @@ class fintype (α : Type*) :=
 (complete : ∀ x : α, x ∈ elems)
 
 namespace finset
-variables [fintype α] {s : finset α}
+variables [fintype α] {s t : finset α}
 
 /-- `univ` is the universal finite set of type `finset α` implied from
   the assumption `fintype α`. -/
@@ -98,6 +98,12 @@ instance : bounded_order (finset α) :=
 
 lemma ssubset_univ_iff {s : finset α} : s ⊂ univ ↔ s ≠ univ := @lt_top_iff_ne_top _ _ _ s
 
+lemma codisjoint_left : codisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t :=
+by { classical, simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left] }
+
+lemma codisjoint_right : codisjoint s t ↔ ∀ ⦃a⦄, a ∉ t → a ∈ s :=
+codisjoint.comm.trans codisjoint_left
+
 section boolean_algebra
 variables [decidable_eq α] {a : α}
 
@@ -316,6 +322,16 @@ def of_surjective [decidable_eq β] [fintype α] (f : α → β) (H : function.s
 
 end fintype
 
+namespace finset
+variables [fintype α] [decidable_eq α] {s t : finset α}
+
+instance decidable_codisjoint : decidable (codisjoint s t) :=
+decidable_of_iff _ codisjoint_left.symm
+
+instance decidable_is_compl : decidable (is_compl s t) := decidable_of_iff' _ is_compl_iff
+
+end finset
+
 section inv
 
 namespace function
@@ -699,6 +715,9 @@ instance plift.fintype_Prop (p : Prop) [decidable p] : fintype (plift p) :=
 instance Prop.fintype : fintype Prop :=
 ⟨⟨{true, false}, by simp [true_ne_false]⟩, classical.cases (by simp) (by simp)⟩
 
+@[simp] lemma fintype.univ_Prop : (finset.univ : finset Prop) = {true, false} :=
+finset.eq_of_veq $ by simp; refl
+
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 fintype.subtype (univ.filter p) (by simp)