Prob split uniform sampling of equiv prod

theorem prob_split_uniform_sampling_of_equiv_prod {α γ δ : Type}    -- Fintype & Nonempty assumptions for all types    [Fintype α] [Fintype γ] [Fintype δ]    [Nonempty α] [Nonempty γ] [Nonempty δ]    -- The equivalence that splits α into γ × δ    (e : α ≃ γ × δ)    -- The predicate on the original (combined) type    (P : α → Prop)    :    -- LHS: Probability over the combined space    Pr_{ let r ← $ᵖ α }[ P r ] =    -- RHS: Probability over the sequential, split spaces    Pr_{ let x ← $ᵖ γ; let y ← $ᵖ δ }[ P (e.symm (x, y)) ] := by  classical  -- 1. Unroll the LHS (a single `let`) using `prStx_unfold_final`  -- LHS = ∑' r, Pr[r] * (if P r then 1 else 0)  rw [prob_tsum_form_singleton]  let D_rest := fun (x : γ) => (do    let y ← $ᵖ δ    return (P (e.symm (x, y)))  )  conv_rhs =>    apply prob_tsum_form_split_first (D := $ᵖ γ) (D_rest := D_rest)  simp_rw [D_rest]  simp only [PMF.uniformOfFintype_apply, mul_ite, mul_one, mul_zero]  simp_rw [prob_tsum_form_singleton]  -- ⊢ (∑' (x : α), ... = ∑' (x : γ), (↑(Fintype.card γ))⁻¹ * ∑' (x_1 : δ), ...  conv_rhs => enter [1, x]; rw [←ENNReal.tsum_mul_left]  -- ⊢ (∑' (x : α), ... = ∑' (x : γ) (i : δ), ...  rw [←ENNReal.tsum_prod]  -- ⊢ (∑' (x : α), ...) = (∑' (p : γ × δ), ...)  conv_lhs =>    rw [tsum_eq_sum (α := ENNReal) (β := α) (f :=      fun x => if P x then (↑(Fintype.card α))⁻¹ else 0) (s := Finset.univ) (hf := fun b => by      simp only [mem_univ, not_true_eq_false, ite_eq_right_iff, ENNReal.inv_eq_zero,        IsEmpty.forall_iff]    )]  conv_rhs =>    rw [tsum_eq_sum (α := ENNReal) (β := γ × δ) (f := fun x =>      (↑(Fintype.card γ))⁻¹ * (($ᵖ δ) x.2 * if P (e.symm x) then 1 else 0)    ) (s := Finset.univ) (hf := fun b => by      simp only [mem_univ, not_true_eq_false, IsEmpty.forall_iff]    )]  -- ⊢ (∑ b : α, .. = ..) = (∑ b : γ × δ, ..)  have hcard_of_equiv: (Fintype.card α) = (Fintype.card (γ × δ)) := Fintype.card_congr e  rw [Finset.sum_equiv (s := Finset.univ (α := α)) (t := Finset.univ (α := γ × δ))    (f := fun x => if P x then (↑(Fintype.card α))⁻¹ else 0)    (g := fun x => (↑(Fintype.card γ))⁻¹ * (($ᵖ δ) x.2 * if P (e.symm x) then 1 else 0))    (e := e) (hst := fun i => by    simp only [mem_univ]  ) (hfg := fun i => by    simp only [mem_univ, PMF.uniformOfFintype_apply, Equiv.symm_apply_apply, mul_ite, mul_one,      mul_zero, forall_const]    by_cases hP : P i    · simp only [hP, ↓reduceIte]      rw [hcard_of_equiv]      rw [ENNReal.mul_inv_rev_ENNReal (ha := Fintype.card_ne_zero)]      rw [Fintype.card_prod]; rw [Nat.cast_mul]    · simp only [hP, ↓reduceIte]  )]