refine ⟨fun ⟨i⟩ ↦ ?_, fun h ↦ ?_⟩
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ Nonempty (Fin n ↪ ↑s) ↔ ↑n ≤ s.encard
case refine_1
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n ≤ s.encard

case refine_2
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : ↑n ≤ s.encard
⊢ Nonempty (Fin n ↪ ↑s)