no goals
α : Type u_1
β : Type ?u.49125
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ ↑(orderEmbOfFin {a} (_ : card {a} = 1)) i = a
rw [Subsingleton.elim i ⟨0, zero_lt_one⟩, orderEmbOfFin_zero _ zero_lt_one, min'_singleton]