rcases (decode e : Option α) <;> simp
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
⊢ ((decode e).bind fun a => if P a then some (encode a) else none) =
    (encode (decode e)).predO.bind fun a => if ∃ a_1, decode a = some a_1 ∧ P a_1 then some a else none
no goals