α : Type u_1
β : Type ?u.49896
γ : Type ?u.49899
x : Part α
⊢ map (fun a => a) x = x
α : Type u_1
β : Type ?u.49896
γ : Type ?u.49899
x : Part α
⊢ Part.bind x some = x
erw [bind_some_eq_map]
no goals
α : Type u_1
β : Type ?u.49896
γ : Type ?u.49899
x : Part α
⊢ map (fun a => a) x = x
simp [map_id']