Prob Output ddh Exp Rand cdh To DDHReduction eq uniform Scalar

theorem probOutput_ddhExpRand_cdhToDDHReduction_eq_uniformScalar    [Fintype F] (g : G) (hg : Function.Bijective (· • g : F → G))    (adversary : CDHAdversary F G) :    Pr[= true | ddhExpRand g (cdhToDDHReduction (F := F) adversary)] =      (Fintype.card F : ℝ≥0∞)⁻¹ := by  simp only [ddhExpRand, cdhToDDHReduction]  have key : ∀ a b : F,      Pr[= true | ($ᵗ F) >>= fun c =>        adversary g (a • g) (b • g) >>= fun h =>          pure (decide (h = c • g))] =        (Fintype.card F : ℝ≥0∞)⁻¹ := by    intro a b    rw [probOutput_bind_bind_swap, probOutput_bind_of_const _ fun h _ =>      probOutput_decide_smul_eq_inv_card g hg h]    simp [probFailure_of_liftM_PMF]  rw [probOutput_bind_of_const _ fun a _ =>    probOutput_bind_of_const _ fun b _ => key a b]  simp [probFailure_of_liftM_PMF]