α : Type u_1
β : Type ?u.2024
γ : Type ?u.2027
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1
α : Type u_1
β : Type ?u.2024
γ : Type ?u.2027
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.2024
γ : Type ?u.2027
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1
simp only [Nat.card_eq_fintype_card, Fintype.card_option]