α : Type u_2
β : Type u_3
γ✝ : Type ?u.31792
γ : Type u_1
f : α → β
x : Part α
g : β → Part γ
⊢ (Part.bind x fun x => Part.bind ((some ∘ f) x) g) = Part.bind x fun y => g (f y)
α : Type u_2
β : Type u_3
γ✝ : Type ?u.31792
γ : Type u_1
f : α → β
x : Part α
g : β → Part γ
⊢ Part.bind (map f x) g = Part.bind x fun y => g (f y)
rw [← bind_some_eq_map, bind_assoc]
no goals
α : Type u_2
β : Type u_3
γ✝ : Type ?u.31792
γ : Type u_1
f : α → β
x : Part α
g : β → Part γ
⊢ (Part.bind x fun x => Part.bind ((some ∘ f) x) g) = Part.bind x fun y => g (f y)
simp