case some
α : Type u_2
β : Type u_1
γ : Type ?u.37095
σ : Type ?u.37098
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(Nat.ppred (encode (f a))) = map encode ↑(f a)
α : Type u_2
β : Type u_1
γ : Type ?u.37095
σ : Type ?u.37098
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← Part.bind ↑(decode n) fun a => map encode (↑f a)
      ↑(Nat.ppred n)) =
    Part.bind ↑(decode n) fun a => map encode ((fun a => ↑(f a)) a)
cases' decode (α := α) n with a <;> simp
no goals
case some
α : Type u_2
β : Type u_1
γ : Type ?u.37095
σ : Type ?u.37098
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(Nat.ppred (encode (f a))) = map encode ↑(f a)
cases' f a with b <;> simp