case H
α : Type u_1
β : Type u_2
γ : Type ?u.64948
δ : Type ?u.64951
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ ↑(bind f (const α)) a✝ = ↑f a✝
α : Type u_1
β : Type u_2
γ : Type ?u.64948
δ : Type ?u.64951
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ bind f (const α) = f
ext
no goals
case H
α : Type u_1
β : Type u_2
γ : Type ?u.64948
δ : Type ?u.64951
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ ↑(bind f (const α)) a✝ = ↑f a✝
simp