Rel Triple prod

theorem relTriple_prod {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β}    {P : α → Prop} {Q : β → Prop} (hP : ∀ a ∈ support oa, P a) (hQ : ∀ b ∈ support ob, Q b) :    RelTriple oa ob (fun a b => P a ∧ Q b) := by  rw [relTriple_iff_relWP, relWP_iff_couplingPost]  have hp : (𝒟[oa]).toPMF none = 0 := probFailure_eq_zero (mx := oa)  have hq : (𝒟[ob]).toPMF none = 0 := probFailure_eq_zero (mx := ob)  refine ⟨_root_.SPMF.Coupling.prod hp hq, ?_⟩  intro z hz  rcases (mem_support_bind_iff (𝒟[oa])    (fun a => 𝒟[ob] >>= fun b => (pure (a, b) : SPMF (α × β))) z).1 hz with    ⟨a, ha, hz'⟩  have ha_supp : a ∈ support oa :=    (mem_support_iff (mx := oa) (x := a)).2      (by simpa [probOutput_def] using (mem_support_iff (mx := 𝒟[oa]) (x := a)).1 ha)  rcases (mem_support_bind_iff (𝒟[ob])    (fun b => (pure (a, b) : SPMF (α × β))) z).1 hz' with ⟨b, hb, hz''⟩  have hb_supp : b ∈ support ob :=    (mem_support_iff (mx := ob) (x := b)).2      (by simpa [probOutput_def] using (mem_support_iff (mx := 𝒟[ob]) (x := b)).1 hb)  obtain rfl : z = (a, b) := by simpa [support_pure, Set.mem_singleton_iff] using hz''  exact ⟨hP a ha_supp, hQ b hb_supp⟩