English
If s ⊆ t, and n is between |s| and |t|, then there exists a finite set u with s ⊆ u ⊆ t and |u| = n.
Русский
Пусть s ⊆ t и n лежит между |s| и |t|. Тогда существует множество u such that s ⊆ u ⊆ t и |u| = n.
LaTeX
$$$s \\subseteq t \\Rightarrow |s| \\le n \\Rightarrow n \\le |t| \\Rightarrow \\exists u, s \\subseteq u \\land u \\subseteq t \\land |u| = n$$$
Lean4
/-- 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`. -/
theorem exists_subsuperset_card_eq (hst : s ⊆ t) (hsn : #s ≤ n) (hnt : n ≤ #t) : ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n := by
classical
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
exact ⟨u.erase a, by grind⟩
