Prob split last uniform sampling of fin Fun

theorem prob_split_last_uniform_sampling_of_finFun {ϑ : ℕ} {F : Type} [Fintype F] [Nonempty F]    (P : F → (Fin ϑ → F) → Prop)    :    Pr_{ let r ← $ᵖ (Fin (ϑ + 1) → F) }[ P (r (Fin.last ϑ)) (fun i ↦ r i.castSucc) ] =    Pr_{ let r_last ← $ᵖ F; let r_init ← $ᵖ (Fin ϑ → F) }[ P r_last r_init ] := by  classical  rw [prob_tsum_form_doubleton]  let e : (Fin (ϑ + 1) → F) ≃ F × (Fin ϑ → F) := equivFinFunSplitLast  conv_lhs =>    rw [prob_split_uniform_sampling_of_equiv_prod (e := e)]  rw [prob_tsum_form_doubleton]  congr 1  funext xy  congr 1  have hEquiv_r_last : e.symm (xy.1, xy.2) (Fin.last ϑ) = xy.1 := by    simp only [equivFinFunSplitLast, Prod.mk.eta, Equiv.coe_fn_symm_mk, Fin.snoc_last, e]  have hEquiv_r_init : ∀ i: Fin ϑ, e.symm (xy.1, xy.2) i.castSucc = xy.2 i := by    simp only [equivFinFunSplitLast, Prod.mk.eta, Equiv.coe_fn_symm_mk, Fin.snoc_castSucc,      implies_true, e]  simp_rw [hEquiv_r_last, hEquiv_r_init]