{ by_cases hs : P s <;> simp[hs] }
case some
α✝ : Type u_1
inst✝² : Encodable α✝
α : Type u_1
P : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred P
e : ℕ
s : α
h : decode e = some s
⊢ Option.rec 0 (fun val => encode ↑val + 1) (if h : P s then some ⟨s, ⋯⟩ else none) =
    Option.rec 0 (fun val => encode val + 1) (if P s then some s else none)
no goals