diff --git a/Complexity.lean b/Complexity.lean
index 209115a40..1810caf83 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1741,6 +1741,7 @@ public import Complexity.Languages.Probabilistic.Forking
 public import Complexity.Languages.Probabilistic.Iteration
 public import Complexity.Languages.Probabilistic.LinearHash
 public import Complexity.Languages.Probabilistic.Memoize
+public import Complexity.Languages.Probabilistic.Notation
 public import Complexity.Languages.Probabilistic.Oracle
 public import Complexity.Languages.Probabilistic.Oracle.Interaction
 public import Complexity.Languages.Probabilistic.Oracle.Simulation
diff --git a/Complexity/Crypto/Computational/Basic.lean b/Complexity/Crypto/Computational/Basic.lean
index 5ef01cbcd..9027b2ed5 100644
--- a/Complexity/Crypto/Computational/Basic.lean
+++ b/Complexity/Crypto/Computational/Basic.lean
@@ -81,15 +81,6 @@ theorem eval_bind_eq_distinguishingGame (sample : ProbComp (List Bool))
     ProbComp.eval (sample >>= adversary) = distinguishingGame (ProbComp.eval sample) adversary :=
   ProbComp.eval_bind _ _
 
-/-- Success after sampling a finite intermediate value is its weighted average. -/
-theorem Game.coe_succProbability_eval_bind {α : Type} [Fintype α]
-    (source : ProbComp α) (next : α → ProbComp Bool) :
-    (Game.succProbability (ProbComp.eval (source >>= next)) : ℝ) =
-      ∑ a, (ProbComp.eval source a).toReal *
-        (Game.succProbability (ProbComp.eval (next a)) : ℝ) := by
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.eval_bind,
-    Probability.PMF.bind_apply_toReal]
-
 /-- Postprocessing the distinguisher's answer postprocesses the experiment's answer. -/
 theorem distinguishingGame_map (distribution : PMF (List Bool))
     (adversary : List Bool → ProbComp Bool) (f : Bool → Bool) :
diff --git a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
index 7734619fe..eb54286e6 100644
--- a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
+++ b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.GoldreichLevin.WordDecoder
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.OneWay
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Computability.Probabilistic.CoinTape
 import Complexity.Tactic.PPT
 
@@ -53,8 +54,6 @@ namespace Cslib.Crypto.GoldreichLevin
 
 open Probability BitString Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- The saved tape covers the unary parameter, the whole image and an `n`-bit query. -/
 def coinBudget (c d n imageLength : ℕ) : ℕ := c * (3 * n + imageLength + 2) ^ d
 
@@ -183,7 +182,7 @@ theorem word_prediction_advantage_le (f : List Bool → List Bool) (adversary :
     |Pr[parityPredictionGame f adversary n] - 1 / 2| ≤
       1 / (precision degree n : ℝ) +
         8 * Pr[inversionGame f (wordInverter f evaluate c d degree) n] := by
-  simp only [Game.succProbability, eval_parityPredictionGame f adversary evaluate c d hrealize,
+  simp only [eval_parityPredictionGame f adversary evaluate c d hrealize,
     eval_wordInversionGame f]
   exact invertSigned_advantage_le _ _ _ _ (precision_pos degree n)
 
diff --git a/Complexity/Crypto/Computational/HardCore.lean b/Complexity/Crypto/Computational/HardCore.lean
index bf913e7bc..08cb5f149 100644
--- a/Complexity/Crypto/Computational/HardCore.lean
+++ b/Complexity/Crypto/Computational/HardCore.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly
 public import Complexity.Crypto.Computational.OneWay
 public import Complexity.Crypto.Computational.Prediction
 public import Complexity.Crypto.Computational.PseudorandomGenerator
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -24,7 +25,8 @@ to be one-way or injective.
 The reduction appends a fixed trial bit to the image, runs a distinguisher, and predicts the trial
 on acceptance or its complement on rejection. The distinguishing gap is the average of the signed
 biases of the two fixed predictors. Both are single uniform programs, with no choice depending on
-the security parameter. `Pr[p]` abbreviates the existing game's success probability in the reals.
+the security parameter. `Pr[p]` is the probability, in the reals, that the program `p` returns
+`true` (the scoped notation of `Cslib.Probability`).
 
 Appending a hard-core predicate to an efficient length-preserving permutation gives a one-bit PRG
 in the existing finite-family security API. This is conditional on the hard-core predicate;
@@ -58,11 +60,6 @@ namespace Cslib.Crypto
 open Probability Turing.MultiTapeTM
 open scoped NNReal
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
-private theorem coe_probability (game : Game) :
-    (Game.succProbability game : ℝ) = (game true).toReal := rfl
-
 /-- Predict a predicate of a uniform seed, given only its image and the security parameter. -/
 noncomputable def predictionGame (f : List Bool → List Bool) (predicate : List Bool → Bool)
     (adversary : Distinguisher) (n : ℕ) : ProbComp Bool := do
@@ -138,7 +135,7 @@ private theorem real_probability (f : List Bool → List Bool) (predicate : List
     Pr[prgRealGame (fun seed => f seed ++ [predicate seed]) adversary n] =
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         Pr[adversary n (f (List.ofFn bits) ++ [predicate (List.ofFn bits)])] := by
-  simp only [coe_probability, eval_prgRealGame, distinguishingGame, PMF.monad_bind_eq_bind,
+  simp only [eval_prgRealGame, distinguishingGame, PMF.monad_bind_eq_bind,
     generatorEnsemble,
     BitString.uniformList, PMF.bind_map, Function.comp_def, PMF.map_comp, PMF.bind_apply_toReal]
 
@@ -148,7 +145,7 @@ private theorem ideal_probability (f : List Bool → List Bool) (adversary : Dis
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         ((Pr[adversary n (f (List.ofFn bits) ++ [false])] +
           Pr[adversary n (f (List.ofFn bits) ++ [true])]) / 2) := by
-  simp only [coe_probability, distinguishingGame, hardCoreIdeal, PMF.monad_bind_eq_bind,
+  simp only [Game.coe_succProbability, distinguishingGame, hardCoreIdeal, PMF.monad_bind_eq_bind,
     BitString.uniformList,
     PMF.bind_map, PMF.bind_bind, Function.comp_def, PMF.bind_apply_toReal]
   apply Finset.sum_congr rfl
@@ -162,7 +159,7 @@ private theorem prediction_probability (f : List Bool → List Bool) (predicate
       ∑ bits : BitString n, ((PMF.uniformOfFintype (BitString n)) bits).toReal *
         Pr[(fun guess => guess == predicate (List.ofFn bits)) <$> adversary n (f (List.ofFn bits))]
       := by
-  simp only [coe_probability, predictionGame, ProbComp.eval_bind, BitString.eval_sampleList,
+  simp only [predictionGame, ProbComp.eval_bind, BitString.eval_sampleList,
     BitString.uniformList, PMF.bind_map, Function.comp_def, ProbComp.eval_map, ProbComp.eval_pure]
   rw [PMF.bind_apply_toReal]
   rfl
@@ -194,7 +191,8 @@ theorem hardCore_advantage_le (f : List Bool → List Bool) (predicate : List Bo
   apply NNReal.coe_le_coe.mp
   rw [Game.coe_advantage, NNReal.coe_div, NNReal.coe_add, NNReal.coe_ofNat,
     predictionAdvantage, predictionAdvantage, Game.coe_guessingAdvantage,
-    Game.coe_guessingAdvantage, hardCore_gap]
+    Game.coe_guessingAdvantage,
+    Game.coe_succProbability (ProbComp.eval (prgRealGame _ adversary n)), hardCore_gap]
   let left := Pr[predictionGame f predicate (hardCorePredictor adversary false) n]
   let right := Pr[predictionGame f predicate (hardCorePredictor adversary true) n]
   change |(left + right - 1) / 2| ≤ (|left - 1 / 2| + |right - 1 / 2|) / 2
diff --git a/Complexity/Crypto/Computational/Prediction.lean b/Complexity/Crypto/Computational/Prediction.lean
index 9512db16b..5fae10b1f 100644
--- a/Complexity/Crypto/Computational/Prediction.lean
+++ b/Complexity/Crypto/Computational/Prediction.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Basic
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Probability.PMF
 import Complexity.Tactic.PPT
 
@@ -18,8 +19,8 @@ The predictor supplies a trial bit to a test and returns that bit on acceptance,
 on rejection. Averaging over an independent fair trial turns the test's signed distinguishing gap
 into prediction bias. The hidden bit is not an input to the predictor.
 
-`Pr[p]` below is local notation for the existing game's success probability, coerced to the reals
-to express signed differences. It introduces no additional probability or security definition.
+`Pr[p]` is the scoped notation of `Cslib.Probability` for the probability, in the reals, that `p`
+returns `true`, so gaps and biases are signed differences.
 
 ## Main definitions
 
@@ -48,8 +49,6 @@ namespace Cslib.Crypto
 
 open Probability Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- Predict a trial bit on acceptance and its complement on rejection. -/
 def trialPredictor (test : Bool → ProbComp Bool) (trial : Bool) : ProbComp Bool :=
   (fun accept => if accept then trial else !trial) <$> test trial
@@ -68,14 +67,12 @@ theorem trialPredictor_gap (test : Bool → ProbComp Bool) (truth : Bool) :
   | false =>
     simp only [trialPredictor, Bool.not_false, Bool.not_true, beq_false,
       Functor.map_map, Bool.ite_true_right, Bool.ite_false_right, Bool.decide_eq_true,
-      Bool.or_false, Bool.and_true, Bool.not_not, id_map',
-      Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.probability_not]
+      Bool.or_false, Bool.and_true, Bool.not_not, id_map', ProbComp.probability_not]
     ring
   | true =>
     simp only [beq_true, trialPredictor, Bool.not_false, Bool.ite_true_right,
       Bool.decide_eq_true, Bool.or_false, Functor.map_map, Bool.not_true, Bool.ite_false_right,
-      Bool.and_true, id_map',
-      Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
+      Bool.and_true, id_map']
     rw [show (fun accept => !accept) = Bool.not from rfl, ProbComp.probability_not]
     ring
 
@@ -84,11 +81,9 @@ theorem probability_bitPredictor (test : Bool → ProbComp Bool) (truth : Bool)
     Pr[(fun guess => guess == truth) <$> bitPredictor test] =
       (Pr[(fun guess => guess == truth) <$> trialPredictor test false] +
         Pr[(fun guess => guess == truth) <$> trialPredictor test true]) / 2 := by
-  change (ProbComp.eval _ true).toReal = _
   simp only [bitPredictor, map_bind, ProbComp.eval_bind, ProbComp.eval_uniform,
     PMF.bind_apply_toReal]
-  norm_num [Fintype.sum_bool, PMF.uniformOfFintype_apply, Game.succProbability, ENNReal.toReal,
-    ENNReal.toNNReal_ofNat]
+  norm_num [Fintype.sum_bool, PMF.uniformOfFintype_apply]
   ring
 
 /-- The randomized predictor's bias equals the gap between the real label and a fair label. -/
@@ -130,20 +125,18 @@ theorem probability_calibratedTest (real ideal challenge : ProbComp Bool) :
   let direction := bitPredictor (fun trial => if trial then real else ideal)
   have htotal := PMF.toReal_true_add_toReal_false (ProbComp.eval direction)
   have hbias := bitPredictor_bias (fun trial => if trial then real else ideal) true
-  simp only [beq_true, id_map', ite_true, Bool.false_eq_true, ite_false,
-    Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hbias
-  simp only [calibratedTest, Game.coe_succProbability_eval_bind, Fintype.sum_bool, beq_false,
-    beq_true, id_map']
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, ProbComp.probability_not]
-  linear_combination (1 - (ProbComp.eval challenge true).toReal) * htotal +
-    (2 * (ProbComp.eval challenge true).toReal - 1) * hbias
+  simp only [beq_true, id_map', ite_true, Bool.false_eq_true, ite_false] at hbias
+  simp only [calibratedTest, ProbComp.probability_bind, Fintype.sum_bool, beq_false,
+    beq_true, id_map', ProbComp.probability_not]
+  linear_combination (1 - Pr[challenge]) * htotal +
+    (2 * Pr[challenge] - 1) * hbias
 
 /-- The same calibration on both sides turns a possibly negative gap into its square. -/
 theorem calibratedTest_gap (real ideal : ProbComp Bool) :
     Pr[calibratedTest real ideal real] -
       Pr[calibratedTest real ideal ideal] =
       (Game.advantage (ProbComp.eval real) (ProbComp.eval ideal) : ℝ) ^ 2 := by
-  simp only [probability_calibratedTest, Game.coe_advantage, sq_abs]
+  simp only [probability_calibratedTest, Game.coe_advantage, Game.coe_succProbability, sq_abs]
   ring
 
 /-- Calibration is an ordinary PPT composition of its three supplied experiments. -/
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean b/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean
index 750c34751..762cea39f 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Probability.Entropy
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -55,8 +56,6 @@ namespace Cslib.Crypto.Pseudoentropy
 
 open Probability Filter Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- Predict the hidden bit from the public component of a sampled pair. -/
 def predictionGame (sample : ℕ → ProbComp (List Bool × Bool))
     (adversary : Distinguisher) (n : ℕ) : ProbComp Bool := do
@@ -129,7 +128,6 @@ theorem HasGap.eventually_error_ge {pair : SamplablePair} {gap : ℕ → ℝ}
   filter_upwards [hgap adversary hefficient] with n hn
   have hsum := PMF.toReal_true_add_toReal_false
     (ProbComp.eval (predictionGame pair.sample adversary n))
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hn
   linarith
 
 /-- A fair-bit predictor has zero correlation, so entropy plus the prediction gap cannot
@@ -140,8 +138,7 @@ theorem HasGap.eventually_entropy_add_gap_le_one {pair : SamplablePair} {gap : 
   have h := hgap (fun _ _ => ProbComp.uniform Bool) (by ppt)
   have hfair (n : ℕ) :
       Pr[predictionGame pair.sample (fun _ _ => ProbComp.uniform Bool) n] = 1 / 2 := by
-    simp [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, predictionGame,
-      ProbComp.eval_bind, ProbComp.eval_map, PMF.bind_apply, PMF.map_apply,
+    simp [predictionGame, ProbComp.eval_bind, ProbComp.eval_map, PMF.bind_apply, PMF.map_apply,
       PMF.uniformOfFintype_apply, ENNReal.tsum_mul_right, PMF.tsum_coe]
   filter_upwards [h] with n hn
   rw [hfair] at hn
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean
index 879c43d19..502bbd282 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Loop
 public import Complexity.Computability.Probabilistic.Selection
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Probability.PMF.Expect
 import Complexity.Tactic.PPT
 
@@ -52,8 +53,6 @@ namespace Cslib.Crypto.Pseudoentropy.Boosting
 
 open Probability BitString Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 variable {α : Type}
 
 /-- Run a trial on a freshly weighted example, with a fair baseline when its weight coin fails. -/
@@ -72,7 +71,7 @@ private theorem gate_probability (mask test : ProbComp Bool) :
   have hfair : Pr[ProbComp.uniform Bool] = 1 / 2 := by
     simp [PMF.uniformOfFintype_apply]
   rw [hfair]
-  change _ = 1 / 2 + (ProbComp.eval mask true).toReal * _
+  change _ = 1 / 2 + Pr[mask] * _
   nlinarith
 
 /-- Acceptance above a fair baseline is exactly the mask-weighted trial bias. -/
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean
index 31cfa9d86..24f148ece 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Basic
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Crypto.Computational.Pseudoentropy.Selection
 import Complexity.Crypto.Computational.Pseudoentropy.SequenceLearner
 import Complexity.Tactic.PPT
@@ -50,8 +51,6 @@ namespace Cslib.Crypto.Pseudoentropy.SamplablePair
 
 open Probability Probability.PMF BitString Boosting Filter Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 /-- All tests in a uniformly efficient polynomial-size family eventually admit dense soft masks
 with small distinguishing gap whenever their density is valid. The common eventual threshold
 allows arbitrary choices of index in the proof without supplying that choice to the program. -/
@@ -183,8 +182,7 @@ theorem HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ
       (fun value => pair.encode n value.1) Prod.snd (count n) (width n) (params n i) state
         (pair.encode n value.1)
         (hsize' n value (by simpa only [pair.eval_latentSample] using hvalue)))
-    (by simpa only [source, pair.eval_latentSample, Game.coe_advantage, Game.succProbability,
-      ENNReal.coe_toNNReal_eq_toReal]
+    (by simpa only [source, pair.eval_latentSample, Game.coe_advantage, Game.coe_succProbability]
       using hdistinguish)
   have hlaw : ProbComp.eval (predictionGame pair.sample (fun n => adversary n i) n) =
       ProbComp.eval (do
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Learning.lean b/Complexity/Crypto/Computational/Pseudoentropy/Learning.lean
index 6d0ab7b14..4bb4c0d14 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/Learning.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/Learning.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
 public import Complexity.Crypto.Computational.Pseudoentropy.RepeatedExtraction
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Learner
+import Complexity.Languages.Probabilistic.Notation
 
 /-!
 # From sequence distinguishers to a learned predictor
@@ -46,8 +47,6 @@ namespace Cslib.Crypto.Pseudoentropy
 
 open Probability Probability.PMF BitString Boosting
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 variable {α β : Type}
 
 /-- The complete sequence gap is the dyadic coordinate count times the average weighted
@@ -80,9 +79,7 @@ theorem maskedSequence_validation_gap [Finite α]
         candidates >>= fun code => pure (predict code (observe value) == truth value))] :=
     congrArg (fun law : PMF Bool => (law true).toReal)
       (eval_weightedTrial_bind candidates source mask _)
-  have hgap := maskedSequence_prediction_gap source observe truth mask count test
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] at hgap
-  rw [hgap, hvalidation, weightedTrial_probability]
+  rw [maskedSequence_prediction_gap, hvalidation, weightedTrial_probability]
   simp only [add_sub_cancel_left]
   congr 1
   apply Finset.sum_congr rfl
@@ -167,7 +164,6 @@ theorem extractedSequence_learn_error_pow {Seed Output : Type} [Fintype α]
   have h := extractLabels_sequence_gap ((fun value => (observe value, truth value)) <$> source)
     (maskedSample source observe truth mask) count seed hash test ideal hclose
   have hgap' := (le_sub_iff_add_le.mpr hdistinguish).trans h
-  simpa only [Game.coe_advantage, Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
-    using hgap'
+  simpa only [Game.coe_advantage, Game.coe_succProbability] using hgap'
 
 end Cslib.Crypto.Pseudoentropy
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean
index 165055385..69c35ac38 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Pseudoentropy.Masking
 public import Complexity.Crypto.Computational.Pseudoentropy.RepeatedExtraction
+import Complexity.Languages.Probabilistic.Notation
 
 /-!
 # Extracting fresh masked labels
@@ -46,8 +47,6 @@ open Probability Probability.PMF BitString
 
 open scoped NNReal
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 /-- Fresh masking preserves the complete public marginal. -/
 theorem maskedSample_map_fst {α β : Type} (source : ProbComp α)
     (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) :
@@ -64,7 +63,7 @@ theorem maskedSample_map_fst {α β : Type} (source : ProbComp α)
 probability at least `mass / 2`. Keeping the original label always has probability at least half. -/
 theorem maskBit_mass_ge (mask : ProbComp Bool) (truth bit : Bool) {mass : ℝ}
     (hmass : mass ≤ 1)
-    (hmask : 0 < (ProbComp.eval mask true).toReal → mass ≤ (ProbComp.eval mask true).toReal)
+    (hmask : 0 < Pr[mask] → mass ≤ Pr[mask])
     (hbit : bit ∈ (ProbComp.eval (maskBit mask truth)).support) :
     mass / 2 ≤ (ProbComp.eval (maskBit mask truth) bit).toReal := by
   have hpositive : 0 < (ProbComp.eval (maskBit mask truth) bit).toReal :=
@@ -87,8 +86,7 @@ theorem maskedSample_mass_ge {α β : Type} (source : ProbComp α)
     (hsource : ∀ value ∈ (ProbComp.eval source).support,
       sourceMass ≤ (ProbComp.eval source value).toReal)
     (hmask : ∀ value ∈ (ProbComp.eval source).support,
-      0 < (ProbComp.eval (mask value) true).toReal →
-        maskMass ≤ (ProbComp.eval (mask value) true).toReal)
+      0 < Pr[mask value] → maskMass ≤ Pr[mask value])
     (pair : β × Bool) (hpair : pair ∈ (ProbComp.eval
       (maskedSample source observe truth mask)).support) :
     sourceMass * (maskMass / 2) ≤
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Masking.lean b/Complexity/Crypto/Computational/Pseudoentropy/Masking.lean
index abb463afb..a4b81860c 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/Masking.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/Masking.lean
@@ -11,6 +11,7 @@ public import Complexity.Probability.Entropy
 public import Complexity.Crypto.Computational.Prediction
 public import Complexity.Crypto.Computational.Hybrid.Sequence
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Sampling
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -57,8 +58,6 @@ namespace Cslib.Crypto.Pseudoentropy
 
 open Probability Probability.PMF BitString Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- Replace a label by a fresh fair bit when the supplied mask accepts. -/
 noncomputable def maskBit (mask : ProbComp Bool) (truth : Bool) : ProbComp Bool := do
   let replace ← mask
@@ -83,8 +82,7 @@ theorem eval_maskBit (mask : ProbComp Bool) (truth : Bool) :
 /-- The original label remains with probability `1 - maskProbability / 2`. -/
 theorem eval_maskBit_apply (mask : ProbComp Bool) (truth bit : Bool) :
     (ProbComp.eval (maskBit mask truth) bit).toReal =
-      if bit = truth then 1 - (ProbComp.eval mask true).toReal / 2
-      else (ProbComp.eval mask true).toReal / 2 := by
+      if bit = truth then 1 - Pr[mask] / 2 else Pr[mask] / 2 := by
   have hmass := toReal_true_add_toReal_false (ProbComp.eval mask)
   rw [eval_maskBit, bind_apply_toReal]
   cases truth <;> cases bit <;>
@@ -92,7 +90,7 @@ theorem eval_maskBit_apply (mask : ProbComp Bool) (truth bit : Bool) :
 
 /-- A fresh replacement contributes one bit of conditional randomness whenever the mask accepts. -/
 theorem entropy_maskBit_ge (mask : ProbComp Bool) (truth : Bool) :
-    (ProbComp.eval mask true).toReal ≤ entropy (ProbComp.eval (maskBit mask truth)) := by
+    Pr[mask] ≤ entropy (ProbComp.eval (maskBit mask truth)) := by
   rw [eval_maskBit]
   have h := sum_mul_entropy_le_entropy_bind (ProbComp.eval mask)
     (fun replace => if replace then PMF.uniformOfFintype Bool else PMF.pure truth)
@@ -110,7 +108,7 @@ theorem eval_maskedSample {α β : Type} (source : ProbComp α)
 in conditional label entropy. In particular, mask probabilities may depend on hidden labels. -/
 theorem maskedSample_entropy_ge {α β : Type} [Fintype α] [Finite β] (source : ProbComp α)
     (observe : α → β) (truth : α → Bool) (mask : α → ProbComp Bool) :
-    (∑ x, (ProbComp.eval source x).toReal * (ProbComp.eval (mask x) true).toReal) ≤
+    (∑ x, (ProbComp.eval source x).toReal * Pr[mask x]) ≤
       conditionalEntropy (ProbComp.eval (maskedSample source observe truth mask)) := by
   rw [eval_maskedSample]
   exact (Finset.sum_le_sum (fun x _ => mul_le_mul_of_nonneg_left
@@ -135,9 +133,9 @@ mask probability. The predictor itself receives only the test, not the mask or h
 theorem maskBit_prediction_gap (test : Bool → ProbComp Bool) (mask : ProbComp Bool)
     (truth : Bool) :
     Pr[test truth] - Pr[maskBit mask truth >>= test] =
-      (ProbComp.eval mask true).toReal *
+      Pr[mask] *
         (Pr[(fun guess => guess == truth) <$> bitPredictor test] - 1 / 2) := by
-  rw [Game.coe_succProbability_eval_bind, bitPredictor_bias]
+  rw [ProbComp.probability_bind, bitPredictor_bias]
   simp only [Fintype.sum_bool, eval_maskBit_apply]
   cases truth <;> norm_num <;> ring
 
@@ -148,12 +146,11 @@ theorem maskedSample_prediction_gap {α β : Type} [Fintype α] (source : ProbCo
     (test : β → Bool → ProbComp Bool) :
     Pr[source >>= fun x => test (observe x) (truth x)] -
         Pr[maskedSample source observe truth mask >>= fun pair => test pair.1 pair.2] =
-      ∑ x, (ProbComp.eval source x).toReal * (ProbComp.eval (mask x) true).toReal *
+      ∑ x, (ProbComp.eval source x).toReal * Pr[mask x] *
         (Pr[(fun guess => guess == truth x) <$> bitPredictor (test (observe x))] -
           1 / 2) := by
   simp only [maskedSample, bind_assoc, bind_map_left]
-  rw [Game.coe_succProbability_eval_bind, Game.coe_succProbability_eval_bind,
-    ← Finset.sum_sub_distrib]
+  rw [ProbComp.probability_bind, ProbComp.probability_bind, ← Finset.sum_sub_distrib]
   simp only [← mul_sub, maskBit_prediction_gap, mul_assoc]
 
 /-- A certified mask and an efficiently supplied label give a strict PPT randomized label. -/
@@ -201,10 +198,13 @@ theorem maskedSequence_prediction_gap {α β : Type} [Fintype α] (source : Prob
       Pr[OracleComp.replicate count (maskedSample source observe truth mask)
         >>= test] =
       (dyadicSize count : ℝ) * ∑ x,
-        (ProbComp.eval source x).toReal * (ProbComp.eval (mask x) true).toReal *
+        (ProbComp.eval source x).toReal * Pr[mask x] *
           (Pr[(fun guess => guess == truth x) <$>
             maskedSequencePredictor source observe truth mask count test (observe x)] - 1 / 2) := by
-  rw [sequenceTest_gap]
+  have hgap := sequenceTest_gap (maskedSample source observe truth mask)
+    ((fun x => (observe x, truth x)) <$> source) count test
+  simp only [Game.coe_succProbability] at hgap
+  rw [hgap]
   unfold maskedSequencePredictor
   congr 1
   simpa only [bind_map_left] using maskedSample_prediction_gap source observe truth mask
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean
index 40d016820..131004c1d 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Pseudoentropy.WordReduction
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Crypto.Computational.OneWay.Normalize
 import Complexity.Computability.Probabilistic.CoinTape
 import Complexity.Crypto.Negligible.Basic
@@ -44,8 +45,6 @@ namespace Cslib.Crypto.Pseudoentropy.HashPair
 open Probability BitString GoldreichLevin Filter Turing.MultiTapeTM
 open scoped NNReal
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- A single cubic precision suffices for all sufficiently large dimensions. -/
 theorem precision_three_ge {n : ℕ} (hn : 8 ≤ n) :
     8 * hashCount n ≤ precision 3 n := by
@@ -78,7 +77,8 @@ theorem eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : One
   have hsmall := hloss.eventually_le_inv_polynomial
     hashCount_polynomiallyBounded (fun n => Nat.pos_of_ne_zero (NeZero.ne (hashCount n)))
   filter_upwards [hsmall, eventually_ge_atTop 8] with n hsmall hn
-  simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_ofNat, NNReal.coe_natCast] at hsmall
+  simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_ofNat, NNReal.coe_natCast,
+    Game.coe_succProbability] at hsmall
   have h := word_prediction_entropy_le f (finiteFunction n) (encodeImage n)
     (hencode n) (hlength n) adversary evaluate c d (fun n input => hrealize (n, input))
     3 (precision_three_ge hn)
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/SequenceLearner.lean b/Complexity/Crypto/Computational/Pseudoentropy/SequenceLearner.lean
index e88caf04a..98d37fb78 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/SequenceLearner.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/SequenceLearner.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Crypto.Computational.Hybrid.SavedPrediction
 public import Complexity.Crypto.Computational.Pseudoentropy.Learning
 public import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Training
+import Complexity.Languages.Probabilistic.Notation
 import Complexity.Tactic.PPT
 
 /-!
@@ -56,8 +57,6 @@ open Probability Probability.PMF BitString Boosting Turing.MultiTapeTM
 
 open scoped NNReal
 
-local notation "Pr[" p "]" => ENNReal.toReal (ProbComp.eval p true)
-
 /-- Configure the loop at the learner's required correlation. The density denominator and
 inverse distinguishing gap determine the rate; the supplied bound covers signed descriptions. -/
 def parameters (confidence numerator densityBound inverseGap codeBound : ℕ) : Parameters :=
@@ -473,8 +472,7 @@ theorem predict_extracted_error {Seed Output : Type}
       (fun x => mask (signedPredict evaluate) params state (observe x, truth x)))
     count seed hash test ideal (hclose state hdense)
   have hgap' := (le_sub_iff_add_le.mpr hdistinguish).trans h
-  simpa only [Game.coe_advantage, Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
-    using hgap'
+  simpa only [Game.coe_advantage, Game.coe_succProbability] using hgap'
 
 end Correctness
 
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean
index 99db2b706..443ede76a 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean
@@ -11,6 +11,7 @@ public import Complexity.Crypto.Computational.Pseudoentropy.HashReduction
 public import Complexity.Crypto.Computational.Pseudoentropy.Basic
 public import Complexity.Crypto.Computational.GoldreichLevin.WordDecoder
 public import Complexity.Crypto.Computational.OneWay
+import Complexity.Languages.Probabilistic.Notation
 
 import Complexity.Computability.Probabilistic.UniformNat
 import Complexity.Tactic.PPT
@@ -54,8 +55,6 @@ namespace Cslib.Crypto.Pseudoentropy.HashPair
 
 open Probability BitString GoldreichLevin Turing.MultiTapeTM
 
-local notation "Pr[" p "]" => (Game.succProbability (ProbComp.eval p) : ℝ)
-
 /-- One polynomial tape budget covers all digest lengths and parity queries for an image. -/
 def coinBudget (c d n imageLength : ℕ) : ℕ :=
   c * (2 * imageLength + 2 * (hashCount n * n) + 4 * hashCount n + 3 * n + 8) ^ d
@@ -281,7 +280,7 @@ theorem word_prediction_entropy_le {n imageLength : ℕ} {Image : Type*}
       1 - 2 / (hashCount n : ℝ) + 128 * (dyadicSize (16 * hashCount n) : ℝ) ^ 2 *
         Pr[inversionGame f (wordInverter f evaluate c d degree) n] := by
   classical
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal,
+  simp only [
     eval_predictionGame f finiteFunction encodeImage hf hlength adversary evaluate c d hrealize,
     eval_wordInversionGame f finiteFunction encodeImage hf hlength evaluate c d degree]
   exact matrixPrediction_entropy_le_of_coins finiteFunction (hashCount_ge n) _ _ _ hp
diff --git a/Complexity/Crypto/Computational/UniformChoice.lean b/Complexity/Crypto/Computational/UniformChoice.lean
index 9aa57e9fc..18152f2ad 100644
--- a/Complexity/Crypto/Computational/UniformChoice.lean
+++ b/Complexity/Crypto/Computational/UniformChoice.lean
@@ -111,7 +111,7 @@ theorem advantage_eq (bound : ℕ) (real ideal : ProbComp (List Bool))
   apply NNReal.eq
   rw [Game.coe_advantage, eval_bind_test, eval_bind_test]
   simp only [PMF.monad_bind_eq_bind, Game.succProbability_uniform,
-    NNReal.coe_div, NNReal.coe_sum, NNReal.coe_pow, NNReal.coe_natCast,
+    NNReal.coe_div, NNReal.coe_sum, NNReal.coe_pow, NNReal.coe_natCast, Game.coe_succProbability,
     Fintype.card_fin, ← sub_div, ← Finset.sum_sub_distrib, hgap]
   exact abs_of_nonneg (div_nonneg (Finset.sum_nonneg (fun _ _ => sq_nonneg _))
     (Nat.cast_nonneg _))
diff --git a/Complexity/Crypto/Game.lean b/Complexity/Crypto/Game.lean
index 8b90073dd..e6b415bf7 100644
--- a/Complexity/Crypto/Game.lean
+++ b/Complexity/Crypto/Game.lean
@@ -233,5 +233,11 @@ theorem Indistinguishable.of_reduction {SourceAdversary TargetAdversary : Type*}
   have hsource := h _ (hadmissible adversary ha)
   exact negligible_of_le (by fun_prop (disch := assumption)) hbound
 
+-- upstream: candidate
+
+/-- As a real number, the success probability is the real-valued probability of `true`. -/
+@[simp] theorem coe_succProbability (game : Game) :
+    (succProbability game : ℝ) = (game true).toReal := rfl
+
 end Game
 end Cslib.Crypto
diff --git a/Complexity/Languages/Probabilistic/Notation.lean b/Complexity/Languages/Probabilistic/Notation.lean
new file mode 100644
index 000000000..5aa0b8d65
--- /dev/null
+++ b/Complexity/Languages/Probabilistic/Notation.lean
@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Languages.Probabilistic.Basic
+
+/-!
+# Probability notation for Boolean experiments
+
+`Pr[e]` is the probability, as a real number, that the Boolean experiment `e` returns `true`.
+The experiment is either a program `e : ProbComp Bool`, for which `Pr[e]` is
+`(ProbComp.eval e true).toReal`, or a distribution `e : PMF Bool`, for which it is
+`(e true).toReal`. The notation adds no constant: `Pr[e]` elaborates to exactly these terms, so
+every lemma about `ENNReal.toReal`, `PMF` and `ProbComp.eval` applies to it, and the program form
+is the distribution form at `ProbComp.eval e`. The elaborator tries `ProbComp Bool` first, so a
+`do` block or a chain of binds is read as a program, and falls back to `PMF Bool`.
+
+Probabilities are real numbers so that advantages and biases are signed differences, as in
+`|Pr[real] - Pr[ideal]|` or `Pr[game] - 1 / 2`. Nonnegativity is `ENNReal.toReal_nonneg`.
+
+Events are final returns. The probability that a sample of `μ : PMF α` lies in a set `s` is
+`Pr[(fun x => decide (x ∈ s)) <$> μ]`, and the probability of an outcome `a` is
+`Pr[(· == a) <$> μ]`; these are `(μ.toOuterMeasure s).toReal` and `(μ a).toReal`. A Boolean game,
+a set event and a single outcome therefore share one form.
+
+The notation is scoped: `open Cslib.Probability` enables it, as does `open Probability` inside the
+namespace `Cslib`. It then also prints both forms back as `Pr[e]`.
+
+## Main definitions
+
+* `Pr[e]`: the probability that the Boolean experiment `e` returns `true`, as a real number.
+
+## Main results
+
+* `Cslib.Probability.PMF.toReal_apply_le_one`: a probability is at most one.
+* `Cslib.ProbComp.probability_pure`: a program that returns a constant.
+* `Cslib.ProbComp.probability_bind`: after a finite random choice, the probability is the
+  average over the choice.
+* `Cslib.Probability.PMF.probability_map_decide_mem`,
+  `Cslib.ProbComp.probability_map_decide_mem`: set events.
+* `Cslib.Probability.PMF.probability_map_beq`, `Cslib.ProbComp.probability_map_beq`: single
+  outcomes.
+-/
+
+public section
+
+namespace Cslib.Probability
+
+/-- `Pr[e]` is the probability, as a real number, that the Boolean experiment `e` returns
+`true`: `(ProbComp.eval e true).toReal` for a program `e : ProbComp Bool`, and `(e true).toReal`
+for a distribution `e : PMF Bool`. -/
+scoped syntax (name := probabilityTrue) "Pr[" term "]" : term
+
+open Lean Elab Term in
+/-- Elaborate `Pr[e]` as `(ProbComp.eval e true).toReal`, with `e` elaborated as a
+`ProbComp Bool`; if that fails, as `(e true).toReal` with `e : PMF Bool`. -/
+@[scoped term_elab probabilityTrue]
+meta def elabProbabilityTrue : TermElab := fun stx expectedType? => do
+  let `(Pr[$e]) := stx | throwUnsupportedSyntax
+  let program ← Term.observing <| withoutErrToSorry <| elabTerm
+    (← `(ENNReal.toReal (Cslib.ProbComp.eval ($e : Cslib.ProbComp Bool) true))) expectedType?
+  let .error programError _ := program | applyResult program
+  let distribution ← Term.observing <| withoutErrToSorry <| elabTerm
+    (← `(ENNReal.toReal (($e : _root_.PMF Bool) true))) expectedType?
+  let .error distributionError _ := distribution | applyResult distribution
+  if (← programError.toMessageData.toString) == (← distributionError.toMessageData.toString) then
+    return ← applyResult program
+  throwError "`Pr[e]` needs a Boolean experiment `e : ProbComp Bool` or `e : PMF Bool`.\
+    \nAs a `ProbComp Bool`:{indentD programError.toMessageData}\
+    \nAs a `PMF Bool`:{indentD distributionError.toMessageData}"
+
+open Lean Meta PrettyPrinter Delaborator SubExpr in
+/-- Print `(ProbComp.eval e true).toReal` as `Pr[e]`, and `(μ true).toReal` for `μ : PMF Bool`
+as `Pr[μ]`. Unlike an unexpander, it checks that the argument is a `PMF Bool`. -/
+@[scoped delab app.ENNReal.toReal]
+meta def delabProbabilityTrue : Delab := whenPPOption getPPNotation do
+  let e ← getExpr
+  guard <| e.isAppOfArity ``ENNReal.toReal 1
+  let mass := e.appArg!
+  guard <| mass.isAppOfArity ``DFunLike.coe 6
+  let args := mass.getAppArgs
+  guard <| args[5]!.isConstOf ``Bool.true
+  let law ← whnfR args[0]!
+  guard <| law.isAppOfArity ``PMF 1 && law.appArg!.isConstOf ``Bool
+  if args[4]!.isAppOfArity ``Cslib.ProbComp.eval 2 then
+    let program ← withAppArg <| withNaryArg 4 <| withAppArg delab
+    `(Pr[$program])
+  else
+    let distribution ← withAppArg <| withNaryArg 4 delab
+    `(Pr[$distribution])
+
+namespace PMF
+
+/-- A probability is at most one; in particular `Pr[e] ≤ 1` for every Boolean experiment. -/
+theorem toReal_apply_le_one {α : Type*} (μ : _root_.PMF α) (a : α) : (μ a).toReal ≤ 1 :=
+  ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using μ.coe_le_one a)
+
+variable {α : Type}
+
+/-- The probability that a sample lies in a set is the probability that testing membership
+returns `true`. -/
+theorem probability_map_decide_mem (μ : _root_.PMF α) (s : Set α) [DecidablePred (· ∈ s)] :
+    Pr[(fun x => decide (x ∈ s)) <$> μ] = (μ.toOuterMeasure s).toReal := by
+  rw [_root_.PMF.monad_map_eq_map, ← _root_.PMF.toOuterMeasure_apply_singleton,
+    _root_.PMF.toOuterMeasure_map_apply]
+  congr 2
+  ext x
+  simp
+
+/-- The probability of an outcome is the probability that comparing with it returns `true`. -/
+theorem probability_map_beq [BEq α] [LawfulBEq α] (μ : _root_.PMF α) (a : α) :
+    Pr[(· == a) <$> μ] = (μ a).toReal := by
+  rw [_root_.PMF.monad_map_eq_map, ← _root_.PMF.toOuterMeasure_apply_singleton,
+    _root_.PMF.toOuterMeasure_map_apply, ← _root_.PMF.toOuterMeasure_apply_singleton]
+  congr 2
+  ext x
+  simp
+
+end PMF
+
+end Cslib.Probability
+
+namespace Cslib.ProbComp
+
+open Probability
+
+variable {α : Type}
+
+/-- A program that returns `b` succeeds with probability one if `b` is `true` and zero
+otherwise. -/
+theorem probability_pure (b : Bool) : Pr[pure b] = if b then 1 else 0 := by
+  cases b <;> simp
+
+/-- After a finite random choice, the probability of success is the average of the
+probabilities of success of the continuations. -/
+theorem probability_bind [Fintype α] (source : ProbComp α) (next : α → ProbComp Bool) :
+    Pr[source >>= next] = ∑ a, (eval source a).toReal * Pr[next a] := by
+  rw [eval_bind, PMF.bind_apply_toReal]
+
+/-- The probability that a program's output lies in a set is the probability that testing
+membership returns `true`. -/
+theorem probability_map_decide_mem (program : ProbComp α) (s : Set α) [DecidablePred (· ∈ s)] :
+    Pr[(fun x => decide (x ∈ s)) <$> program] = ((eval program).toOuterMeasure s).toReal := by
+  rw [eval_map, ← _root_.PMF.monad_map_eq_map, PMF.probability_map_decide_mem]
+
+/-- The probability of an output is the probability that comparing with it returns `true`. -/
+theorem probability_map_beq [BEq α] [LawfulBEq α] (program : ProbComp α) (a : α) :
+    Pr[(· == a) <$> program] = (eval program a).toReal := by
+  rw [eval_map, ← _root_.PMF.monad_map_eq_map, PMF.probability_map_beq]
+
+end Cslib.ProbComp
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index b78011bef..0494a2b8d 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -339,6 +339,7 @@ import ComplexityTests.PostTuringMachine
 import ComplexityTests.Presample
 import ComplexityTests.ProbabilisticComposition
 import ComplexityTests.ProbabilisticSampling
+import ComplexityTests.ProbabilityNotation
 import ComplexityTests.ProbabilityToolkit
 import ComplexityTests.ProbabilityToolkit2
 import ComplexityTests.ProbabilityToolkit3
diff --git a/ComplexityTests/Axioms.lean b/ComplexityTests/Axioms.lean
index 635062c28..d73bf4515 100644
--- a/ComplexityTests/Axioms.lean
+++ b/ComplexityTests/Axioms.lean
@@ -7892,13 +7892,6 @@ info: 'Turing.MultiTapeTM.ComputableTidilyInPolyTime.findGreatest' depends on ax
 #guard_msgs (whitespace := lax) in
 #print axioms Turing.MultiTapeTM.ComputableTidilyInPolyTime.findGreatest
 
-/--
-info: 'Cslib.Crypto.Game.coe_succProbability_eval_bind' depends on axioms:
-[propext, Classical.choice, Quot.sound]
--/
-#guard_msgs (whitespace := lax) in
-#print axioms Cslib.Crypto.Game.coe_succProbability_eval_bind
-
 /--
 info: 'Cslib.Crypto.Negligible.sqrt' depends on axioms:
 [propext, Classical.choice, Quot.sound]
diff --git a/ComplexityTests/DenseMask.lean b/ComplexityTests/DenseMask.lean
index 83f3c9561..01f53023e 100644
--- a/ComplexityTests/DenseMask.lean
+++ b/ComplexityTests/DenseMask.lean
@@ -79,8 +79,7 @@ private theorem fairPair_gap : fairPair.HasGap (fun _ => 0) := by
       (fun guess => (uniformOfFintype Bool).map (fun bit => guess == bit)) = _
     simp only [hbit, PMF.bind_const]
   rw [hgame, fairPair_entropy]
-  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal]
-  norm_num [Game.succProbability, PMF.uniformOfFintype_apply]
+  norm_num [PMF.uniformOfFintype_apply]
 
 private noncomputable def saved : fairPair.SeedRealization :=
   Classical.choice fairPair.exists_seedRealization
diff --git a/ComplexityTests/ProbabilityNotation.lean b/ComplexityTests/ProbabilityNotation.lean
new file mode 100644
index 000000000..fa0fbb4d5
--- /dev/null
+++ b/ComplexityTests/ProbabilityNotation.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Languages.Probabilistic.Notation
+
+/-! The scoped notation `Pr[e]`: its two elaborated forms, `do` blocks, display and API. -/
+
+namespace ComplexityTests.ProbabilityNotation
+
+open Cslib Probability
+
+variable (program : ProbComp Bool) (next : Fin 2 → ProbComp Bool) (μ : PMF Bool)
+  (mass : Bool → ENNReal)
+
+section Elaboration
+
+-- `#guard_expr` checks syntactic equality of elaborated terms and is silent when it succeeds,
+-- which the `#`-command linter would otherwise report.
+set_option linter.hashCommand false
+
+-- A program elaborates to exactly the real probability of `true` under its distribution, and a
+-- distribution to its own real probability of `true`. No new constant appears.
+#guard_expr Pr[program] =ₛ ENNReal.toReal (ProbComp.eval program true)
+#guard_expr Pr[μ] =ₛ ENNReal.toReal (μ true)
+
+-- A `do` block or a chain of binds is read as a program, not as a distribution.
+#guard_expr Pr[do let b ← ProbComp.uniform Bool; return !b] =ₛ
+  ENNReal.toReal (ProbComp.eval (do let b ← ProbComp.uniform Bool; return !b) true)
+#guard_expr Pr[ProbComp.uniform (Fin 2) >>= next] =ₛ
+  ENNReal.toReal (ProbComp.eval (ProbComp.uniform (Fin 2) >>= next) true)
+
+end Elaboration
+
+-- Both forms print back as `Pr[e]`; other masses of `true` and other outcomes do not.
+/-- info: Pr[program] : ℝ -/
+#guard_msgs in
+#check ENNReal.toReal (ProbComp.eval program true)
+/-- info: Pr[μ] : ℝ -/
+#guard_msgs in
+#check ENNReal.toReal (μ true)
+/-- info: (mass true).toReal : ℝ -/
+#guard_msgs in
+#check ENNReal.toReal (mass true)
+/-- info: (program.eval false).toReal : ℝ -/
+#guard_msgs in
+#check ENNReal.toReal (ProbComp.eval program false)
+
+-- A fair coin, through the single-outcome form.
+example : Pr[(· == true) <$> ProbComp.uniform Bool] = 1 / 2 := by
+  rw [ProbComp.probability_map_beq, ProbComp.eval_uniform, PMF.uniformOfFintype_apply]
+  simp
+
+-- A set event of a distribution.
+example (ν : PMF (Fin 3)) : Pr[(fun x => decide (x ∈ ({0} : Set (Fin 3)))) <$> ν] =
+    (ν 0).toReal := by
+  rw [PMF.probability_map_decide_mem, PMF.toOuterMeasure_apply_singleton]
+
+-- The finite-average bind law and the bounds.
+example : Pr[ProbComp.uniform (Fin 2) >>= next] = (Pr[next 0] + Pr[next 1]) / 2 := by
+  rw [ProbComp.probability_bind]
+  simp [Fin.sum_univ_two, PMF.uniformOfFintype_apply]
+  ring
+
+example : 0 ≤ Pr[program] ∧ Pr[program] ≤ 1 :=
+  ⟨ENNReal.toReal_nonneg, PMF.toReal_apply_le_one _ _⟩
+
+example : Pr[pure true] = 1 := by
+  rw [ProbComp.probability_pure]
+  rfl
+
+end ComplexityTests.ProbabilityNotation
diff --git a/ComplexityTests/PseudoentropyMasking.lean b/ComplexityTests/PseudoentropyMasking.lean
index 8dcb1a67e..51123bbad 100644
--- a/ComplexityTests/PseudoentropyMasking.lean
+++ b/ComplexityTests/PseudoentropyMasking.lean
@@ -78,7 +78,7 @@ example : (Game.succProbability (ProbComp.eval
     Game.succProbability, PMF.uniformOfFintype_apply, ProbComp.eval_bind,
     bind_apply_toReal, Fintype.sum_bool, ProbComp.eval_pure, PMF.pure_apply,
     ENNReal.toNNReal_ofNat] at h
-  dsimp only [Game.succProbability]
+  rw [Game.coe_succProbability]
   linarith
 
 -- All progress inequalities can hold at equality, including the exact four-round clock.