-- Mathlib/Data/Fintype/EquivFin.lean
theorem exists_superset_card_eq [Infinite α] (s : Finset α) (n : ℕ) (hn : #s ≤ n) :
    ∃ t : Finset α, s ⊆ t ∧ #t = n

Proof state:
case succ.inl
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s = n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
exact ⟨s, subset_refl _, hn'⟩

Result:
no goals

Proof state:
case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')

Result:
case succ.inr.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Proof state:
case succ.inr.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨x, hx⟩ := exists_not_mem_finset t

Result:
case succ.inr.intro.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Proof state:
case zero
α : Type u_1
inst✝ : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ t, s ⊆ t ∧ #t = 0

Tactic:
exact ⟨s, subset_refl _, Nat.eq_zero_of_le_zero hn⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
rcases hn.eq_or_lt with hn' | hn'

Result:
case succ.inl
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s = n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Proof state:
case succ.inr.intro.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ #(cons x t hx) = n + 1

Tactic:
simp [hx, ht]

Result:
no goals

Proof state:
case succ.inr.intro.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩

Result:
case succ.inr.intro.intro.intro
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ #(cons x t hx) = n + 1

Proof state:
α : Type u_1
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
induction' n with n IH generalizing s

Result:
case zero
α : Type u_1
inst✝ : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ t, s ⊆ t ∧ #t = 0

case succ
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1