case mk
α : Type u_1
β : Type ?u.46876
t : Finset α
f : α → β
n : ℕ
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ card { val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}
α : Type u_1
β : Type ?u.46876
s t : Finset α
f : α → β
n : ℕ
⊢ card s = 1 ↔ ∃ a, s = {a}
cases s
no goals
case mk
α : Type u_1
β : Type ?u.46876
t : Finset α
f : α → β
n : ℕ
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ card { val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]