α : Type u_1
β : Type ?u.57513
inst✝ : LinearOrder α
s : Finset α
i j : Fin (card s)
⊢ ↑(orderEmbOfFin s (_ : card s = card s)) i = ↑(orderEmbOfFin s (_ : card s = card s)) j ↔ ↑i = ↑j
α : Type u_1
β : Type ?u.57513
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : card s = k
h' : card s = l
⊢ ↑(orderEmbOfFin s h) i = ↑(orderEmbOfFin s h') j ↔ ↑i = ↑j
substs k l
no goals
α : Type u_1
β : Type ?u.57513
inst✝ : LinearOrder α
s : Finset α
i j : Fin (card s)
⊢ ↑(orderEmbOfFin s (_ : card s = card s)) i = ↑(orderEmbOfFin s (_ : card s = card s)) j ↔ ↑i = ↑j
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff