case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0
cases finite_or_infinite β
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0
haveI := card_eq_zero_iff.mp h
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
haveI := Function.isEmpty f
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0
exact Nat.card_of_isEmpty
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0
haveI := Infinite.of_surjective f hf
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.4320
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0
exact Nat.card_eq_zero_of_infinite