case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Fintype ↑∅
⊢ h = fintypeEmpty
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Fintype ↑∅
⊢ Fintype.card ↑∅ = Fintype.card ↑∅
congr
no goals
case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Fintype ↑∅
⊢ h = fintypeEmpty
exact Subsingleton.elim _ _