feat(data/option/basic): `option.map` is injective (#16626)
* prove that `option.map : (α → β) → (option α → option β)` is injective;
* add `iff` version of this lemma;
* add `option.map_comp_some` and `option.map_eq_id`;
* drop `option.map_id'`: it was the same as `option.map_id`.
