feat: remove @[simp] from Option.pmap/pbind and add simp lemmas

Author: kim-em

src/Init/Data/Option/Instances.lean

@@ -55,7 +55,7 @@ partial function defined on `a : α` giving an `Option β`, where `some a = x`,
 then `pbind x f h` is essentially the same as `bind x f`
 but is defined only when all `x = some a`, using the proof to apply `f`.
 -/
-@[simp, inline]
+@[inline]
 def pbind : ∀ x : Option α, (∀ a : α, a ∈ x → Option β) → Option β
   | none, _ => none
   | some a, f => f a rfl
@@ -65,7 +65,7 @@ Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α`
 then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
 satisfy `p`, using the proof to apply `f`.
 -/
-@[simp, inline] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) :
+@[inline] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) :
     ∀ x : Option α, (∀ a, a ∈ x → p a) → Option β
   | none, _ => none
   | some a, H => f a (H a rfl)

src/Init/Data/Option/Lemmas.lean

@@ -11,7 +11,11 @@ import Init.Ext
 
 namespace Option
 
-theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = a := .rfl
+theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
+
+@[simp] theorem mem_some {a b : α} : a ∈ some b ↔ a = b := by simp [mem_iff, eq_comm]
+
+theorem mem_some_self (a : α) : a ∈ some a := mem_some.2 rfl
 
 theorem some_ne_none (x : α) : some x ≠ none := nofun
 
@@ -395,4 +399,17 @@ section ite
 
 end ite
 
+/-! ### pbind -/
+
+@[simp] theorem pbind_none : pbind none f = none := rfl
+@[simp] theorem pbind_some : pbind (some a) f = f a (mem_some_self a) := rfl
+
+/-! ### pmap -/
+
+@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+    pmap f none h = none := rfl
+
+@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h}:
+    pmap f (some a) h = f a (h a (mem_some_self a)) := rfl
+
 end Option