Eval Dist uniform Sample bind update

lemma evalDist_uniformSample_bind_update    {D R : Type} [Finite D] [DecidableEq D] [Finite R] [Nonempty R]    [SampleableType R] [SampleableType (D → R)] (t : D) :    𝒟[do let u ← $ᵗ R; let g ← $ᵗ (D → R); pure (Function.update g t u)] =      𝒟[$ᵗ (D → R)] := by  classical  letI := Fintype.ofFinite D  letI := Fintype.ofFinite R  haveI : Nonempty (D → R) := ⟨fun _ => Classical.arbitrary R⟩  refine evalDist_ext fun h => ?_  rw [probOutput_uniformSample (D → R) h, probOutput_bind_eq_sum_fintype]  -- For each fixed `u`, count the tables `g` whose `t`-update equals `h`.  have hinner : ∀ u : R,      Pr[= h | (do let g ← $ᵗ (D → R); pure (Function.update g t u))]        = (if u = h t then            (Fintype.card R : ℝ≥0∞) * (Fintype.card (D → R) : ℝ≥0∞)⁻¹ else 0) := by    intro u    rw [bind_pure_comp, probOutput_map_eq_sum_fintype_ite]    simp only [probOutput_uniformSample (D → R)]    rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]    -- The matching tables are exactly `Function.update h t r` for `r : R`.    have hcard :        ((Finset.univ.filter fun g : D → R => h = Function.update g t u).card : ℝ≥0∞)          = if u = h t then (Fintype.card R : ℝ≥0∞) else 0 := by      by_cases hu : u = h t      · have hset : (Finset.univ.filter fun g : D → R => h = Function.update g t u)            = Finset.univ.image (fun r : R => Function.update h t r) := by          ext g          simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]          constructor          · intro hg            exact ⟨g t, by subst hg; simp⟩          · rintro ⟨r, rfl⟩            subst hu; simp        rw [hset, Finset.card_image_of_injective _          (fun r₁ r₂ hr => by simpa using congrFun hr t), Finset.card_univ, if_pos hu]      · rw [if_neg hu, Nat.cast_eq_zero, Finset.card_eq_zero, Finset.filter_eq_empty_iff]        rintro g - rfl        simp at hu    rw [hcard, ite_mul, zero_mul]  simp_rw [hinner, mul_ite, mul_zero]  rw [Finset.sum_ite_eq' Finset.univ (h t), if_pos (Finset.mem_univ _), probOutput_uniformSample R,      ← mul_assoc, ENNReal.inv_mul_cancel (by simp [Fintype.card_ne_zero])        (ENNReal.natCast_ne_top _), one_mul]