mathlib

9be82475 - feat(logic/function/embedding): add `function.embedding.option_elim` (#9841)

feat(logic/function/embedding): add `function.embedding.option_elim` (#9841) * add `option.injective_iff`; * add `function.embedding.option_elim`; * use it in the proof of `cardinal.add_one_le_succ`; * add `function.embedding.cardinal_le`, `cardinal.succ_pos`; * add `@[simp]` to `cardinal.lt_succ`.