diff --git a/Mathlib.lean b/Mathlib.lean
index 61d60f8f92677..86580b32bcb95 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1673,6 +1673,7 @@ import Mathlib.Data.Finset.Pairwise
 import Mathlib.Data.Finset.Pi
 import Mathlib.Data.Finset.PiAntidiagonal
 import Mathlib.Data.Finset.PiInduction
+import Mathlib.Data.Finset.Piecewise
 import Mathlib.Data.Finset.Pointwise
 import Mathlib.Data.Finset.Pointwise.Interval
 import Mathlib.Data.Finset.Powerset
@@ -1684,6 +1685,7 @@ import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Finset.Sups
 import Mathlib.Data.Finset.Sym
+import Mathlib.Data.Finset.Union
 import Mathlib.Data.Finset.Update
 import Mathlib.Data.Finsupp.AList
 import Mathlib.Data.Finsupp.Antidiagonal
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index dbcce2ef8f9b3..fee96453ea00c 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.BigOperators.Multiset.Order
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Data.Finset.Powerset
+import Mathlib.Data.Finset.Piecewise
 import Mathlib.Data.Finset.Preimage
 import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Finset.Sum
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
index ad03ef5b0992e..22b53faa38684 100644
--- a/Mathlib/Data/Finset/Basic.lean
+++ b/Mathlib/Data/Finset/Basic.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Data.Finset.Attr
-import Mathlib.Data.Multiset.Bind
 import Mathlib.Data.Multiset.FinsetOps
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Logic.Equiv.Set
+import Mathlib.Order.Directed
 
 #align_import data.finset.basic from "leanprover-community/mathlib"@"442a83d738cb208d3600056c489be16900ba701d"
 
@@ -85,9 +86,6 @@ In Lean, we use lattice notation to talk about things involving unions and inter
   See `Finset.sup`/`Finset.biUnion` for finite unions.
 * `Finset.instInterFinset`: Defines `s ∩ t` (or `s ⊓ t`) as the intersection of `s` and `t`.
   See `Finset.inf` for finite intersections.
-* `Finset.disjUnion`: Given a hypothesis `h` which states that finsets `s` and `t` are disjoint,
-  `s.disjUnion t h` is the set such that `a ∈ disjUnion s t h` iff `a ∈ s` or `a ∈ t`; this does
-  not require decidable equality on the type `α`.
 
 ### Operations on two or more finsets
 
@@ -100,21 +98,12 @@ In Lean, we use lattice notation to talk about things involving unions and inter
 * `Finset.instSDiffFinset`: Defines the set difference `s \ t` for finsets `s` and `t`.
 * `Finset.product`: Given finsets of `α` and `β`, defines finsets of `α × β`.
   For arbitrary dependent products, see `Mathlib.Data.Finset.Pi`.
-* `Finset.biUnion`: Finite unions of finsets; given an indexing function `f : α → Finset β` and an
-  `s : Finset α`, `s.biUnion f` is the union of all finsets of the form `f a` for `a ∈ s`.
-* `Finset.bInter`: TODO: Implement finite intersections.
-
-### Maps constructed using finsets
-
-* `Finset.piecewise`: Given two functions `f`, `g`, `s.piecewise f g` is a function which is equal
-  to `f` on `s` and `g` on the complement.
 
 ### Predicates on finsets
 
 * `Disjoint`: defined via the lattice structure on finsets; two sets are disjoint if their
   intersection is empty.
-* `Finset.Nonempty`: A finset is nonempty if it has elements.
-  This is equivalent to saying `s ≠ ∅`. TODO: Decide on the simp normal form.
+* `Finset.Nonempty`: A finset is nonempty if it has elements. This is equivalent to saying `s ≠ ∅`.
 
 ### Equivalences between finsets
 
@@ -128,6 +117,12 @@ finite sets, finset
 
 -/
 
+-- Assert that we define `Finset` without the material on `List.sublists`.
+-- Note that we cannot use `List.sublists` itself as that is defined very early.
+assert_not_exists List.sublistsLen
+assert_not_exists Multiset.Powerset
+
+assert_not_exists CompleteLattice
 
 open Multiset Subtype Nat Function
 
@@ -1594,34 +1589,6 @@ theorem induction_on_union (P : Finset α → Finset α → Prop) (symm : ∀ {a
   exact union_of singletons (symm hi)
 #align finset.induction_on_union Finset.induction_on_union
 
-theorem _root_.Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [hn : Nonempty ι]
-    {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
-    ∃ i, (s : Set α) ⊆ f i := by
-  classical
-    revert hs
-    refine' s.induction_on _ _
-    · refine' fun _ => ⟨hn.some, _⟩
-      simp only [coe_empty, Set.empty_subset]
-    · intro b t _hbt htc hbtc
-      obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
-      obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
-      rcases h j i with ⟨k, hk, hk'⟩
-      use k
-      rw [coe_insert, Set.insert_subset_iff]
-      exact ⟨hk hbj, _root_.trans hti hk'⟩
-#align directed.exists_mem_subset_of_finset_subset_bUnion Directed.exists_mem_subset_of_finset_subset_biUnion
-
-theorem _root_.DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α}
-    {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α}
-    (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : Set α) ⊆ f i := by
-  rw [Set.biUnion_eq_iUnion] at hs
-  haveI := hn.coe_sort
-  obtain ⟨⟨i, hic⟩, hi⟩ :=
-    (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs
-  exact ⟨i, hic, hi⟩
-#align directed_on.exists_mem_subset_of_finset_subset_bUnion DirectedOn.exists_mem_subset_of_finset_subset_biUnion
-
-
 /-! #### inter -/
 
 
@@ -2552,175 +2519,6 @@ theorem attach_eq_empty_iff {s : Finset α} : s.attach = ∅ ↔ s = ∅ := by
   simp [eq_empty_iff_forall_not_mem]
 #align finset.attach_eq_empty_iff Finset.attach_eq_empty_iff
 
-/-! ### piecewise -/
-
-
-section Piecewise
-
-/-- `s.piecewise f g` is the function equal to `f` on the finset `s`, and to `g` on its
-complement. -/
-def piecewise {α : Type*} {δ : α → Sort*} (s : Finset α) (f g : ∀ i, δ i)
-    [∀ j, Decidable (j ∈ s)] : ∀ i, δ i := fun i => if i ∈ s then f i else g i
-#align finset.piecewise Finset.piecewise
-
-variable {δ : α → Sort*} (s : Finset α) (f g : ∀ i, δ i)
-
--- Porting note (#10618): @[simp] can prove this
-theorem piecewise_insert_self [DecidableEq α] {j : α} [∀ i, Decidable (i ∈ insert j s)] :
-    (insert j s).piecewise f g j = f j := by simp [piecewise]
-#align finset.piecewise_insert_self Finset.piecewise_insert_self
-
-@[simp]
-theorem piecewise_empty [∀ i : α, Decidable (i ∈ (∅ : Finset α))] : piecewise ∅ f g = g := by
-  ext i
-  simp [piecewise]
-#align finset.piecewise_empty Finset.piecewise_empty
-
-variable [∀ j, Decidable (j ∈ s)]
-
--- TODO: fix this in norm_cast
-@[norm_cast move]
-theorem piecewise_coe [∀ j, Decidable (j ∈ (s : Set α))] :
-    (s : Set α).piecewise f g = s.piecewise f g := by
-  ext
-  congr
-#align finset.piecewise_coe Finset.piecewise_coe
-
-@[simp]
-theorem piecewise_eq_of_mem {i : α} (hi : i ∈ s) : s.piecewise f g i = f i := by
-  simp [piecewise, hi]
-#align finset.piecewise_eq_of_mem Finset.piecewise_eq_of_mem
-
-@[simp]
-theorem piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i := by
-  simp [piecewise, hi]
-#align finset.piecewise_eq_of_not_mem Finset.piecewise_eq_of_not_mem
-
-theorem piecewise_congr {f f' g g' : ∀ i, δ i} (hf : ∀ i ∈ s, f i = f' i)
-    (hg : ∀ i ∉ s, g i = g' i) : s.piecewise f g = s.piecewise f' g' :=
-  funext fun i => if_ctx_congr Iff.rfl (hf i) (hg i)
-#align finset.piecewise_congr Finset.piecewise_congr
-
-@[simp]
-theorem piecewise_insert_of_ne [DecidableEq α] {i j : α} [∀ i, Decidable (i ∈ insert j s)]
-    (h : i ≠ j) : (insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]
-#align finset.piecewise_insert_of_ne Finset.piecewise_insert_of_ne
-
-theorem piecewise_insert [DecidableEq α] (j : α) [∀ i, Decidable (i ∈ insert j s)] :
-    (insert j s).piecewise f g = update (s.piecewise f g) j (f j) := by
-  classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
-  ext
-  congr
-  simp
-#align finset.piecewise_insert Finset.piecewise_insert
-
-theorem piecewise_cases {i} (p : δ i → Prop) (hf : p (f i)) (hg : p (g i)) :
-    p (s.piecewise f g i) := by
-  by_cases hi : i ∈ s <;> simpa [hi]
-#align finset.piecewise_cases Finset.piecewise_cases
-
-theorem piecewise_mem_set_pi {δ : α → Type*} {t : Set α} {t' : ∀ i, Set (δ i)} {f g}
-    (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') : s.piecewise f g ∈ Set.pi t t' := by
-  classical
-    rw [← piecewise_coe]
-    exact Set.piecewise_mem_pi (↑s) hf hg
-#align finset.piecewise_mem_set_pi Finset.piecewise_mem_set_pi
-
-theorem piecewise_singleton [DecidableEq α] (i : α) : piecewise {i} f g = update g i (f i) := by
-  rw [← insert_emptyc_eq, piecewise_insert, piecewise_empty]
-#align finset.piecewise_singleton Finset.piecewise_singleton
-
-theorem piecewise_piecewise_of_subset_left {s t : Finset α} [∀ i, Decidable (i ∈ s)]
-    [∀ i, Decidable (i ∈ t)] (h : s ⊆ t) (f₁ f₂ g : ∀ a, δ a) :
-    s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g :=
-  s.piecewise_congr (fun _i hi => piecewise_eq_of_mem _ _ _ (h hi)) fun _ _ => rfl
-#align finset.piecewise_piecewise_of_subset_left Finset.piecewise_piecewise_of_subset_left
-
-@[simp]
-theorem piecewise_idem_left (f₁ f₂ g : ∀ a, δ a) :
-    s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g :=
-  piecewise_piecewise_of_subset_left (Subset.refl _) _ _ _
-#align finset.piecewise_idem_left Finset.piecewise_idem_left
-
-theorem piecewise_piecewise_of_subset_right {s t : Finset α} [∀ i, Decidable (i ∈ s)]
-    [∀ i, Decidable (i ∈ t)] (h : t ⊆ s) (f g₁ g₂ : ∀ a, δ a) :
-    s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂ :=
-  s.piecewise_congr (fun _ _ => rfl) fun _i hi => t.piecewise_eq_of_not_mem _ _ (mt (@h _) hi)
-#align finset.piecewise_piecewise_of_subset_right Finset.piecewise_piecewise_of_subset_right
-
-@[simp]
-theorem piecewise_idem_right (f g₁ g₂ : ∀ a, δ a) :
-    s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂ :=
-  piecewise_piecewise_of_subset_right (Subset.refl _) f g₁ g₂
-#align finset.piecewise_idem_right Finset.piecewise_idem_right
-
-theorem update_eq_piecewise {β : Type*} [DecidableEq α] (f : α → β) (i : α) (v : β) :
-    update f i v = piecewise (singleton i) (fun _ => v) f :=
-  (piecewise_singleton (fun _ => v) _ _).symm
-#align finset.update_eq_piecewise Finset.update_eq_piecewise
-
-theorem update_piecewise [DecidableEq α] (i : α) (v : δ i) :
-    update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v) := by
-  ext j
-  rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]
-#align finset.update_piecewise Finset.update_piecewise
-
-theorem update_piecewise_of_mem [DecidableEq α] {i : α} (hi : i ∈ s) (v : δ i) :
-    update (s.piecewise f g) i v = s.piecewise (update f i v) g := by
-  rw [update_piecewise]
-  refine' s.piecewise_congr (fun _ _ => rfl) fun j hj => update_noteq _ _ _
-  exact fun h => hj (h.symm ▸ hi)
-#align finset.update_piecewise_of_mem Finset.update_piecewise_of_mem
-
-theorem update_piecewise_of_not_mem [DecidableEq α] {i : α} (hi : i ∉ s) (v : δ i) :
-    update (s.piecewise f g) i v = s.piecewise f (update g i v) := by
-  rw [update_piecewise]
-  refine' s.piecewise_congr (fun j hj => update_noteq _ _ _) fun _ _ => rfl
-  exact fun h => hi (h ▸ hj)
-#align finset.update_piecewise_of_not_mem Finset.update_piecewise_of_not_mem
-
-theorem piecewise_le_of_le_of_le {δ : α → Type*} [∀ i, Preorder (δ i)] {f g h : ∀ i, δ i}
-    (Hf : f ≤ h) (Hg : g ≤ h) : s.piecewise f g ≤ h := fun x =>
-  piecewise_cases s f g (· ≤ h x) (Hf x) (Hg x)
-#align finset.piecewise_le_of_le_of_le Finset.piecewise_le_of_le_of_le
-
-theorem le_piecewise_of_le_of_le {δ : α → Type*} [∀ i, Preorder (δ i)] {f g h : ∀ i, δ i}
-    (Hf : h ≤ f) (Hg : h ≤ g) : h ≤ s.piecewise f g := fun x =>
-  piecewise_cases s f g (fun y => h x ≤ y) (Hf x) (Hg x)
-#align finset.le_piecewise_of_le_of_le Finset.le_piecewise_of_le_of_le
-
-theorem piecewise_le_piecewise' {δ : α → Type*} [∀ i, Preorder (δ i)] {f g f' g' : ∀ i, δ i}
-    (Hf : ∀ x ∈ s, f x ≤ f' x) (Hg : ∀ x ∉ s, g x ≤ g' x) :
-    s.piecewise f g ≤ s.piecewise f' g' := fun x => by by_cases hx : x ∈ s <;> simp [hx, *]
-#align finset.piecewise_le_piecewise' Finset.piecewise_le_piecewise'
-
-theorem piecewise_le_piecewise {δ : α → Type*} [∀ i, Preorder (δ i)] {f g f' g' : ∀ i, δ i}
-    (Hf : f ≤ f') (Hg : g ≤ g') : s.piecewise f g ≤ s.piecewise f' g' :=
-  s.piecewise_le_piecewise' (fun x _ => Hf x) fun x _ => Hg x
-#align finset.piecewise_le_piecewise Finset.piecewise_le_piecewise
-
-theorem piecewise_mem_Icc_of_mem_of_mem {δ : α → Type*} [∀ i, Preorder (δ i)]
-    {f f₁ g g₁ : ∀ i, δ i} (hf : f ∈ Set.Icc f₁ g₁) (hg : g ∈ Set.Icc f₁ g₁) :
-    s.piecewise f g ∈ Set.Icc f₁ g₁ :=
-  ⟨le_piecewise_of_le_of_le _ hf.1 hg.1, piecewise_le_of_le_of_le _ hf.2 hg.2⟩
-#align finset.piecewise_mem_Icc_of_mem_of_mem Finset.piecewise_mem_Icc_of_mem_of_mem
-
-theorem piecewise_mem_Icc {δ : α → Type*} [∀ i, Preorder (δ i)] {f g : ∀ i, δ i} (h : f ≤ g) :
-    s.piecewise f g ∈ Set.Icc f g :=
-  piecewise_mem_Icc_of_mem_of_mem _ (Set.left_mem_Icc.2 h) (Set.right_mem_Icc.2 h)
-#align finset.piecewise_mem_Icc Finset.piecewise_mem_Icc
-
-theorem piecewise_mem_Icc' {δ : α → Type*} [∀ i, Preorder (δ i)] {f g : ∀ i, δ i} (h : g ≤ f) :
-    s.piecewise f g ∈ Set.Icc g f :=
-  piecewise_mem_Icc_of_mem_of_mem _ (Set.right_mem_Icc.2 h) (Set.left_mem_Icc.2 h)
-#align finset.piecewise_mem_Icc' Finset.piecewise_mem_Icc'
-
-lemma piecewise_same : s.piecewise f f = f := by
-  ext i
-  by_cases h : i ∈ s <;> simp [h]
-
-end Piecewise
-
 section DecidablePiExists
 
 variable {s : Finset α}
@@ -3251,9 +3049,9 @@ def notMemRangeEquiv (k : ℕ) : { n // n ∉ range k } ≃ ℕ where
   invFun j := ⟨j + k, by simp⟩
   left_inv j := by
     rw [Subtype.ext_iff_val]
-    apply tsub_add_cancel_of_le
+    apply Nat.sub_add_cancel
     simpa using j.2
-  right_inv j := add_tsub_cancel_right _ _
+  right_inv j := Nat.add_sub_cancel_right _ _
 #align not_mem_range_equiv notMemRangeEquiv
 
 @[simp]
@@ -3379,15 +3177,10 @@ theorem toFinset_dedup (m : Multiset α) : m.dedup.toFinset = m.toFinset := by
   simp_rw [toFinset, dedup_idem]
 #align multiset.to_finset_dedup Multiset.toFinset_dedup
 
-@[simp]
-theorem toFinset_bind_dedup [DecidableEq β] (m : Multiset α) (f : α → Multiset β) :
-    (m.dedup.bind f).toFinset = (m.bind f).toFinset := by simp_rw [toFinset, dedup_bind_dedup]
-#align multiset.to_finset_bind_dedup Multiset.toFinset_bind_dedup
-
-@[simp]
-theorem toFinset_range (n : ℕ) :
-    Multiset.toFinset (Multiset.range n) = Finset.range n := by
-  ext; simp
+-- @[simp]
+-- theorem toFinset_bind_dedup [DecidableEq β] (m : Multiset α) (f : α → Multiset β) :
+--     (m.dedup.bind f).toFinset = (m.bind f).toFinset := by simp_rw [toFinset, dedup_bind_dedup]
+-- #align multiset.to_finset_bind_dedup Multiset.toFinset_bind_dedup
 
 @[simp]
 theorem toFinset_filter (s : Multiset α) (p : α → Prop) [DecidablePred p] :
@@ -3530,10 +3323,6 @@ theorem toFinset_nonempty_iff (l : List α) : l.toFinset.Nonempty ↔ l ≠ [] :
   simp [Finset.nonempty_iff_ne_empty]
 #align list.to_finset_nonempty_iff List.toFinset_nonempty_iff
 
-@[simp]
-theorem toFinset_range (n : ℕ) : (List.range n).toFinset = Finset.range n := by
-  ext; simp
-
 @[simp]
 theorem toFinset_filter (s : List α) (p : α → Bool) :
     (s.filter p).toFinset = s.toFinset.filter (p ·) := by
@@ -3623,275 +3412,6 @@ theorem toList_insert [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) :
 
 end ToList
 
-/-!
-### disjiUnion
-
-This section is about the bounded union of a disjoint indexed family `t : α → Finset β` of finite
-sets over a finite set `s : Finset α`. In most cases `Finset.biUnion` should be preferred.
--/
-
-
-section DisjiUnion
-
-variable {s s₁ s₂ : Finset α} {t t₁ t₂ : α → Finset β}
-
-/-- `disjiUnion s f h` is the set such that `a ∈ disjiUnion s f` iff `a ∈ f i` for some `i ∈ s`.
-It is the same as `s.biUnion f`, but it does not require decidable equality on the type. The
-hypothesis ensures that the sets are disjoint. -/
-def disjiUnion (s : Finset α) (t : α → Finset β) (hf : (s : Set α).PairwiseDisjoint t) : Finset β :=
-  ⟨s.val.bind (Finset.val ∘ t),
-    Multiset.nodup_bind.mpr
-      ⟨fun a _ => (t a).nodup,
-        s.nodup.pairwise fun _ ha _ hb hab => disjoint_val.2 <| hf ha hb hab⟩⟩
-#align finset.disj_Union Finset.disjUnionₓ -- Porting note: universes and more
-
-@[simp]
-theorem disjiUnion_val (s : Finset α) (t : α → Finset β) (h) :
-    (s.disjiUnion t h).1 = s.1.bind fun a => (t a).1 :=
-  rfl
-#align finset.disj_Union_val Finset.disjiUnion_val
-
-@[simp]
-theorem disjiUnion_empty (t : α → Finset β) : disjiUnion ∅ t (by simp) = ∅ :=
-  rfl
-#align finset.disj_Union_empty Finset.disjiUnion_empty
-
-@[simp]
-theorem mem_disjiUnion {b : β} {h} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a := by
-  simp only [mem_def, disjiUnion_val, mem_bind, exists_prop]
-#align finset.mem_disj_Union Finset.mem_disjiUnion
-
-@[simp, norm_cast]
-theorem coe_disjiUnion {h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x := by
-  simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
-#align finset.coe_disj_Union Finset.coe_disjiUnion
-
-@[simp]
-theorem disjiUnion_cons (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H) :
-    disjiUnion (cons a s ha) f H =
-    (f a).disjUnion ((s.disjiUnion f) fun _ hb _ hc => H (mem_cons_of_mem hb) (mem_cons_of_mem hc))
-      (disjoint_left.mpr fun _ hb h =>
-        let ⟨_, hc, h⟩ := mem_disjiUnion.mp h
-        disjoint_left.mp
-          (H (mem_cons_self a s) (mem_cons_of_mem hc) (ne_of_mem_of_not_mem hc ha).symm) hb h) :=
-  eq_of_veq <| Multiset.cons_bind _ _ _
-#align finset.disj_Union_cons Finset.disjiUnion_cons
-
-@[simp]
-theorem singleton_disjiUnion (a : α) {h} : Finset.disjiUnion {a} t h = t a :=
-  eq_of_veq <| Multiset.singleton_bind _ _
-#align finset.singleton_disj_Union Finset.singleton_disjiUnion
-
-theorem disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 h2) :
-    (s.disjiUnion f h1).disjiUnion g h2 =
-      s.attach.disjiUnion
-        (fun a =>
-          ((f a).disjiUnion g) fun b hb c hc =>
-            h2 (mem_disjiUnion.mpr ⟨_, a.prop, hb⟩) (mem_disjiUnion.mpr ⟨_, a.prop, hc⟩))
-        fun a _ b _ hab =>
-        disjoint_left.mpr fun x hxa hxb => by
-          obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
-          obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
-          refine'
-            disjoint_left.mp
-              (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) _) hga
-              hgb
-          rintro rfl
-          exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb :=
-  eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm
-#align finset.disj_Union_disj_Union Finset.disjiUnion_disjiUnion
-
-theorem disjiUnion_filter_eq_of_maps_to [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
-    (h : ∀ x ∈ s, f x ∈ t) :
-    t.disjiUnion (fun a => s.filter (fun c => f c = a))
-      (fun x' hx y' hy hne => by
-        simp_rw [disjoint_left, mem_filter]
-        rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
-        exact hne rfl) = s :=
-  ext fun b => by simpa using h b
-#align finset.disj_Union_filter_eq_of_maps_to Finset.disjiUnion_filter_eq_of_maps_to
-
-end DisjiUnion
-
-section BUnion
-
-/-!
-### biUnion
-
-This section is about the bounded union of an indexed family `t : α → Finset β` of finite sets
-over a finite set `s : Finset α`.
--/
-
--- TODO: should be `biUnion`
-
-variable [DecidableEq β] {s s₁ s₂ : Finset α} {t t₁ t₂ : α → Finset β}
-
-/-- `biUnion s t` is the union of `t x` over `x ∈ s`.
-(This was formerly `bind` due to the monad structure on types with `DecidableEq`.) -/
-protected def biUnion (s : Finset α) (t : α → Finset β) : Finset β :=
-  (s.1.bind fun a => (t a).1).toFinset
-#align finset.bUnion Finset.biUnion
-
-@[simp]
-theorem biUnion_val (s : Finset α) (t : α → Finset β) :
-    (s.biUnion t).1 = (s.1.bind fun a => (t a).1).dedup :=
-  rfl
-#align finset.bUnion_val Finset.biUnion_val
-
-@[simp]
-theorem biUnion_empty : Finset.biUnion ∅ t = ∅ :=
-  rfl
-#align finset.bUnion_empty Finset.biUnion_empty
-
-@[simp]
-theorem mem_biUnion {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a := by
-  simp only [mem_def, biUnion_val, mem_dedup, mem_bind, exists_prop]
-#align finset.mem_bUnion Finset.mem_biUnion
-
-@[simp, norm_cast]
-theorem coe_biUnion : (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x := by
-  simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
-#align finset.coe_bUnion Finset.coe_biUnion
-
-@[simp]
-theorem biUnion_insert [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t :=
-  ext fun x => by
-    simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or,
-      exists_eq_left]
-#align finset.bUnion_insert Finset.biUnion_insert
-
-theorem biUnion_congr (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂ :=
-  ext fun x ↦ by
-    -- Porting note: this entire proof was `simp [or_and_distrib_right, exists_or_distrib]`
-    simp_rw [mem_biUnion]
-    apply exists_congr
-    simp (config := { contextual := true }) only [hs, and_congr_right_iff, ht, implies_true]
-#align finset.bUnion_congr Finset.biUnion_congr
-
-@[simp]
-theorem disjiUnion_eq_biUnion (s : Finset α) (f : α → Finset β) (hf) :
-    s.disjiUnion f hf = s.biUnion f :=
-  eq_of_veq (s.disjiUnion f hf).nodup.dedup.symm
-#align finset.disj_Union_eq_bUnion Finset.disjiUnion_eq_biUnion
-
-theorem biUnion_subset {s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s' := by
-  simp only [subset_iff, mem_biUnion]
-  exact ⟨fun H a ha b hb => H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ => H a ha hb⟩
-#align finset.bUnion_subset Finset.biUnion_subset
-
-@[simp]
-theorem singleton_biUnion {a : α} : Finset.biUnion {a} t = t a := by
-  classical rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]
-#align finset.singleton_bUnion Finset.singleton_biUnion
-
-theorem biUnion_inter (s : Finset α) (f : α → Finset β) (t : Finset β) :
-    s.biUnion f ∩ t = s.biUnion fun x => f x ∩ t := by
-  ext x
-  simp only [mem_biUnion, mem_inter]
-  tauto
-#align finset.bUnion_inter Finset.biUnion_inter
-
-theorem inter_biUnion (t : Finset β) (s : Finset α) (f : α → Finset β) :
-    t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x := by
-  rw [inter_comm, biUnion_inter]
-  simp [inter_comm]
-#align finset.inter_bUnion Finset.inter_biUnion
-
-theorem biUnion_biUnion [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
-    (s.biUnion f).biUnion g = s.biUnion fun a => (f a).biUnion g := by
-  ext
-  simp only [Finset.mem_biUnion, exists_prop]
-  simp_rw [← exists_and_right, ← exists_and_left, and_assoc]
-  rw [exists_comm]
-#align finset.bUnion_bUnion Finset.biUnion_biUnion
-
-theorem bind_toFinset [DecidableEq α] (s : Multiset α) (t : α → Multiset β) :
-    (s.bind t).toFinset = s.toFinset.biUnion fun a => (t a).toFinset :=
-  ext fun x => by simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]
-#align finset.bind_to_finset Finset.bind_toFinset
-
-theorem biUnion_mono (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂ := by
-  have : ∀ b a, a ∈ s → b ∈ t₁ a → ∃ a : α, a ∈ s ∧ b ∈ t₂ a := fun b a ha hb =>
-    ⟨a, ha, Finset.mem_of_subset (h a ha) hb⟩
-  simpa only [subset_iff, mem_biUnion, exists_imp, and_imp, exists_prop]
-#align finset.bUnion_mono Finset.biUnion_mono
-
-theorem biUnion_subset_biUnion_of_subset_left (t : α → Finset β) (h : s₁ ⊆ s₂) :
-    s₁.biUnion t ⊆ s₂.biUnion t := by
-  intro x
-  simp only [and_imp, mem_biUnion, exists_prop]
-  exact Exists.imp fun a ha => ⟨h ha.1, ha.2⟩
-#align finset.bUnion_subset_bUnion_of_subset_left Finset.biUnion_subset_biUnion_of_subset_left
-
-theorem subset_biUnion_of_mem (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u :=
-  singleton_biUnion.superset.trans <|
-    biUnion_subset_biUnion_of_subset_left u <| singleton_subset_iff.2 xs
-#align finset.subset_bUnion_of_mem Finset.subset_biUnion_of_mem
-
-@[simp]
-theorem biUnion_subset_iff_forall_subset {α β : Type*} [DecidableEq β] {s : Finset α}
-    {t : Finset β} {f : α → Finset β} : s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t :=
-  ⟨fun h _ hx => (subset_biUnion_of_mem f hx).trans h, fun h _ hx =>
-    let ⟨_, ha₁, ha₂⟩ := mem_biUnion.mp hx
-    h _ ha₁ ha₂⟩
-#align finset.bUnion_subset_iff_forall_subset Finset.biUnion_subset_iff_forall_subset
-
-@[simp]
-theorem biUnion_singleton_eq_self [DecidableEq α] : s.biUnion (singleton : α → Finset α) = s :=
-  ext fun x => by simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']
-#align finset.bUnion_singleton_eq_self Finset.biUnion_singleton_eq_self
-
-theorem filter_biUnion (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] :
-    (s.biUnion f).filter p = s.biUnion fun a => (f a).filter p := by
-  ext b
-  simp only [mem_biUnion, exists_prop, mem_filter]
-  constructor
-  · rintro ⟨⟨a, ha, hba⟩, hb⟩
-    exact ⟨a, ha, hba, hb⟩
-  · rintro ⟨a, ha, hba, hb⟩
-    exact ⟨⟨a, ha, hba⟩, hb⟩
-#align finset.filter_bUnion Finset.filter_biUnion
-
-theorem biUnion_filter_eq_of_maps_to [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β}
-    (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun a => s.filter fun c => f c = a) = s := by
-  simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h
-#align finset.bUnion_filter_eq_of_maps_to Finset.biUnion_filter_eq_of_maps_to
-
-theorem erase_biUnion (f : α → Finset β) (s : Finset α) (b : β) :
-    (s.biUnion f).erase b = s.biUnion fun x => (f x).erase b := by
-  ext a
-  simp only [mem_biUnion, not_exists, not_and, mem_erase, ne_eq]
-  tauto
-#align finset.erase_bUnion Finset.erase_biUnion
-
-@[simp]
-theorem biUnion_nonempty : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty := by
-  simp only [Finset.Nonempty, mem_biUnion]
-  rw [exists_swap]
-  simp [exists_and_left]
-#align finset.bUnion_nonempty Finset.biUnion_nonempty
-
-theorem Nonempty.biUnion (hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) :
-    (s.biUnion t).Nonempty :=
-  biUnion_nonempty.2 <| hs.imp fun x hx => ⟨hx, ht x hx⟩
-#align finset.nonempty.bUnion Finset.Nonempty.biUnion
-
-theorem disjoint_biUnion_left (s : Finset α) (f : α → Finset β) (t : Finset β) :
-    Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t := by
-  classical
-    refine' s.induction _ _
-    · simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
-    · intro i s his ih
-      simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]
-#align finset.disjoint_bUnion_left Finset.disjoint_biUnion_left
-
-theorem disjoint_biUnion_right (s : Finset β) (t : Finset α) (f : α → Finset β) :
-    Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i) := by
-  simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s
-#align finset.disjoint_bUnion_right Finset.disjoint_biUnion_right
-
-end BUnion
-
 /-! ### choose -/
 
 
@@ -3991,6 +3511,7 @@ def piFinsetUnion {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h
 
 end Equiv
 
+
 namespace Multiset
 
 variable [DecidableEq α]
@@ -4018,11 +3539,6 @@ theorem disjoint_toFinset_iff_disjoint : _root_.Disjoint l.toFinset l'.toFinset
 
 end List
 
--- Assert that we define `Finset` without the material on `List.sublists`.
--- Note that we cannot use `List.sublists` itself as that is defined very early.
-assert_not_exists List.sublistsLen
-assert_not_exists Multiset.powerset
-
 namespace Mathlib.Meta
 open Qq Lean Meta Finset
 
diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 7e1f69bc19569..3b3a667b01473 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Embedding
 import Mathlib.Data.Fin.Basic
-import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Union
 import Mathlib.Data.Int.Order.Basic
 
 #align_import data.finset.image from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
index adce2d9434b41..86dddac24ffb7 100644
--- a/Mathlib/Data/Finset/Lattice.lean
+++ b/Mathlib/Data/Finset/Lattice.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Finset.Option
 import Mathlib.Data.Finset.Pi
 import Mathlib.Data.Finset.Prod
 import Mathlib.Data.Multiset.Lattice
+import Mathlib.Data.Set.Lattice
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.Hom.Lattice
 
diff --git a/Mathlib/Data/Finset/Piecewise.lean b/Mathlib/Data/Finset/Piecewise.lean
new file mode 100644
index 0000000000000..a6b60de52b913
--- /dev/null
+++ b/Mathlib/Data/Finset/Piecewise.lean
@@ -0,0 +1,204 @@
+/-
+Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Set.Intervals.Basic
+
+/-!
+# Functions defined piecewise on a finset
+
+This file defines `Finset.piecewise`: Given two functions `f`, `g`, `s.piecewise f g` is a function
+which is equal to `f` on `s` and `g` on the complement.
+
+## TODO
+
+Should we deduplicate this from `Set.piecewise`?
+-/
+
+open Function
+
+namespace Finset
+variable {ι : Type*} {π : ι → Sort*} (s : Finset ι) (f g : ∀ i, π i)
+
+/-- `s.piecewise f g` is the function equal to `f` on the finset `s`, and to `g` on its
+complement. -/
+def piecewise [∀ j, Decidable (j ∈ s)] : ∀ i, π i := fun i ↦ if i ∈ s then f i else g i
+#align finset.piecewise Finset.piecewise
+
+-- Porting note (#10618): @[simp] can prove this
+lemma piecewise_insert_self [DecidableEq ι] {j : ι} [∀ i, Decidable (i ∈ insert j s)] :
+    (insert j s).piecewise f g j = f j := by simp [piecewise]
+#align finset.piecewise_insert_self Finset.piecewise_insert_self
+
+@[simp]
+lemma piecewise_empty [∀ i : ι, Decidable (i ∈ (∅ : Finset ι))] : piecewise ∅ f g = g := by
+  ext i
+  simp [piecewise]
+#align finset.piecewise_empty Finset.piecewise_empty
+
+variable [∀ j, Decidable (j ∈ s)]
+
+-- TODO: fix this in norm_cast
+@[norm_cast move]
+lemma piecewise_coe [∀ j, Decidable (j ∈ (s : Set ι))] :
+    (s : Set ι).piecewise f g = s.piecewise f g := by
+  ext
+  congr
+#align finset.piecewise_coe Finset.piecewise_coe
+
+@[simp]
+lemma piecewise_eq_of_mem {i : ι} (hi : i ∈ s) : s.piecewise f g i = f i := by
+  simp [piecewise, hi]
+#align finset.piecewise_eq_of_mem Finset.piecewise_eq_of_mem
+
+@[simp]
+lemma piecewise_eq_of_not_mem {i : ι} (hi : i ∉ s) : s.piecewise f g i = g i := by
+  simp [piecewise, hi]
+#align finset.piecewise_eq_of_not_mem Finset.piecewise_eq_of_not_mem
+
+lemma piecewise_congr {f f' g g' : ∀ i, π i} (hf : ∀ i ∈ s, f i = f' i)
+    (hg : ∀ i ∉ s, g i = g' i) : s.piecewise f g = s.piecewise f' g' :=
+  funext fun i => if_ctx_congr Iff.rfl (hf i) (hg i)
+#align finset.piecewise_congr Finset.piecewise_congr
+
+@[simp]
+lemma piecewise_insert_of_ne [DecidableEq ι] {i j : ι} [∀ i, Decidable (i ∈ insert j s)]
+    (h : i ≠ j) : (insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]
+#align finset.piecewise_insert_of_ne Finset.piecewise_insert_of_ne
+
+lemma piecewise_insert [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
+    (insert j s).piecewise f g = update (s.piecewise f g) j (f j) := by
+  classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
+  ext
+  congr
+  simp
+#align finset.piecewise_insert Finset.piecewise_insert
+
+lemma piecewise_cases {i} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) :
+    p (s.piecewise f g i) := by
+  by_cases hi : i ∈ s <;> simpa [hi]
+#align finset.piecewise_cases Finset.piecewise_cases
+
+lemma piecewise_singleton [DecidableEq ι] (i : ι) : piecewise {i} f g = update g i (f i) := by
+  rw [← insert_emptyc_eq, piecewise_insert, piecewise_empty]
+#align finset.piecewise_singleton Finset.piecewise_singleton
+
+lemma piecewise_piecewise_of_subset_left {s t : Finset ι} [∀ i, Decidable (i ∈ s)]
+    [∀ i, Decidable (i ∈ t)] (h : s ⊆ t) (f₁ f₂ g : ∀ a, π a) :
+    s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g :=
+  s.piecewise_congr (fun _i hi => piecewise_eq_of_mem _ _ _ (h hi)) fun _ _ => rfl
+#align finset.piecewise_piecewise_of_subset_left Finset.piecewise_piecewise_of_subset_left
+
+@[simp]
+lemma piecewise_idem_left (f₁ f₂ g : ∀ a, π a) :
+    s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g :=
+  piecewise_piecewise_of_subset_left (Subset.refl _) _ _ _
+#align finset.piecewise_idem_left Finset.piecewise_idem_left
+
+lemma piecewise_piecewise_of_subset_right {s t : Finset ι} [∀ i, Decidable (i ∈ s)]
+    [∀ i, Decidable (i ∈ t)] (h : t ⊆ s) (f g₁ g₂ : ∀ a, π a) :
+    s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂ :=
+  s.piecewise_congr (fun _ _ => rfl) fun _i hi => t.piecewise_eq_of_not_mem _ _ (mt (@h _) hi)
+#align finset.piecewise_piecewise_of_subset_right Finset.piecewise_piecewise_of_subset_right
+
+@[simp]
+lemma piecewise_idem_right (f g₁ g₂ : ∀ a, π a) :
+    s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂ :=
+  piecewise_piecewise_of_subset_right (Subset.refl _) f g₁ g₂
+#align finset.piecewise_idem_right Finset.piecewise_idem_right
+
+lemma update_eq_piecewise {β : Type*} [DecidableEq ι] (f : ι → β) (i : ι) (v : β) :
+    update f i v = piecewise (singleton i) (fun _ => v) f :=
+  (piecewise_singleton (fun _ => v) _ _).symm
+#align finset.update_eq_piecewise Finset.update_eq_piecewise
+
+lemma update_piecewise [DecidableEq ι] (i : ι) (v : π i) :
+    update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v) := by
+  ext j
+  rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]
+#align finset.update_piecewise Finset.update_piecewise
+
+lemma update_piecewise_of_mem [DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) :
+    update (s.piecewise f g) i v = s.piecewise (update f i v) g := by
+  rw [update_piecewise]
+  refine' s.piecewise_congr (fun _ _ => rfl) fun j hj => update_noteq _ _ _
+  exact fun h => hj (h.symm ▸ hi)
+#align finset.update_piecewise_of_mem Finset.update_piecewise_of_mem
+
+lemma update_piecewise_of_not_mem [DecidableEq ι] {i : ι} (hi : i ∉ s) (v : π i) :
+    update (s.piecewise f g) i v = s.piecewise f (update g i v) := by
+  rw [update_piecewise]
+  refine' s.piecewise_congr (fun j hj => update_noteq _ _ _) fun _ _ => rfl
+  exact fun h => hi (h ▸ hj)
+#align finset.update_piecewise_of_not_mem Finset.update_piecewise_of_not_mem
+
+lemma piecewise_same : s.piecewise f f = f := by
+  ext i
+  by_cases h : i ∈ s <;> simp [h]
+
+section Fintype
+variable [Fintype ι]
+
+@[simp]
+lemma piecewise_univ [∀ i, Decidable (i ∈ (univ : Finset ι))] (f g : ∀ i, π i) :
+    univ.piecewise f g = f := by
+  ext i
+  simp [piecewise]
+#align finset.piecewise_univ Finset.piecewise_univ
+
+lemma piecewise_compl [DecidableEq ι] (s : Finset ι) [∀ i, Decidable (i ∈ s)]
+    [∀ i, Decidable (i ∈ sᶜ)] (f g : ∀ i, π i) :
+    sᶜ.piecewise f g = s.piecewise g f := by
+  ext i
+  simp [piecewise]
+#align finset.piecewise_compl Finset.piecewise_compl
+
+@[simp]
+lemma piecewise_erase_univ [DecidableEq ι] (i : ι) (f g : ∀ i, π i) :
+    (Finset.univ.erase i).piecewise f g = Function.update f i (g i) := by
+  rw [← compl_singleton, piecewise_compl, piecewise_singleton]
+#align finset.piecewise_erase_univ Finset.piecewise_erase_univ
+
+end Fintype
+
+variable {π : ι → Type*} {t : Set ι} {t' : ∀ i, Set (π i)} {f g f' g' h : ∀ i, π i}
+
+lemma piecewise_mem_set_pi (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') :
+    s.piecewise f g ∈ Set.pi t t' := by
+  classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg
+#align finset.piecewise_mem_set_pi Finset.piecewise_mem_set_pi
+
+variable [∀ i, Preorder (π i)]
+
+lemma piecewise_le_of_le_of_le (hf : f ≤ h) (hg : g ≤ h) : s.piecewise f g ≤ h := fun x =>
+  piecewise_cases s f g (· ≤ h x) (hf x) (hg x)
+#align finset.piecewise_le_of_le_of_le Finset.piecewise_le_of_le_of_le
+
+lemma le_piecewise_of_le_of_le (hf : h ≤ f) (hg : h ≤ g) : h ≤ s.piecewise f g := fun x =>
+  piecewise_cases s f g (fun y => h x ≤ y) (hf x) (hg x)
+#align finset.le_piecewise_of_le_of_le Finset.le_piecewise_of_le_of_le
+
+lemma piecewise_le_piecewise' (hf : ∀ x ∈ s, f x ≤ f' x) (hg : ∀ x ∉ s, g x ≤ g' x) :
+    s.piecewise f g ≤ s.piecewise f' g' := fun x => by by_cases hx : x ∈ s <;> simp [hx, *]
+#align finset.piecewise_le_piecewise' Finset.piecewise_le_piecewise'
+
+lemma piecewise_le_piecewise (hf : f ≤ f') (hg : g ≤ g') : s.piecewise f g ≤ s.piecewise f' g' :=
+  s.piecewise_le_piecewise' (fun x _ => hf x) fun x _ => hg x
+#align finset.piecewise_le_piecewise Finset.piecewise_le_piecewise
+
+lemma piecewise_mem_Icc_of_mem_of_mem (hf : f ∈ Set.Icc f' g') (hg : g ∈ Set.Icc f' g') :
+    s.piecewise f g ∈ Set.Icc f' g' :=
+  ⟨le_piecewise_of_le_of_le _ hf.1 hg.1, piecewise_le_of_le_of_le _ hf.2 hg.2⟩
+#align finset.piecewise_mem_Icc_of_mem_of_mem Finset.piecewise_mem_Icc_of_mem_of_mem
+
+lemma piecewise_mem_Icc (h : f ≤ g) : s.piecewise f g ∈ Set.Icc f g :=
+  piecewise_mem_Icc_of_mem_of_mem _ (Set.left_mem_Icc.2 h) (Set.right_mem_Icc.2 h)
+#align finset.piecewise_mem_Icc Finset.piecewise_mem_Icc
+
+lemma piecewise_mem_Icc' (h : g ≤ f) : s.piecewise f g ∈ Set.Icc g f :=
+  piecewise_mem_Icc_of_mem_of_mem _ (Set.right_mem_Icc.2 h) (Set.left_mem_Icc.2 h)
+#align finset.piecewise_mem_Icc' Finset.piecewise_mem_Icc'
+
+end Finset
diff --git a/Mathlib/Data/Finset/Union.lean b/Mathlib/Data/Finset/Union.lean
new file mode 100644
index 0000000000000..1bc57a67df11d
--- /dev/null
+++ b/Mathlib/Data/Finset/Union.lean
@@ -0,0 +1,263 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Multiset.Bind
+import Mathlib.Order.SetNotation
+
+/-!
+# Unions of finite sets
+
+This file defines the union of a family `t : α → Finset β` of finsets bounded by a finset
+`s : Finset α`.
+
+## Main declarations
+
+* `Finset.disjUnion`: Given a hypothesis `h` which states that finsets `s` and `t` are disjoint,
+  `s.disjUnion t h` is the set such that `a ∈ disjUnion s t h` iff `a ∈ s` or `a ∈ t`; this does
+  not require decidable equality on the type `α`.
+* `Finset.biUnion`: Finite unions of finsets; given an indexing function `f : α → Finset β` and an
+  `s : Finset α`, `s.biUnion f` is the union of all finsets of the form `f a` for `a ∈ s`.
+
+## TODO
+
+Remove `Finset.biUnion` in favour of `Finset.sup`.
+-/
+
+variable {α β γ : Type*} {s s₁ s₂ : Finset α} {t t₁ t₂ : α → Finset β}
+
+namespace Finset
+section DisjiUnion
+
+/-- `disjiUnion s f h` is the set such that `a ∈ disjiUnion s f` iff `a ∈ f i` for some `i ∈ s`.
+It is the same as `s.biUnion f`, but it does not require decidable equality on the type. The
+hypothesis ensures that the sets are disjoint. -/
+def disjiUnion (s : Finset α) (t : α → Finset β) (hf : (s : Set α).PairwiseDisjoint t) : Finset β :=
+  ⟨s.val.bind (Finset.val ∘ t), Multiset.nodup_bind.2
+    ⟨fun a _ ↦ (t a).nodup, s.nodup.pairwise fun _ ha _ hb hab ↦ disjoint_val.2 <| hf ha hb hab⟩⟩
+#align finset.disj_Union Finset.disjUnionₓ -- Porting note: universes and more
+
+@[simp]
+lemma disjiUnion_val (s : Finset α) (t : α → Finset β) (h) :
+    (s.disjiUnion t h).1 = s.1.bind fun a ↦ (t a).1 := rfl
+#align finset.disj_Union_val Finset.disjiUnion_val
+
+@[simp] lemma disjiUnion_empty (t : α → Finset β) : disjiUnion ∅ t (by simp) = ∅ := rfl
+#align finset.disj_Union_empty Finset.disjiUnion_empty
+
+@[simp] lemma mem_disjiUnion {b : β} {h} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a := by
+  simp only [mem_def, disjiUnion_val, Multiset.mem_bind, exists_prop]
+#align finset.mem_disj_Union Finset.mem_disjiUnion
+
+@[simp, norm_cast]
+lemma coe_disjiUnion {h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x := by
+  simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
+#align finset.coe_disj_Union Finset.coe_disjiUnion
+
+@[simp] lemma disjiUnion_cons (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H) :
+    disjiUnion (cons a s ha) f H =
+    (f a).disjUnion ((s.disjiUnion f) fun _ hb _ hc ↦ H (mem_cons_of_mem hb) (mem_cons_of_mem hc))
+      (disjoint_left.2 fun _ hb h ↦
+        let ⟨_, hc, h⟩ := mem_disjiUnion.mp h
+        disjoint_left.mp
+          (H (mem_cons_self a s) (mem_cons_of_mem hc) (ne_of_mem_of_not_mem hc ha).symm) hb h) :=
+  eq_of_veq <| Multiset.cons_bind _ _ _
+#align finset.disj_Union_cons Finset.disjiUnion_cons
+
+@[simp] lemma singleton_disjiUnion (a : α) {h} : Finset.disjiUnion {a} t h = t a :=
+  eq_of_veq <| Multiset.singleton_bind _ _
+#align finset.singleton_disj_Union Finset.singleton_disjiUnion
+
+lemma disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 h2) :
+    (s.disjiUnion f h1).disjiUnion g h2 =
+      s.attach.disjiUnion
+        (fun a ↦ ((f a).disjiUnion g) fun b hb c hc ↦
+            h2 (mem_disjiUnion.mpr ⟨_, a.prop, hb⟩) (mem_disjiUnion.mpr ⟨_, a.prop, hc⟩))
+        fun a _ b _ hab ↦
+        disjoint_left.mpr fun x hxa hxb ↦ by
+          obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
+          obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
+          refine'
+            disjoint_left.mp
+              (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) _) hga
+              hgb
+          rintro rfl
+          exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb :=
+  eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm
+#align finset.disj_Union_disj_Union Finset.disjiUnion_disjiUnion
+
+lemma disjiUnion_filter_eq_of_maps_to [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
+    (h : ∀ x ∈ s, f x ∈ t) :
+    t.disjiUnion (fun a ↦ s.filter (fun c ↦ f c = a))
+      (fun x' hx y' hy hne ↦ by
+        simp_rw [disjoint_left, mem_filter]
+        rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
+        exact hne rfl) = s :=
+  ext fun b ↦ by simpa using h b
+#align finset.disj_Union_filter_eq_of_maps_to Finset.disjiUnion_filter_eq_of_maps_to
+
+end DisjiUnion
+
+section BUnion
+variable [DecidableEq β]
+
+/-- `Finset.biUnion s t` is the union of `t a` over `a ∈ s`.
+
+(This was formerly `bind` due to the monad structure on types with `DecidableEq`.) -/
+protected def biUnion (s : Finset α) (t : α → Finset β) : Finset β :=
+  (s.1.bind fun a ↦ (t a).1).toFinset
+#align finset.bUnion Finset.biUnion
+
+@[simp] lemma biUnion_val (s : Finset α) (t : α → Finset β) :
+    (s.biUnion t).1 = (s.1.bind fun a ↦ (t a).1).dedup := rfl
+#align finset.bUnion_val Finset.biUnion_val
+
+@[simp] lemma biUnion_empty : Finset.biUnion ∅ t = ∅ := rfl
+#align finset.bUnion_empty Finset.biUnion_empty
+
+@[simp] lemma mem_biUnion {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a := by
+  simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind, exists_prop]
+#align finset.mem_bUnion Finset.mem_biUnion
+
+@[simp, norm_cast]
+lemma coe_biUnion : (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x := by
+  simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
+#align finset.coe_bUnion Finset.coe_biUnion
+
+@[simp]
+lemma biUnion_insert [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t :=
+  ext fun x ↦ by
+    simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or,
+      exists_eq_left]
+#align finset.bUnion_insert Finset.biUnion_insert
+
+lemma biUnion_congr (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂ :=
+  ext fun x ↦ by
+    -- Porting note: this entire proof was `simp [or_and_distrib_right, exists_or_distrib]`
+    simp_rw [mem_biUnion]
+    apply exists_congr
+    simp (config := { contextual := true }) only [hs, and_congr_right_iff, ht, implies_true]
+#align finset.bUnion_congr Finset.biUnion_congr
+
+@[simp]
+lemma disjiUnion_eq_biUnion (s : Finset α) (f : α → Finset β) (hf) :
+    s.disjiUnion f hf = s.biUnion f := eq_of_veq (s.disjiUnion f hf).nodup.dedup.symm
+#align finset.disj_Union_eq_bUnion Finset.disjiUnion_eq_biUnion
+
+lemma biUnion_subset {s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s' := by
+  simp only [subset_iff, mem_biUnion]
+  exact ⟨fun H a ha b hb ↦ H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ ↦ H a ha hb⟩
+#align finset.bUnion_subset Finset.biUnion_subset
+
+@[simp]
+lemma singleton_biUnion {a : α} : Finset.biUnion {a} t = t a := by
+  classical rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]
+#align finset.singleton_bUnion Finset.singleton_biUnion
+
+lemma biUnion_inter (s : Finset α) (f : α → Finset β) (t : Finset β) :
+    s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t := by
+  ext x
+  simp only [mem_biUnion, mem_inter]
+  tauto
+#align finset.bUnion_inter Finset.biUnion_inter
+
+lemma inter_biUnion (t : Finset β) (s : Finset α) (f : α → Finset β) :
+    t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x := by
+  rw [inter_comm, biUnion_inter]
+  simp [inter_comm]
+#align finset.inter_bUnion Finset.inter_biUnion
+
+lemma biUnion_biUnion [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
+    (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g := by
+  ext
+  simp only [Finset.mem_biUnion, exists_prop]
+  simp_rw [← exists_and_right, ← exists_and_left, and_assoc]
+  rw [exists_comm]
+#align finset.bUnion_bUnion Finset.biUnion_biUnion
+
+lemma bind_toFinset [DecidableEq α] (s : Multiset α) (t : α → Multiset β) :
+    (s.bind t).toFinset = s.toFinset.biUnion fun a ↦ (t a).toFinset :=
+  ext fun x ↦ by simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]
+#align finset.bind_to_finset Finset.bind_toFinset
+
+lemma biUnion_mono (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂ := by
+  have : ∀ b a, a ∈ s → b ∈ t₁ a → ∃ a : α, a ∈ s ∧ b ∈ t₂ a := fun b a ha hb ↦
+    ⟨a, ha, Finset.mem_of_subset (h a ha) hb⟩
+  simpa only [subset_iff, mem_biUnion, exists_imp, and_imp, exists_prop]
+#align finset.bUnion_mono Finset.biUnion_mono
+
+lemma biUnion_subset_biUnion_of_subset_left (t : α → Finset β) (h : s₁ ⊆ s₂) :
+    s₁.biUnion t ⊆ s₂.biUnion t := fun x ↦ by
+  simp only [and_imp, mem_biUnion, exists_prop]; exact Exists.imp fun a ha ↦ ⟨h ha.1, ha.2⟩
+#align finset.bUnion_subset_bUnion_of_subset_left Finset.biUnion_subset_biUnion_of_subset_left
+
+lemma subset_biUnion_of_mem (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u :=
+  singleton_biUnion.superset.trans <|
+    biUnion_subset_biUnion_of_subset_left u <| singleton_subset_iff.2 xs
+#align finset.subset_bUnion_of_mem Finset.subset_biUnion_of_mem
+
+@[simp]
+lemma biUnion_subset_iff_forall_subset {α β : Type*} [DecidableEq β] {s : Finset α}
+    {t : Finset β} {f : α → Finset β} : s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t :=
+  ⟨fun h _ hx ↦ (subset_biUnion_of_mem f hx).trans h, fun h _ hx ↦
+    let ⟨_, ha₁, ha₂⟩ := mem_biUnion.mp hx
+    h _ ha₁ ha₂⟩
+#align finset.bUnion_subset_iff_forall_subset Finset.biUnion_subset_iff_forall_subset
+
+@[simp]
+lemma biUnion_singleton_eq_self [DecidableEq α] : s.biUnion (singleton : α → Finset α) = s :=
+  ext fun x ↦ by simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']
+#align finset.bUnion_singleton_eq_self Finset.biUnion_singleton_eq_self
+
+lemma filter_biUnion (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] :
+    (s.biUnion f).filter p = s.biUnion fun a ↦ (f a).filter p := by
+  ext b
+  simp only [mem_biUnion, exists_prop, mem_filter]
+  constructor
+  · rintro ⟨⟨a, ha, hba⟩, hb⟩
+    exact ⟨a, ha, hba, hb⟩
+  · rintro ⟨a, ha, hba, hb⟩
+    exact ⟨⟨a, ha, hba⟩, hb⟩
+#align finset.filter_bUnion Finset.filter_biUnion
+
+lemma biUnion_filter_eq_of_maps_to [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β}
+    (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun a ↦ s.filter fun c ↦ f c = a) = s := by
+  simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h
+#align finset.bUnion_filter_eq_of_maps_to Finset.biUnion_filter_eq_of_maps_to
+
+lemma erase_biUnion (f : α → Finset β) (s : Finset α) (b : β) :
+    (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b := by
+  ext a
+  simp only [mem_biUnion, not_exists, not_and, mem_erase, ne_eq]
+  tauto
+#align finset.erase_bUnion Finset.erase_biUnion
+
+@[simp]
+lemma biUnion_nonempty : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty := by
+  simp only [Finset.Nonempty, mem_biUnion]
+  rw [exists_swap]
+  simp [exists_and_left]
+#align finset.bUnion_nonempty Finset.biUnion_nonempty
+
+lemma Nonempty.biUnion (hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) :
+    (s.biUnion t).Nonempty := biUnion_nonempty.2 <| hs.imp fun x hx ↦ ⟨hx, ht x hx⟩
+#align finset.nonempty.bUnion Finset.Nonempty.biUnion
+
+lemma disjoint_biUnion_left (s : Finset α) (f : α → Finset β) (t : Finset β) :
+    Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t := by
+  classical
+  refine s.induction ?_ ?_
+  · simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
+  · intro i s his ih
+    simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]
+#align finset.disjoint_bUnion_left Finset.disjoint_biUnion_left
+
+lemma disjoint_biUnion_right (s : Finset β) (t : Finset α) (f : α → Finset β) :
+    Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i) := by
+  simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s
+#align finset.disjoint_bUnion_right Finset.disjoint_biUnion_right
+
+end BUnion
+end Finset
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index 942a6b83a6e1f..090d2e57de533 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -302,26 +302,6 @@ theorem map_univ_equiv [Fintype β] (f : β ≃ α) : univ.map f.toEmbedding = u
   map_univ_of_surjective f.surjective
 #align finset.map_univ_equiv Finset.map_univ_equiv
 
-@[simp]
-theorem piecewise_univ [∀ i : α, Decidable (i ∈ (univ : Finset α))] {δ : α → Sort*}
-    (f g : ∀ i, δ i) : univ.piecewise f g = f := by
-  ext i
-  simp [piecewise]
-#align finset.piecewise_univ Finset.piecewise_univ
-
-theorem piecewise_compl [DecidableEq α] (s : Finset α) [∀ i : α, Decidable (i ∈ s)]
-    [∀ i : α, Decidable (i ∈ sᶜ)] {δ : α → Sort*} (f g : ∀ i, δ i) :
-    sᶜ.piecewise f g = s.piecewise g f := by
-  ext i
-  simp [piecewise]
-#align finset.piecewise_compl Finset.piecewise_compl
-
-@[simp]
-theorem piecewise_erase_univ {δ : α → Sort*} [DecidableEq α] (a : α) (f g : ∀ a, δ a) :
-    (Finset.univ.erase a).piecewise f g = Function.update f a (g a) := by
-  rw [← compl_singleton, piecewise_compl, piecewise_singleton]
-#align finset.piecewise_erase_univ Finset.piecewise_erase_univ
-
 theorem univ_map_equiv_to_embedding {α β : Type*} [Fintype α] [Fintype β] (e : α ≃ β) :
     univ.map e.toEmbedding = univ :=
   eq_univ_iff_forall.mpr fun b => mem_map.mpr ⟨e.symm b, mem_univ _, by simp⟩
diff --git a/Mathlib/Data/Set/Constructions.lean b/Mathlib/Data/Set/Constructions.lean
index ee86cddb7909c..f3bb99c3d9c97 100644
--- a/Mathlib/Data/Set/Constructions.lean
+++ b/Mathlib/Data/Set/Constructions.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Set.Lattice
 
 #align_import data.set.constructions from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
 
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 2731b3b0d6ea4..ec986403f3409 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 -/
 import Mathlib.Data.Finset.Basic
-import Mathlib.Data.Set.Functor
 import Mathlib.Data.Finite.Basic
+import Mathlib.Data.Set.Functor
+import Mathlib.Data.Set.Lattice
 
 #align_import data.set.finite from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 
@@ -1753,3 +1754,27 @@ lemma Set.finite_diff_iUnion_Ioo (s : Set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Io
 lemma Set.finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite := by
   simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo
 #align set.finite_diff_Union_Ioo' Set.finite_diff_iUnion_Ioo'
+
+lemma Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι]
+    {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
+    ∃ i, (s : Set α) ⊆ f i := by
+  classical
+  revert hs
+  refine s.induction_on ?_ ?_
+  · simp
+  intro b t _hbt htc hbtc
+  obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
+  obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
+  rcases h j i with ⟨k, hk, hk'⟩
+  use k
+  rw [Finset.coe_insert, Set.insert_subset_iff]
+  exact ⟨hk hbj, _root_.trans hti hk'⟩
+#align directed.exists_mem_subset_of_finset_subset_bUnion Directed.exists_mem_subset_of_finset_subset_biUnion
+
+theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α}
+    {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α}
+    (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : Set α) ⊆ f i := by
+  rw [Set.biUnion_eq_iUnion] at hs
+  haveI := hn.coe_sort
+  simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs
+#align directed_on.exists_mem_subset_of_finset_subset_bUnion DirectedOn.exists_mem_subset_of_finset_subset_biUnion