case h.e'_5.h
α : Type u_2
β : Type u_1
γ : Type ?u.185392
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
x✝ : α
⊢ Option.map (g x✝) (f x✝) = Option.bind (f x✝) fun b => Option.some (g x✝ b)
α : Type u_2
β : Type u_1
γ : Type ?u.185392
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
⊢ Computable fun a => Option.map (g a) (f a)
convert option_bind hf (option_some.comp₂ hg)
no goals
case h.e'_5.h
α : Type u_2
β : Type u_1
γ : Type ?u.185392
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
x✝ : α
⊢ Option.map (g x✝) (f x✝) = Option.bind (f x✝) fun b => Option.some (g x✝ b)
apply Option.map_eq_bind