case h.e'_1.h.e'_7.h.h
α : Type u_1
β : Type u_3
γ : Type ?u.160634
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → σ
x✝¹ : α
x✝ : ℕ
⊢ Option.map (f x✝¹) (decode x✝) = Option.bind (decode x✝) (Option.some ∘ f x✝¹)
α : Type u_1
β : Type u_3
γ : Type ?u.160634
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Computable₂ fun a n => Option.map (f a) (decode n)) ↔ Computable₂ f
convert (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff
no goals
case h.e'_1.h.e'_7.h.h
α : Type u_1
β : Type u_3
γ : Type ?u.160634
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β → σ
x✝¹ : α
x✝ : ℕ
⊢ Option.map (f x✝¹) (decode x✝) = Option.bind (decode x✝) (Option.some ∘ f x✝¹)
apply Option.map_eq_bind