case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (#↑s) = ↑n → ∃ t, ↑t = s ∧ Finset.card t = n

case mpr
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ Finset.card t = n) → (#↑s) = ↑n
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (#↑s) = ↑n ↔ ∃ t, ↑t = s ∧ Finset.card t = n
constructor
case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
h : (#↑s) = ↑n
⊢ ∃ t, ↑t = s ∧ Finset.card t = n
case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (#↑s) = ↑n → ∃ t, ↑t = s ∧ Finset.card t = n
intro h
case mp.intro
α✝ β : Type u
α : Type u_1
n : ℕ
s : Finset α
h : (#↑↑s) = ↑n
⊢ ∃ t, ↑t = ↑s ∧ Finset.card t = n
case mp
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
h : (#↑s) = ↑n
⊢ ∃ t, ↑t = s ∧ Finset.card t = n
lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ nat_lt_aleph0 n)
no goals
case mp.intro
α✝ β : Type u
α : Type u_1
n : ℕ
s : Finset α
h : (#↑↑s) = ↑n
⊢ ∃ t, ↑t = ↑s ∧ Finset.card t = n
simpa using h
case mpr.intro.intro
α✝ β : Type u
α : Type u_1
t : Finset α
⊢ (#↑↑t) = ↑(Finset.card t)
case mpr
α✝ β : Type u
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ Finset.card t = n) → (#↑s) = ↑n
rintro ⟨t, rfl, rfl⟩
no goals
case mpr.intro.intro
α✝ β : Type u
α : Type u_1
t : Finset α
⊢ (#↑↑t) = ↑(Finset.card t)
exact mk_coe_finset