case inl
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Finite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0

case inr
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Infinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
cases finite_or_infinite α
case inl
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
case inl
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Finite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
letI := Fintype.ofFinite α
no goals
case inl
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
simp only [*, Nat.card_eq_fintype_card, dif_pos]
no goals
case inr
α✝ : Type ?u.215
β : Type ?u.218
γ : Type ?u.221
α : Type u_1
h✝ : Infinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]