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