feat(logic/equiv/option): equivalence with subtypes (#16302)
Add an equivalence between equivalences
```lean
/-- Equivalences between `option α` and `β` that send `none` to `x` are equivalent to
equivalences between `α` and `{y : β // y ≠ x}`. -/
def option_subtype [decidable_eq β] (x : β) :
{e : option α ≃ β // e none = x} ≃ (α ≃ {y : β // y ≠ x}) :=
```
which can be used to give a much simpler definition of an equivalence
in #16278.
