[Merged by Bors] - feat: Miscellaneous Finset lemmas

Mathlib/Combinatorics/SetFamily/Compression/Down.lean

@@ -209,7 +209,7 @@ theorem card_compression (a : α) (𝒜 : Finset (Finset α)) : (𝓓 a 𝒜).ca
   · conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
   · exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
   intro s hs
-  rw [mem_coe, mem_filter, Function.comp_apply] at hs
+  rw [mem_coe, mem_filter] at hs
   exact not_imp_comm.1 erase_eq_of_not_mem (ne_of_mem_of_not_mem hs.1 hs.2).symm
 #align down.card_compression Down.card_compression
 

Mathlib/Combinatorics/SetFamily/Compression/UV.lean

@@ -194,7 +194,6 @@ theorem compression_idem (u v : α) (s : Finset α) :
   have h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅ :=
     filter_false_of_mem fun a ha h => h <| compress_mem_compression_of_mem_compression ha
   rw [compression, image_filter]
-  simp_rw [Function.comp]
   rw [h, image_empty, ← h]
   exact filter_union_filter_neg_eq _ (compression u v s)
 #align uv.compression_idem UV.compression_idem
@@ -203,12 +202,11 @@ theorem compression_idem (u v : α) (s : Finset α) :
 theorem card_compression (u v : α) (s : Finset α) : (𝓒 u v s).card = s.card := by
   rw [compression, card_disjoint_union (compress_disjoint _ _), image_filter, card_image_of_injOn,
     ← card_disjoint_union]
-  simp_rw [Function.comp]
   rw [filter_union_filter_neg_eq]
   · rw [disjoint_iff_inter_eq_empty]
     exact filter_inter_filter_neg_eq _ _ _
   intro a ha b hb hab
-  rw [mem_coe, mem_filter, Function.comp_apply] at ha hb
+  rw [mem_coe, mem_filter] at ha hb
   rw [compress] at ha hab
   split_ifs at ha hab with has
   · rw [compress] at hb hab

Mathlib/Data/Finset/Basic.lean

@@ -1972,6 +1972,13 @@ theorem insert_erase {a : α} {s : Finset α} (h : a ∈ s) : insert a (erase s
     exact h
 #align finset.insert_erase Finset.insert_erase
 
+lemma erase_eq_iff_eq_insert (hs : a ∈ s) (ht : a ∉ t) : erase s a = t ↔ s = insert a t := by
+  have := insert_erase hs; aesop
+
+lemma insert_erase_invOn :
+    Set.InvOn (insert a) (λ s ↦ erase s a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s} :=
+  ⟨λ _s ↦ insert_erase, λ _s ↦ erase_insert⟩
+
 theorem erase_subset_erase (a : α) {s t : Finset α} (h : s ⊆ t) : erase s a ⊆ erase t a :=
   val_le_iff.1 <| erase_le_erase _ <| val_le_iff.2 h
 #align finset.erase_subset_erase Finset.erase_subset_erase
@@ -2221,6 +2228,9 @@ theorem insert_sdiff_of_mem (s : Finset α) {x : α} (h : x ∈ t) : insert x s
   exact Set.insert_diff_of_mem _ h
 #align finset.insert_sdiff_of_mem Finset.insert_sdiff_of_mem
 
+lemma insert_sdiff_cancel (ha : a ∉ s) : insert a s \ s = {a} := by
+  rw [insert_sdiff_of_not_mem _ ha, Finset.sdiff_self, insert_emptyc_eq]
+
 @[simp]
 theorem insert_sdiff_insert (s t : Finset α) (x : α) : insert x s \ insert x t = s \ insert x t :=
   insert_sdiff_of_mem _ (mem_insert_self _ _)
@@ -2420,6 +2430,10 @@ theorem coe_symmDiff : (↑(s ∆ t) : Set α) = (s : Set α) ∆ t :=
   Set.ext fun x => by simp [mem_symmDiff, Set.mem_symmDiff]
 #align finset.coe_symm_diff Finset.coe_symmDiff
 
+@[simp] lemma symmDiff_eq_empty : s ∆ t = ∅ ↔ s = t := symmDiff_eq_bot
+@[simp] lemma symmDiff_nonempty : (s ∆ t).Nonempty ↔ s ≠ t :=
+  nonempty_iff_ne_empty.trans symmDiff_eq_empty.not
+
 end SymmDiff
 
 /-! ### attach -/

Mathlib/Data/Finset/Card.lean

@@ -462,6 +462,9 @@ theorem card_sdiff_add_card : (s \ t).card + t.card = (s ∪ t).card := by
   rw [← card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
 #align finset.card_sdiff_add_card Finset.card_sdiff_add_card
 
+lemma card_sdiff_comm (h : s.card = t.card) : (s \ t).card = (t \ s).card :=
+  add_left_injective t.card $ by simp_rw [card_sdiff_add_card, ←h, card_sdiff_add_card, union_comm]
+
 end Lattice
 
 theorem filter_card_add_filter_neg_card_eq_card

Mathlib/Data/Finset/Image.lean

@@ -337,6 +337,10 @@ theorem forall_image {p : β → Prop} : (∀ b ∈ s.image f, p b) ↔ ∀ a 
   simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 #align finset.forall_image Finset.forall_image
 
+theorem map_eq_image (f : α ↪ β) (s : Finset α) : s.map f = s.image f :=
+  eq_of_veq (s.map f).2.dedup.symm
+#align finset.map_eq_image Finset.map_eq_image
+
 --@[simp] Porting note: removing simp, `simp` [Nonempty] can prove it
 theorem mem_image_const : c ∈ s.image (const α b) ↔ s.Nonempty ∧ b = c := by
   rw [mem_image]
@@ -451,21 +455,31 @@ theorem image_subset_iff : s.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t :=
 theorem image_mono (f : α → β) : Monotone (Finset.image f) := fun _ _ => image_subset_image
 #align finset.image_mono Finset.image_mono
 
+lemma image_injective (hf : Injective f) : Injective (image f) := by
+  simpa only [funext (map_eq_image _)] using map_injective ⟨f, hf⟩
+
+lemma image_inj {t : Finset α} (hf : Injective f) : s.image f = t.image f ↔ s = t :=
+  (image_injective hf).eq_iff
+
 theorem image_subset_image_iff {t : Finset α} (hf : Injective f) :
     s.image f ⊆ t.image f ↔ s ⊆ t := by
   simp_rw [← coe_subset]
   push_cast
   exact Set.image_subset_image_iff hf
 #align finset.image_subset_image_iff Finset.image_subset_image_iff
 
+lemma image_ssubset_image {t : Finset α} (hf : Injective f) : s.image f ⊂ t.image f ↔ s ⊂ t := by
+  simp_rw [←lt_iff_ssubset]
+  exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)
+
 theorem coe_image_subset_range : ↑(s.image f) ⊆ Set.range f :=
   calc
     ↑(s.image f) = f '' ↑s := coe_image
     _ ⊆ Set.range f := Set.image_subset_range f ↑s
 #align finset.coe_image_subset_range Finset.coe_image_subset_range
 
 theorem image_filter {p : β → Prop} [DecidablePred p] :
-    (s.image f).filter p = (s.filter (p ∘ f)).image f :=
+    (s.image f).filter p = (s.filter λ a ↦ p (f a)).image f :=
   ext fun b => by
     simp only [mem_filter, mem_image, exists_prop]
     exact
@@ -600,10 +614,6 @@ theorem attach_insert [DecidableEq α] {a : α} {s : Finset α} :
       fun _ => Finset.mem_attach _ _⟩
 #align finset.attach_insert Finset.attach_insert
 
-theorem map_eq_image (f : α ↪ β) (s : Finset α) : s.map f = s.image f :=
-  eq_of_veq (s.map f).2.dedup.symm
-#align finset.map_eq_image Finset.map_eq_image
-
 @[simp]
 theorem disjoint_image {s t : Finset α} {f : α → β} (hf : Injective f) :
     Disjoint (s.image f) (t.image f) ↔ Disjoint s t := by

Mathlib/Data/Finset/Slice.lean

@@ -37,7 +37,7 @@ variable {α : Type*} {ι : Sort*} {κ : ι → Sort*}
 
 namespace Set
 
-variable {A B : Set (Finset α)} {r : ℕ}
+variable {A B : Set (Finset α)} {s : Finset α} {r : ℕ}
 
 /-! ### Families of `r`-sets -/
 
@@ -50,6 +50,9 @@ def Sized (r : ℕ) (A : Set (Finset α)) : Prop :=
 theorem Sized.mono (h : A ⊆ B) (hB : B.Sized r) : A.Sized r := fun _x hx => hB <| h hx
 #align set.sized.mono Set.Sized.mono
 
+@[simp] lemma sized_empty : (∅ : Set (Finset α)).Sized r := by simp [Sized]
+@[simp] lemma sized_singleton : ({s} : Set (Finset α)).Sized r ↔ s.card = r := by simp [Sized]
+
 theorem sized_union : (A ∪ B).Sized r ↔ A.Sized r ∧ B.Sized r :=
   ⟨fun hA => ⟨hA.mono <| subset_union_left _ _, hA.mono <| subset_union_right _ _⟩, fun hA _x hx =>
     hx.elim (fun h => hA.1 h) fun h => hA.2 h⟩
@@ -110,11 +113,11 @@ theorem subset_powersetLen_univ_iff : 𝒜 ⊆ powersetLen r univ ↔ (𝒜 : Se
 alias ⟨_, _root_.Set.Sized.subset_powersetLen_univ⟩ := subset_powersetLen_univ_iff
 #align set.sized.subset_powerset_len_univ Set.Sized.subset_powersetLen_univ
 
-theorem Set.Sized.card_le (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
+theorem _root_.Set.Sized.card_le (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
     card 𝒜 ≤ (Fintype.card α).choose r := by
   rw [Fintype.card, ← card_powersetLen]
   exact card_le_of_subset (subset_powersetLen_univ_iff.mpr h𝒜)
-#align set.sized.card_le Finset.Set.Sized.card_le
+#align set.sized.card_le Set.Sized.card_le
 
 end Sized