diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
index 96fa2df2357f59..72e49f5ece1132 100644
--- a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
+++ b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
@@ -380,7 +380,7 @@ theorem mulRothNumber_lt_of_forall_not_threeGPFree
   obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
   rw [← hcard, ← not_le]
   intro hn
-  obtain ⟨u, hut, rfl⟩ := exists_smaller_set t n hn
+  obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn
   exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)
 #align mul_roth_number_lt_of_forall_not_mul_salem_spencer mulRothNumber_lt_of_forall_not_threeGPFree
 #align add_roth_number_lt_of_forall_not_add_salem_spencer addRothNumber_lt_of_forall_not_threeAPFree
diff --git a/Mathlib/Combinatorics/SetFamily/Shadow.lean b/Mathlib/Combinatorics/SetFamily/Shadow.lean
index ad50d790c35f41..a5573ad0dd0399 100644
--- a/Mathlib/Combinatorics/SetFamily/Shadow.lean
+++ b/Mathlib/Combinatorics/SetFamily/Shadow.lean
@@ -310,13 +310,8 @@ theorem mem_upShadow_iff_exists_mem_card_add :
     rw [← hcardst, hcardtu, add_right_comm]
     rfl
   · rintro ⟨t, ht, hts, hcard⟩
-    obtain ⟨u, htu, hus, hu⟩ :=
-      Finset.exists_intermediate_set 1
-        (by
-          rw [add_comm, ← hcard]
-          exact add_le_add_left (succ_le_of_lt (zero_lt_succ _)) _)
-        hts
-    rw [add_comm] at hu
+    obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1)
+      (by omega)
     refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
     rw [hu, ← hcard, add_right_comm]
     rfl
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index ef1a5fb0924f68..c2c62a508ab617 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -351,7 +351,7 @@ theorem cliqueFree_bot (h : 2 ≤ n) : (⊥ : SimpleGraph α).CliqueFree n := by
 
 theorem CliqueFree.mono (h : m ≤ n) : G.CliqueFree m → G.CliqueFree n := by
   intro hG s hs
-  obtain ⟨t, hts, ht⟩ := s.exists_smaller_set _ (h.trans hs.card_eq.ge)
+  obtain ⟨t, hts, ht⟩ := exists_subset_card_eq (h.trans hs.card_eq.ge)
   exact hG _ ⟨hs.clique.subset hts, ht⟩
 #align simple_graph.clique_free.mono SimpleGraph.CliqueFree.mono
 
@@ -469,7 +469,7 @@ theorem CliqueFreeOn.subset (hs : s₁ ⊆ s₂) (h₂ : G.CliqueFreeOn s₂ n)
 
 theorem CliqueFreeOn.mono (hmn : m ≤ n) (hG : G.CliqueFreeOn s m) : G.CliqueFreeOn s n := by
   rintro t hts ht
-  obtain ⟨u, hut, hu⟩ := t.exists_smaller_set _ (hmn.trans ht.card_eq.ge)
+  obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)
   exact hG ((coe_subset.2 hut).trans hts) ⟨ht.clique.subset hut, hu⟩
 #align simple_graph.clique_free_on.mono SimpleGraph.CliqueFreeOn.mono
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
index 034e2d8edc5aea..79edb953a76e19 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
@@ -80,7 +80,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
     of `u` of size `n`). The rest of each branch is just tedious calculations to satisfy the
     induction hypothesis. -/
   by_cases h : ∀ u ∈ P.parts, card u < m + 1
-  · obtain ⟨t, hts, htn⟩ := exists_smaller_set s n (hn₂.trans_eq hs)
+  · obtain ⟨t, hts, htn⟩ := exists_subset_card_eq (hn₂.trans_eq hs)
     have ht : t.Nonempty := by rwa [← card_pos, htn]
     have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card := by
       rw [card_sdiff ‹t ⊆ s›, htn, hn₃]
@@ -99,7 +99,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
     · intro H; exact ht.ne_empty (le_sdiff_iff.1 <| R.le <| filter_subset _ _ H)
   push_neg at h
   obtain ⟨u, hu₁, hu₂⟩ := h
-  obtain ⟨t, htu, htn⟩ := exists_smaller_set _ _ (hn₁.trans hu₂)
+  obtain ⟨t, htu, htn⟩ := exists_subset_card_eq (hn₁.trans hu₂)
   have ht : t.Nonempty := by rwa [← card_pos, htn]
   have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card := by
     rw [card_sdiff (htu.trans <| P.le hu₁), htn, hn₃]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Turan.lean b/Mathlib/Combinatorics/SimpleGraph/Turan.lean
index 339d7f6030974e..9fe9759ac80c9a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Turan.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Turan.lean
@@ -104,7 +104,7 @@ if it can accommodate such a clique. -/
 theorem not_cliqueFree_of_isTuranMaximal (hn : r ≤ Fintype.card V) (hG : G.IsTuranMaximal r) :
     ¬G.CliqueFree r := by
   rintro h
-  obtain ⟨K, _, rfl⟩ := exists_smaller_set (univ : Finset V) r hn
+  obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn
   obtain ⟨a, -, b, -, hab, hGab⟩ : ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬ G.Adj a b := by
     simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
       exists_prop, exists_and_right] using h K
diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
index 2e46aa8fcf9f80..272dea575e9af4 100644
--- a/Mathlib/Data/Finset/Card.lean
+++ b/Mathlib/Data/Finset/Card.lean
@@ -618,39 +618,42 @@ theorem filter_card_add_filter_neg_card_eq_card
   rw [← card_union_of_disjoint (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
 #align finset.filter_card_add_filter_neg_card_eq_card Finset.filter_card_add_filter_neg_card_eq_card
 
+/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
+set `u` of size `n` which is both a superset of `s` and a subset of `t`. -/
+lemma exists_subsuperset_card_eq (hst : s ⊆ t) (hsn : s.card ≤ n) (hnt : n ≤ t.card) :
+    ∃ u, s ⊆ u ∧ u ⊆ t ∧ card u = n := by
+  classical
+  obtain ⟨k, hk⟩ := Nat.le.dest hnt
+  clear hnt
+  induction' k with k ih generalizing t
+  · exact ⟨t, hst, Subset.rfl, hk.symm⟩
+  obtain ⟨a, ha⟩ : (t \ s).Nonempty := by rw [← card_pos, card_sdiff hst]; omega
+  replace hst : s ⊆ t.erase a := subset_erase.2 ⟨hst, (mem_sdiff.1 ha).2⟩
+  replace hk : n + k = card (erase t a) := by rw [card_erase_of_mem (mem_sdiff.1 ha).1]; omega
+  obtain ⟨u, hsu, hut, hu⟩ := ih hst hk
+  exact ⟨u, hsu, hut.trans (erase_subset ..), hu⟩
+
+/-- We can shrink a set `s` to any smaller size. -/
+lemma exists_subset_card_eq (hns : n ≤ s.card) : ∃ t ⊆ s, t.card = n := by
+  simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns
+
 /-- Given a set `A` and a set `B` inside it, we can shrink `A` to any appropriate size, and keep `B`
 inside it. -/
+@[deprecated exists_subsuperset_card_eq (since := "2024-06-23")]
 theorem exists_intermediate_set {A B : Finset α} (i : ℕ) (h₁ : i + card B ≤ card A) (h₂ : B ⊆ A) :
-    ∃ C : Finset α, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B := by
-  classical
-    rcases Nat.le.dest h₁ with ⟨k, h⟩
-    clear h₁
-    induction' k with k ih generalizing A
-    · exact ⟨A, h₂, Subset.refl _, h.symm⟩
-    obtain ⟨a, ha⟩ : (A \ B).Nonempty := by rw [← card_pos, card_sdiff h₂]; omega
-    have z : i + card B + k = card (erase A a) := by
-      rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h,
-        Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ← pred_eq_sub_one,
-        k.pred_succ]
-    have : B ⊆ A.erase a := by
-      rintro t th
-      apply mem_erase_of_ne_of_mem _ (h₂ th)
-      rintro rfl
-      exact not_mem_sdiff_of_mem_right th ha
-    rcases ih this z with ⟨B', hB', B'subA', cards⟩
-    exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
+    ∃ C : Finset α, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B :=
+  exists_subsuperset_card_eq h₂ (Nat.le_add_left ..) h₁
 #align finset.exists_intermediate_set Finset.exists_intermediate_set
 
 /-- We can shrink `A` to any smaller size. -/
+@[deprecated exists_subset_card_eq (since := "2024-06-23")]
 theorem exists_smaller_set (A : Finset α) (i : ℕ) (h₁ : i ≤ card A) :
-    ∃ B : Finset α, B ⊆ A ∧ card B = i :=
-  let ⟨B, _, x₁, x₂⟩ := exists_intermediate_set i (by simpa) (empty_subset A)
-  ⟨B, x₁, x₂⟩
+    ∃ B : Finset α, B ⊆ A ∧ card B = i := exists_subset_card_eq h₁
 #align finset.exists_smaller_set Finset.exists_smaller_set
 
 theorem le_card_iff_exists_subset_card : n ≤ s.card ↔ ∃ t ⊆ s, t.card = n := by
   refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩
-  exact exists_smaller_set s n h
+  exact exists_subset_card_eq h
 
 theorem exists_subset_or_subset_of_two_mul_lt_card [DecidableEq α] {X Y : Finset α} {n : ℕ}
     (hXY : 2 * n < (X ∪ Y).card) : ∃ C : Finset α, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y) := by
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
index 9a5582a7f7308f..a1af66ff88191f 100644
--- a/Mathlib/Data/Finset/Powerset.lean
+++ b/Mathlib/Data/Finset/Powerset.lean
@@ -243,7 +243,7 @@ theorem powersetCard_one (s : Finset α) :
 lemma powersetCard_eq_empty : powersetCard n s = ∅ ↔ s.card < n := by
   refine ⟨?_, fun h ↦ card_eq_zero.1 $ by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
   contrapose!
-  exact fun h ↦ nonempty_iff_ne_empty.1 $ (exists_smaller_set _ _ h).imp $ by simp
+  exact fun h ↦ nonempty_iff_ne_empty.1 $ (exists_subset_card_eq h).imp $ by simp
 #align finset.powerset_len_empty Finset.powersetCard_eq_empty
 
 @[simp] lemma powersetCard_card_add (s : Finset α) (hn : 0 < n) :
@@ -272,7 +272,7 @@ theorem powersetCard_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h :
 
 @[simp, aesop safe apply (rule_sets := [finsetNonempty])]
 lemma powersetCard_nonempty : (powersetCard n s).Nonempty ↔ n ≤ s.card := by
-  aesop (add simp [Finset.Nonempty, exists_smaller_set, card_le_card])
+  aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])
 #align finset.powerset_len_nonempty Finset.powersetCard_nonempty
 
 @[simp]
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index 81bcfd6099af14..aba1128bfc9361 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -781,6 +781,11 @@ noncomputable def Finset.equivOfCardEq {s : Finset α} {t : Finset β} (h : s.ca
 theorem Finset.card_eq_of_equiv {s : Finset α} {t : Finset β} (i : s ≃ t) : s.card = t.card :=
   (card_eq_of_equiv_fintype i).trans (Fintype.card_coe _)
 
+/-- We can shrink a set `s` to any smaller size. -/
+lemma Finset.exists_superset_card_eq [Fintype α] {n : ℕ} {s : Finset α} (hsn : s.card ≤ n)
+    (hnα : n ≤ Fintype.card α) :
+    ∃ t, s ⊆ t ∧ t.card = n := by simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα
+
 @[simp]
 theorem Fintype.card_prop : Fintype.card Prop = 2 :=
   rfl
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 15c3b812ff646c..7ea1e3f559597b 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -521,7 +521,7 @@ theorem ncard_mono [Finite α] : @Monotone (Set α) _ _ _ ncard := fun _ _ ↦ n
   rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
 #align set.ncard_eq_zero Set.ncard_eq_zero
 
-@[simp] theorem ncard_coe_Finset (s : Finset α) : (s : Set α).ncard = s.card := by
+@[simp, norm_cast] theorem ncard_coe_Finset (s : Finset α) : (s : Set α).ncard = s.card := by
   rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]
 #align set.ncard_coe_finset Set.ncard_coe_Finset
 
@@ -938,35 +938,40 @@ theorem ncard_add_ncard_compl (s : Set α) (hs : s.Finite := by toFinite_tac)
 
 end Lattice
 
+/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
+set `u` of size `n` which is both a superset of `s` and a subset of `t`. -/
+lemma exists_subsuperset_card_eq {n : ℕ} (hst : s ⊆ t) (hsn : s.ncard ≤ n) (hnt : n ≤ t.ncard) :
+    ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n := by
+  obtain ht | ht := t.infinite_or_finite
+  · rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt
+    exact ⟨t, hst, Subset.rfl, hnt.symm⟩
+  lift s to Finset α using ht.subset hst
+  lift t to Finset α using ht
+  obtain ⟨u, hsu, hut, hu⟩ := Finset.exists_subsuperset_card_eq (mod_cast hst) (by simpa using hsn)
+    (mod_cast hnt)
+  exact ⟨u, mod_cast hsu, mod_cast hut, mod_cast hu⟩
+
+/-- We can shrink a set `s` to any smaller size. -/
+lemma exists_subset_card_eq {n : ℕ} (hns : n ≤ s.ncard) : ∃ t ⊆ s, t.ncard = n := by
+  simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns
+
 /-- Given a set `t` and a set `s` inside it, we can shrink `t` to any appropriate size, and keep `s`
     inside it. -/
+@[deprecated exists_subsuperset_card_eq (since := "2024-06-24")]
 theorem exists_intermediate_Set (i : ℕ) (h₁ : i + s.ncard ≤ t.ncard) (h₂ : s ⊆ t) :
-    ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = i + s.ncard := by
-  cases' t.finite_or_infinite with ht ht
-  · rw [ncard_eq_toFinset_card _ (ht.subset h₂)] at h₁ ⊢
-    rw [ncard_eq_toFinset_card t ht] at h₁
-    obtain ⟨r', hsr', hr't, hr'⟩ := Finset.exists_intermediate_set _ h₁ (by simpa)
-    exact ⟨r', by simpa using hsr', by simpa using hr't, by rw [← hr', ncard_coe_Finset]⟩
-  rw [ht.ncard] at h₁
-  have h₁' := Nat.eq_zero_of_le_zero h₁
-  rw [add_eq_zero_iff] at h₁'
-  refine ⟨t, h₂, rfl.subset, ?_⟩
-  rw [h₁'.2, h₁'.1, ht.ncard, add_zero]
+    ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = i + s.ncard :=
+  exists_subsuperset_card_eq h₂ (Nat.le_add_left ..) h₁
 #align set.exists_intermediate_set Set.exists_intermediate_Set
 
+@[deprecated exists_subsuperset_card_eq (since := "2024-06-24")]
 theorem exists_intermediate_set' {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.ncard) (h : s ⊆ t) :
-    ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = m := by
-  obtain ⟨r, hsr, hrt, hc⟩ :=
-    exists_intermediate_Set (m - s.ncard) (by rwa [tsub_add_cancel_of_le hs]) h
-  rw [tsub_add_cancel_of_le hs] at hc
-  exact ⟨r, hsr, hrt, hc⟩
+    ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = m := exists_subsuperset_card_eq h hs ht
 #align set.exists_intermediate_set' Set.exists_intermediate_set'
 
 /-- We can shrink `s` to any smaller size. -/
+@[deprecated exists_subset_card_eq (since := "2024-06-23")]
 theorem exists_smaller_set (s : Set α) (i : ℕ) (h₁ : i ≤ s.ncard) :
-    ∃ t : Set α, t ⊆ s ∧ t.ncard = i :=
-  (exists_intermediate_Set i (by simpa) (empty_subset s)).imp fun t ht ↦
-    ⟨ht.2.1, by simpa using ht.2.2⟩
+    ∃ t : Set α, t ⊆ s ∧ t.ncard = i := exists_subset_card_eq h₁
 #align set.exists_smaller_set Set.exists_smaller_set
 
 theorem Infinite.exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ) :