α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) ↔ ∃ h, Fintype.card α = n
α β : Type u
n : ℕ
⊢ (#α) = ↑n ↔ ∃ h, Fintype.card α = n
rw [mk_eq_nat_iff_finset]
case mp
α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) → ∃ h, Fintype.card α = n

case mpr
α β : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ Finset.card t = n
α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) ↔ ∃ h, Fintype.card α = n
constructor
case mp.intro.intro
α β : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : Finset.card t = n
⊢ ∃ h, Fintype.card α = n
case mp
α β : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ Finset.card t = n) → ∃ h, Fintype.card α = n
rintro ⟨t, ht, hn⟩
no goals
case mp.intro.intro
α β : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : Finset.card t = n
⊢ ∃ h, Fintype.card α = n
exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩
case mpr.intro.mk
α β : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ Finset.card t = n
case mpr
α β : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ Finset.card t = n
rintro ⟨⟨t, ht⟩, hn⟩
no goals
case mpr.intro.mk
α β : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ Finset.card t = n
exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩