α : Type u_1
β : Type ?u.9267
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
α : Type u_1
β : Type ?u.9267
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1
letI := Fintype.ofSubsingleton a
no goals
α : Type u_1
β : Type ?u.9267
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]