Posterior Dist eq prior of output Indist

theorem posteriorDist_eq_prior_of_outputIndist (p : PMF α) (f : α → PMF β)    (h : ∀ a₀ a₁ : α, f a₀ = f a₁)    (b : β) (hb : b ∈ (p.bind f).support) :    posteriorDist p f b hb = p := by  ext a  rw [posteriorDist_apply, bind_pair_apply, PMF.bind_apply]  have hf : ∀ a', f a' b = f a b := fun a' => by rw [h a' a]  simp_rw [hf]  rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]  have hb' : (p.bind f) b ≠ 0 := (PMF.mem_support_iff _ _).mp hb  have hmarg : (p.bind f) b = f a b := by    rw [PMF.bind_apply]    simp_rw [hf]    rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]  exact ENNReal.mul_div_cancel_right (hmarg ▸ hb')    (ne_top_of_le_ne_top ENNReal.one_ne_top (PMF.coe_le_one _ _))