Eval Dist uniform Sample map comp injective

lemma evalDist_uniformSample_map_comp_injective    {A B R : Type} [Finite A] [Finite B] [Finite R]    [Nonempty R] [SampleableType R] [SampleableType (A → R)] [SampleableType (B → R)]    {e : A → B} (he : Function.Injective e) :    𝒟[do let g ← $ᵗ (B → R); pure (g ∘ e)] = 𝒟[$ᵗ (A → R)] := by  classical  letI := Fintype.ofFinite A  letI := Fintype.ofFinite B  letI := Fintype.ofFinite R  letI : Inhabited R := Classical.inhabited_of_nonempty inferInstance  set C := {b : B // b ∉ Set.range e}  -- A table `g : B → R` is determined by its restriction `g ∘ e` along `e` and its values off  -- `range e`, splitting `B → R` as the product `(A → R) × (C → R)` via the reindexing of `B` by  -- `A ⊕ C` along `e` and the complement inclusion.  set φ : (B → R) ≃ (A → R) × (C → R) :=    (Equiv.arrowCongr ((Equiv.Set.sumCompl (Set.range e)).symm.trans      ((Equiv.ofInjective e he).symm.sumCongr (Equiv.refl C))) (Equiv.refl R)).trans      (Equiv.sumArrowEquivProdArrow _ _ _)  have hφ1 : ∀ g : B → R, (φ g).1 = g ∘ e := fun g => funext fun a => by    simp [φ, Equiv.sumArrowEquivProdArrow, Equiv.ofInjective]  calc 𝒟[do let g ← $ᵗ (B → R); pure (g ∘ e)]      = 𝒟[Prod.fst <$> (φ <$> ($ᵗ (B → R)))] := by        simp only [bind_pure_comp, Functor.map_map, Function.comp_def, hφ1]    _ = 𝒟[Prod.fst <$> ($ᵗ ((A → R) × (C → R)))] := by        rw [evalDist_map, evalDist_ext fun p =>          probOutput_map_bijective_uniform_cross (α := B → R) φ φ.bijective p, ← evalDist_map]    _ = 𝒟[$ᵗ (A → R)] := evalDist_map_fst_uniformSample_prod