obtain (hfin | hinf) := s.finite_or_infinite
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hfin : s.Finite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard