Sq prob Output bind le prob Output bind prod

lemma sq_probOutput_bind_le_probOutput_bind_prod    (source : m α) (kernel : α → m β) (y : β) :    Pr[= y | source >>= kernel] ^ 2 ≤      Pr[= (y, y) | source >>= fun x => do        let a ← kernel x        let b ← kernel x        pure (a, b)] := by  have hfactor (x : α) :      Pr[= (y, y) | do        let a ← kernel x        let b ← kernel x        pure (a, b)] = Pr[= y | kernel x] * Pr[= y | kernel x] := by    rw [probOutput_bind_bind_prod_mk_eq_mul']    simp only [show (fun a : β ↦ a) = id from rfl, id_map]  rw [probOutput_bind_eq_tsum source kernel y,    probOutput_bind_eq_tsum source (fun x ↦ do      let a ← kernel x      let b ← kernel x      pure (a, b)) (y, y)]  refine (ENNReal.sq_tsum_le_tsum_sq    (fun x ↦ Pr[= x | source]) (fun x ↦ Pr[= y | kernel x])      (tsum_probOutput_le_one (mx := source))).trans_eq ?_  refine tsum_congr fun x ↦ ?_  rw [hfactor]  simp [sq]