-- Mathlib/Data/Finset/Card.lean
/-- 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 ≤ n) (hnt : n ≤ #t) :
    ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Proof state:
case intro
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u ∧ a ∉ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
exact ⟨u.erase a, by simp [subset_erase, erase_subset_iff_of_mem (hu₂ _), *]⟩

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u ∧ a ∉ s
⊢ s ⊆ u.erase a ∧ u.erase a ⊆ t ∧ #(u.erase a) = k

Tactic:
simp [subset_erase, erase_subset_iff_of_mem (hu₂ _), *]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ 0 < #u - #s

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩

Result:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∀ k < #t, n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∀ k < #t, n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩

Result:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
obtain ⟨a, ha⟩ : (u \ s).Nonempty := by rw [← card_pos, card_sdiff hu₁]; omega

Result:
case intro
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
classical
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
obtain ⟨a, ha⟩ : (u \ s).Nonempty := by rw [← card_pos, card_sdiff hu₁]; omega
simp only [mem_sdiff] at ha
exact ⟨u.erase a, by simp [subset_erase, erase_subset_iff_of_mem (hu₂ _), *]⟩

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ s ⊆ t ∧ t ⊆ t ∧ #t = #t

Tactic:
simp [hst]

Result:
no goals

Proof state:
case intro
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
simp only [mem_sdiff] at ha

Result:
case intro
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u ∧ a ∉ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Proof state:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ (u \ s).Nonempty

Tactic:
rw [← card_pos, card_sdiff hu₁]

Result:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ 0 < #u - #s