feat(data/option/basic): add `option.coe_get` (#13081)
Adds lemma `coe_get {o : option α} (h : o.is_some) : ((option.get h : α) : option α) = o`
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)
