case inl
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Finite α
⊢ ncard univ = Nat.card α

case inr
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Infinite α
⊢ ncard univ = Nat.card α
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
⊢ ncard univ = Nat.card α
cases' finite_or_infinite α with h h
case inr
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Infinite α
⊢ Set.Infinite univ
case inr
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Infinite α
⊢ ncard univ = Nat.card α
rw [Nat.card_eq_zero_of_infinite, Infinite.ncard]
no goals
case inr
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Infinite α
⊢ Set.Infinite univ
exact infinite_univ
case inl
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Finite α
hft : Fintype α
⊢ ncard univ = Nat.card α
case inl
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Finite α
⊢ ncard univ = Nat.card α
have hft := Fintype.ofFinite α
no goals
case inl
α✝ : Type ?u.4996
β : Type ?u.4999
s t : Set α✝
a b x y : α✝
f : α✝ → β
α : Type u_1
h : Finite α
hft : Fintype α
⊢ ncard univ = Nat.card α
rw [ncard_eq_toFinset_card, Finite.toFinset_univ, Finset.card_univ, Nat.card_eq_fintype_card]