feat: Finset family induction (#7522)

Provide an induction principle for finset families: One can increase the support of a finset family one by one.

Mathlib/Combinatorics/SetFamily/Compression/Down.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Finset.Card
+import Mathlib.Data.Finset.Lattice
 
 #align_import combinatorics.set_family.compression.down from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
 
@@ -136,6 +136,84 @@ theorem nonMemberSubfamily_nonMemberSubfamily :
   simp
 #align finset.non_member_subfamily_non_member_subfamily Finset.nonMemberSubfamily_nonMemberSubfamily
 
+lemma memberSubfamily_image_insert (h𝒜 : ∀ s ∈ 𝒜, a ∉ s) :
+    (𝒜.image <| insert a).memberSubfamily a = 𝒜 := by
+  ext s
+  simp only [mem_memberSubfamily, mem_image]
+  refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
+  rintro ⟨⟨t, ht, hts⟩, hs⟩
+  rwa [←insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]
+
+@[simp] lemma nonMemberSubfamily_image_insert : (𝒜.image <| insert a).nonMemberSubfamily a = ∅ := by
+  simp [eq_empty_iff_forall_not_mem]
+
+@[simp] lemma memberSubfamily_image_erase : (𝒜.image (erase · a)).memberSubfamily a = ∅ := by
+  simp [eq_empty_iff_forall_not_mem,
+    (ne_of_mem_of_not_mem' (mem_insert_self _ _) (not_mem_erase _ _)).symm]
+
+lemma image_insert_memberSubfamily (𝒜 : Finset (Finset α)) (a : α) :
+    (𝒜.memberSubfamily a).image (insert a) = 𝒜.filter (a ∈ ·) := by
+  ext s
+  simp only [mem_memberSubfamily, mem_image, mem_filter]
+  refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, not_mem_erase _ _⟩, insert_erase ha⟩⟩
+  · rintro ⟨s, ⟨hs, -⟩, rfl⟩
+    exact ⟨hs, mem_insert_self _ _⟩
+  · rwa [insert_erase ha]
+
+/-- Induction principle for finset families. To prove a statement for every finset family,
+it suffices to prove it for
+* the empty finset family.
+* the finset family which only contains the empty finset.
+* `ℬ ∪ {s ∪ {a} | s ∈ 𝒞}` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the
+  ground type and `𝒜` and `ℬ` are families of finsets not containing `a`.
+  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you
+  `𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, so that `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.
+
+This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.
+
+See also `Finset.family_induction_on.`-/
+@[elab_as_elim]
+lemma memberFamily_induction_on {p : Finset (Finset α) → Prop}
+    (𝒜 : Finset (Finset α)) (empty : p ∅) (singleton_empty : p {∅})
+    (subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
+      p (𝒜.nonMemberSubfamily a) → p (𝒜.memberSubfamily a) → p 𝒜) : p 𝒜 := by
+  set u := 𝒜.sup id
+  have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)
+  clear_value u
+  induction' u using Finset.induction with a u _ ih generalizing 𝒜
+  · simp_rw [subset_empty] at hu
+    rw [←subset_singleton_iff', subset_singleton_iff] at hu
+    obtain rfl | rfl := hu <;> assumption
+  refine subfamily a (ih _ ?_) (ih _ ?_)
+  · simp only [mem_nonMemberSubfamily, and_imp]
+    exact fun s hs has ↦ (subset_insert_iff_of_not_mem has).1 <| hu _ hs
+  · simp only [mem_memberSubfamily, and_imp]
+    exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs
+
+/-- Induction principle for finset families. To prove a statement for every finset family,
+it suffices to prove it for
+* the empty finset family.
+* the finset family which only contains the empty finset.
+* `{s ∪ {a} | s ∈ 𝒜}` assuming the property for `𝒜` a family of finsets not containing `a`.
+* `ℬ ∪ 𝒞` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the ground type and
+  `ℬ`is a family of finsets not containing `a` and `𝒞` a family of finsets containing `a`.
+  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you `𝒜 = ℬ ∪ 𝒞`, so that
+  `ℬ = 𝒜.filter (a ∉ ·)` and `𝒞 = 𝒜.filter (a ∈ ·)`.
+
+This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.
+
+See also `Finset.memberFamily_induction_on.`-/
+@[elab_as_elim]
+protected lemma family_induction_on {p : Finset (Finset α) → Prop}
+    (𝒜 : Finset (Finset α)) (empty : p ∅) (singleton_empty : p {∅})
+    (image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
+      (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (𝒜.image <| insert a))
+    (subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
+      p (𝒜.filter (a ∉ ·)) → p (𝒜.filter (a ∈ ·)) → p 𝒜) : p 𝒜 := by
+  refine memberFamily_induction_on 𝒜 empty singleton_empty fun a 𝒜 h𝒜₀ h𝒜₁ ↦ subfamily a h𝒜₀ ?_
+  rw [←image_insert_memberSubfamily]
+  exact image_insert _ (by simp) h𝒜₁
+
 end Finset
 
 open Finset

Mathlib/Data/Finset/Basic.lean

@@ -1198,6 +1198,9 @@ theorem insert_subset_insert (a : α) {s t : Finset α} (h : s ⊆ t) : insert a
   insert_subset_iff.2 ⟨mem_insert_self _ _, Subset.trans h (subset_insert _ _)⟩
 #align finset.insert_subset_insert Finset.insert_subset_insert
 
+@[simp] lemma insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t := by
+  simp_rw [←coe_subset]; simp [-coe_subset, ha]
+
 theorem insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
   ⟨fun h => eq_of_not_mem_of_mem_insert (h.subst <| mem_insert_self _ _) ha, congr_arg (insert · s)⟩
 #align finset.insert_inj Finset.insert_inj

Mathlib/Data/Set/Basic.lean

@@ -1172,7 +1172,7 @@ theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t :=
 theorem insert_subset_insert (h : s ⊆ t) : insert a s ⊆ insert a t := fun _ => Or.imp_right (@h _)
 #align set.insert_subset_insert Set.insert_subset_insert
 
-theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t := by
+@[simp] theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t := by
   refine' ⟨fun h x hx => _, insert_subset_insert⟩
   rcases h (subset_insert _ _ hx) with (rfl | hxt)
   exacts [(ha hx).elim, hxt]