convert ((Equiv.Set.univ (Fin n)).toEmbedding.trans i).enccard_le
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 h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n = univ.encard