mathlib

995b47e5 - refactor(*): use `option.map₂` (#18081)

refactor(*): use `option.map₂` (#18081) Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>