no goals
α : Type u_1
β : Type ?u.61522
γ : Type ?u.61525
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x y : α
hy : y ≠ x
⊢ ↑p y * ↑(pure y) x = 0
rw [pure_apply_of_ne _ _ hy.symm, MulZeroClass.mul_zero]
no goals
α : Type u_1
β : Type ?u.61522
γ : Type ?u.61525
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x : α
⊢ ↑p x * ↑(pure x) x = ↑p x
rw [pure_apply_self, mul_one]