α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Set.Infinite ∅
⊢ False
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Infinite s
⊢ s ≠ ∅
rintro rfl
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Set.Infinite ∅
⊢ False
exact h finite_empty