mathlib3

44c31d8f - feat(data/finset/basic): add `map_injective` and `sigma_equiv_option_of_inhabited` (#13083)

feat(data/finset/basic): add `map_injective` and `sigma_equiv_option_of_inhabited` (#13083) Adds `map_injective (f : α ↪ β) : injective (map f) := (map_embedding f).injective` and `sigma_equiv_option_of_inhabited [inhabited α] : Σ (β : Type u), α ≃ option β`. Extracted from @huynhtrankhanh's https://github.com/leanprover-community/mathlib/pull/11162, moved here to a separate PR Co-authored-by: Huỳnh Trần Khanh [qcdz9r6wpcbh59@gmail.com](mailto:qcdz9r6wpcbh59@gmail.com)