Lean/Mathlib: simp won't reduce `Part.some a >>= B` when B : ℕ →. ℕ

After Nat.RecursiveIn.comp hB hg |>.of_eq, the goal had the form Part.some x >>= B = ... with B : ℕ →. ℕ (a PFun). simp only [Part.bind_eq_bind, Part.bind_some] reported both lemmas unused, and rw [hBX] (with hBX : B x = ...) failed with a motive error saying 'B has type ℕ →. ℕ but is expected to have type ℕ → Part ℕ'. The PFun-typed function blocks syntactic matching with the Monad Part instance. A fix that works: a calc step _ = B x := Part.bind_some _ _, which is accepted up to defeq, and then rewrite in the second step. Defining B as fun m => ... : ℕ → Part ℕ instead of ℕ →. ℕ probably avoids the problem as well.