rw [hinf.encard_eq, iff_true_intro le_top, true_iff, iff_false_intro hinf, false_imp_iff]
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ ↑n ≤ s.encard ↔ s.Finite → n ≤ s.ncard
case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
hinf : s.Infinite
⊢ True