α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
rw [← card_fintypeInsertOfNotMem s h]
case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ d = fintypeInsertOfNotMem s h
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
congr
no goals
case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ d = fintypeInsertOfNotMem s h
exact Subsingleton.elim _ _