α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ Finset.card { val := a ::ₘ (toFinset s).val, nodup := (_ : Multiset.Nodup (a ::ₘ (toFinset s).val)) } =
    Fintype.card ↑s + 1
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
rw [fintypeInsertOfNotMem, Fintype.card_ofFinset]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ ↑Multiset.card Finset.univ.val = Fintype.card ↑s
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ Finset.card { val := a ::ₘ (toFinset s).val, nodup := (_ : Multiset.Nodup (a ::ₘ (toFinset s).val)) } =
    Fintype.card ↑s + 1
simp only [Finset.card, toFinset, Finset.map_val, Embedding.coe_subtype,
           Multiset.card_cons, Multiset.card_map, add_left_inj]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ ↑Multiset.card Finset.univ.val = Fintype.card ↑s
rfl