fix(Data/Option/Defs): Remove Option.rel and Option.maybe, superc…

…eded by std4 (#9178)

Remove `Option.rel` and `Option.maybe`, which have identical definitions to `Option.Rel` and `Option.sequence`, and aren't used anywhere.

Mathlib/Data/Option/Defs.lean

@@ -21,15 +21,6 @@ namespace Option
 
 #align option.lift_or_get Option.liftOrGet
 
-/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
-`none ~ none`. -/
-inductive rel (r : α → β → Prop) : Option α → Option β → Prop
-  | /-- If `a ~ b`, then `some a ~ some b` -/
-    some {a b} : r a b → rel r (some a) (some b)
-  | /-- `none ~ none` -/
-    none : rel r none none
-#align option.rel Option.rel
-
 /-- Traverse an object of `Option α` with a function `f : α → F β` for an applicative `F`. -/
 protected def traverse.{u, v}
     {F : Type u → Type v} [Applicative F] {α : Type*} {β : Type u} (f : α → F β) :
@@ -38,13 +29,7 @@ protected def traverse.{u, v}
   | some x => some <$> f x
 #align option.traverse Option.traverse
 
-/-- If you maybe have a monadic computation in a `[Monad m]` which produces a term of type `α`,
-then there is a naturally associated way to always perform a computation in `m` which maybe
-produces a result. -/
-def maybe.{u, v} {m : Type u → Type v} [Monad m] {α : Type u} : Option (m α) → m (Option α)
-  | none => pure none
-  | some fn => some <$> fn
-#align option.maybe Option.maybe
+#align option.maybe Option.sequence
 
 #align option.mmap Option.mapM
 #align option.melim Option.elimM