∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : LinearOrder α] {m n : ℕ} {s : Finset α}
  (hm : s.card = m) (hn : sᶜ.card = n) (i : Fin m), (finSumEquivOfFinset hm hn) (Sum.inl i) = (s.orderEmbOfFin hm) i