case zero
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n : ℕ
hn✝ : card s✝ ≤ n
s : Finset α
hn : card s ≤ zero
⊢ ∃ t, s ⊆ t ∧ card t = zero

case succ
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : card s ≤ n
⊢ ∃ t, s ⊆ t ∧ card t = n
induction' n with n IH generalizing s
no goals
case zero
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n : ℕ
hn✝ : card s✝ ≤ n
s : Finset α
hn : card s ≤ zero
⊢ ∃ t, s ⊆ t ∧ card t = zero
exact ⟨s, subset_refl _, Nat.eq_zero_of_le_zero hn⟩
case succ.inl
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s = succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n

case succ.inr
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
case succ
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
cases' hn.eq_or_lt with hn' hn'
case succ.inr.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
case succ.inr
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
case succ.inr.intro.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ ∃ t, s ⊆ t ∧ card t = succ n
case succ.inr.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
obtain ⟨x, hx⟩ := exists_not_mem_finset t
case succ.inr.intro.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ card (cons x t hx) = succ n
case succ.inr.intro.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ ∃ t, s ⊆ t ∧ card t = succ n
refine' ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), _⟩
no goals
case succ.inr.intro.intro.intro
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ card (cons x t hx) = succ n
simp [hx, ht]
no goals
case succ.inl
α : Type u_1
β : Type ?u.80843
γ : Type ?u.80846
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s = succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
exact ⟨s, subset_refl _, hn'⟩