From f737ca11965922b3e9269f26258c409e9f6c2552 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Tue, 11 Oct 2022 18:36:20 +0000
Subject: [PATCH] feat(data/option/basic): add `bind_some'` (#16641)

We already have `some_bind` `bind_some` `some_bind'`, but there is no `bind_some'`.
---
 src/data/option/basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/data/option/basic.lean b/src/data/option/basic.lean
index 16ff17eba180f..e02a2de4d7611 100644
--- a/src/data/option/basic.lean
+++ b/src/data/option/basic.lean
@@ -110,6 +110,9 @@ theorem eq_none_iff_forall_not_mem {o : option α} :
 @[simp] theorem bind_some : ∀ x : option α, x >>= some = x :=
 @bind_pure α option _ _
 
+@[simp] theorem bind_some' : ∀ x : option α, x.bind some = x :=
+bind_some
+
 @[simp] theorem bind_eq_some {α β} {x : option α} {f : α → option β} {b : β} :
   x >>= f = some b ↔ ∃ a, x = some a ∧ f a = some b :=
 by cases x; simp