diff --git a/Complexity/Crypto/Computational/Commitment.lean b/Complexity/Crypto/Computational/Commitment.lean
index d6c07c4ee4..4126e44533 100644
--- a/Complexity/Crypto/Computational/Commitment.lean
+++ b/Complexity/Crypto/Computational/Commitment.lean
@@ -228,7 +228,7 @@ structure CommitmentReceiver.IsPPT (receiver : CommitmentReceiver) : Prop where
   /-- The second stage is strict PPT on `(n, state, c)`. -/
   guess :
     IsPPTOn (encPair encUnary (encPair encBits encBits)) encBool
-      (fun p => receiver.guess p.1 p.2.1 p.2.2)
+      (fun ⟨n, state, c⟩ => receiver.guess n state c)
 
 /-- The two-stage commitment-hiding experiment against a stateful receiver `receiver` with
 auxiliary input `aux` and hidden bit selector `bit : Bool` at security parameter `n`.
@@ -239,19 +239,20 @@ noncomputable def commitmentHidingGame (commit : List Bool → Bool → List Boo
     (receiver : CommitmentReceiver) (aux : List Bool) (bit : Bool) (n : ℕ) : ProbComp Bool := do
   let choice ← receiver.choose n aux
   let seed ← BitString.sampleList n
-  receiver.guess n choice.2
-    (commit choice.1.1 (if bit then choice.1.2.2 else choice.1.2.1) seed)
+  let ((r, b₀, b₁), state) := choice
+  receiver.guess n state
+    (commit r (if bit then b₁ else b₀) seed)
 
 /-- The commitment-hiding experiment runs in strict PPT on `(n, aux, bit)` whenever `commit` is
 computable in plain polynomial time and `receiver` is strict PPT. -/
 theorem isPPTOn_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT) :
     IsPPTOn (encPair encUnary (encPair encBits encBool)) encBool
-      (fun p => commitmentHidingGame commit receiver p.2.1 p.2.2 p.1) := by
+      (fun ⟨n, aux, bit⟩ => commitmentHidingGame commit receiver aux bit n) := by
   have hcommit_tidy := hcommit.tidy
   have hchoose := hR.choose
   have hguess := hR.guess
@@ -263,7 +264,7 @@ indexed family on `(n, aux)`. -/
 theorem isPPT_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT) (bit : Bool) :
     IsPPT encBool (fun n aux => commitmentHidingGame commit receiver aux bit n) := by
@@ -278,7 +279,7 @@ in the unary security parameter `n`. -/
 theorem isPPTOn_commitmentHidingGame_aux {commit : List Bool → Bool → List Bool → List Bool}
     {receiver : CommitmentReceiver} {aux : ℕ → List Bool}
     (hcommit : ComputableInPolyTime
-      (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+      (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits)
     (hR : receiver.IsPPT)
     (haux : ComputableInPolyTime aux encUnary encBits) (bit : Bool) :
@@ -372,8 +373,9 @@ noncomputable def naorReceiverDistinguisher (receiver : CommitmentReceiver)
     (aux : ℕ → List Bool) (bit : Bool) : Distinguisher :=
   fun n pad => do
     let choice ← receiver.choose n (aux n)
-    receiver.guess n choice.2
-      (naorCommit id choice.1.1 (if bit then choice.1.2.2 else choice.1.2.1) pad)
+    let ((r, b₀, b₁), state) := choice
+    receiver.guess n state
+      (naorCommit id r (if bit then b₁ else b₀) pad)
 
 /-- `naorReceiverDistinguisher receiver aux bit` is a strict PPT distinguisher whenever `receiver`
 is strict PPT and `aux` is computable in plain polynomial time. -/
@@ -1148,13 +1150,12 @@ structure BitCommitmentScheme where
   polyTime_commitLength : ComputableInPolyTime commitLength encUnary encUnary
   /-- `commit` is computable in plain polynomial time. -/
   polyTime_commit :
-    ComputableInPolyTime (fun p : List Bool × Bool × List Bool => commit p.1 p.2.1 p.2.2)
+    ComputableInPolyTime (fun ⟨r, b, seed⟩ => commit r b seed)
       (encPair encBits (encPair encBool encBits)) encBits
   /-- `verify` is computable in plain polynomial time. -/
   polyTime_verify :
     ComputableInPolyTime
-      (fun p : ℕ × List Bool × List Bool × Bool × List Bool =>
-        verify p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2)
+      (fun ⟨n, r, c, b, seed⟩ => verify n r c b seed)
       (encPair encUnary (encPair encBits (encPair encBits (encPair encBool encBits)))) encBool
   /-- Honest commitments have length `commitLength n` when `seed.length = n`. -/
   length_commit : ∀ (n : ℕ) (r : List Bool) (b : Bool) (seed : List Bool),
diff --git a/Complexity/Crypto/Computational/DiffieHellman.lean b/Complexity/Crypto/Computational/DiffieHellman.lean
index 2f8a35c452..bc7f922239 100644
--- a/Complexity/Crypto/Computational/DiffieHellman.lean
+++ b/Complexity/Crypto/Computational/DiffieHellman.lean
@@ -160,8 +160,9 @@ def CDH (setup : ℕ → PMF F.Desc) : Prop :=
 to obtain a candidate exponent `a` and multiplying `encode (β • g)` by `a`. -/
 def dlToCDHAdversary (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool))
     (n : ℕ) (input : F.Desc × List Bool × List Bool) : ProbComp (List Bool) := do
-  let guess ← adversary n (input.1, input.2.1)
-  return F.smul (input.1, ofBits guess, input.2.2)
+  let (d, u, v) := input
+  let guess ← adversary n (d, u)
+  return F.smul (d, ofBits guess, v)
 
 /-- Whenever the discrete-logarithm adversary recovers `α`, `dlToCDHAdversary` outputs the valid
 Diffie–Hellman shared element `encode ((α * β) • g)`. -/
@@ -248,8 +249,9 @@ equals the challenge third element. -/
 def cdhToDDHDistinguisher
     (adversary : ℕ → F.Desc × List Bool × List Bool → ProbComp (List Bool))
     (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := do
-  let guess ← adversary n (input.1, input.2.1, input.2.2.1)
-  return decide (guess = input.2.2.2)
+  let (d, u, v, w) := input
+  let guess ← adversary n (d, u, v)
+  return decide (guess = w)
 
 /-- In the real DDH game, `cdhToDDHDistinguisher` simulates the CDH game exactly. -/
 @[simp] theorem ddhRealGame_cdhToDDHDistinguisher (setup : ℕ → PMF F.Desc)
@@ -529,13 +531,7 @@ natural-number exponents `r, s₁, s₂ : ℕ`, evaluate the encoded tuple corre
 def encodeDDHRerandomize
     (input : F.Desc × (List Bool × List Bool × List Bool) × ℕ × ℕ × ℕ) :
     List Bool × List Bool × List Bool :=
-  let d := input.1
-  let u := input.2.1.1
-  let v := input.2.1.2.1
-  let w := input.2.1.2.2
-  let r := input.2.2.1
-  let s₁ := input.2.2.2.1
-  let s₂ := input.2.2.2.2
+  let (d, (u, v, w), r, s₁, s₂) := input
   let g := F.encode d (F.generator d)
   (F.add (d, F.smul (d, r, u), F.smul (d, s₁, g)),
     F.add (d, v, F.smul (d, s₂, g)),
@@ -548,9 +544,9 @@ def encodeDDHRerandomize
 /-- `encodeDDHRerandomize` evaluates `ddhRerandomize` on encoded group elements. -/
 @[simp] theorem encodeDDHRerandomize_encode (d : F.Desc) (u v w : F.Carrier d) (r s₁ s₂ : ℕ) :
     F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r, s₁, s₂) =
-      let t := F.ddhRerandomize d u v w
+      let (u', v', w') := F.ddhRerandomize d u v w
         (r : ZMod (F.order d)) (s₁ : ZMod (F.order d)) (s₂ : ZMod (F.order d))
-      (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2) := by
+      (F.encode d u', F.encode d v', F.encode d w') := by
   simp only [encodeDDHRerandomize, ddhRerandomize, F.smul_encode, F.add_encode, Nat.cast_mul]
 
 /-- Evaluating `encodeDDHRerandomize` at `.val` of exponents in `ZMod (F.order d)` agrees with
@@ -558,8 +554,8 @@ def encodeDDHRerandomize
 theorem encodeDDHRerandomize_val (d : F.Desc) (u v w : F.Carrier d)
     (r s₁ s₂ : ZMod (F.order d)) :
     F.encodeDDHRerandomize (d, (F.encode d u, F.encode d v, F.encode d w), r.val, s₁.val, s₂.val) =
-      let t := F.ddhRerandomize d u v w r s₁ s₂
-      (F.encode d t.1, F.encode d t.2.1, F.encode d t.2.2) := by
+      let (u', v', w') := F.ddhRerandomize d u v w r s₁ s₂
+      (F.encode d u', F.encode d v', F.encode d w') := by
   simp only [encodeDDHRerandomize_encode, ZMod.natCast_zmod_val]
 
 /-- Word-level DDH tuple re-randomization is computable in polynomial time. -/
@@ -765,9 +761,10 @@ noncomputable def ddhRerandomizeGame (setup : ℕ → PMF F.Desc)
   let r ← PMF.uniformOfFintype (ZMod (F.order d))
   let s₁ ← PMF.uniformOfFintype (ZMod (F.order d))
   let s₂ ← PMF.uniformOfFintype (ZMod (F.order d))
+  let (u, v, w) := tuple d
   ProbComp.eval (distinguisher n
     (d, F.encodeDDHRerandomize
-      (d, (F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2),
+      (d, (F.encode d u, F.encode d v, F.encode d w),
         r.val, s₁.val, s₂.val)))
 
 /-- Re-randomizing any family of real DDH tuples `(α d • g, β d • g, (α d * β d) • g)` with
@@ -855,15 +852,15 @@ theorem DDH.ddhRerandomizeGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF
   exact (F.advantage_ddhRerandomizeGame_eq setup α β α' β' γ' distinguisher n hn).le
 
 /-- The worst-case DDH experiment on a fixed tuple family `tuple` (original): draw `d ← setup n`
-and give the encoded tuple `(d, encode (tuple d).1, encode (tuple d).2.1, encode (tuple d).2.2)`
-directly to `distinguisher`. -/
+and give the encoded tuple `(d, encode u, encode v, encode w)` directly to `distinguisher`. -/
 noncomputable def ddhWorstCaseGame (setup : ℕ → PMF F.Desc)
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
     (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool)
     (n : ℕ) : Game := do
   let d ← setup n
+  let (u, v, w) := tuple d
   ProbComp.eval (distinguisher n
-    (d, F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2))
+    (d, F.encode d u, F.encode d v, F.encode d w))
 
 private noncomputable def ddhRerandomizeStep
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
@@ -1110,8 +1107,9 @@ theorem computableInPolyTime_ddhIdealRefTuple :
     (tuple : ∀ d : F.Desc, F.Carrier d × F.Carrier d × F.Carrier d)
     (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) :
     F.ddhWorstCaseGame (fun _ => PMF.pure d) tuple distinguisher n =
+      let (u, v, w) := tuple d
       ProbComp.eval (distinguisher n
-        (d, F.encode d (tuple d).1, F.encode d (tuple d).2.1, F.encode d (tuple d).2.2)) := by
+        (d, F.encode d u, F.encode d v, F.encode d w)) := by
   simp [ddhWorstCaseGame]
 
 /-- **Single-trial real DDH proximity**: on any fixed group `d` and any real DDH triple
diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean
index 5baba3606d..e51e6fdcc7 100644
--- a/Complexity/Crypto/Computational/MAC.lean
+++ b/Complexity/Crypto/Computational/MAC.lean
@@ -311,7 +311,7 @@ noncomputable def signingOracle (M : MACScheme) (sk : List Bool)
 
 Unlike [Boneh and Shoup, Attack Game 6.1 / Definition 6.2][BonehShoup2023], which logs `(msg, tag)`
 pairs and rejects only previously returned pairs, this experiment logs queried messages and rejects
-any previously queried message (`!out.2.contains out.1.1`). The two notions differ for randomized
+any previously queried message (`!out.2.contains msg`). The two notions differ for randomized
 `sign` algorithms, and coincide for deterministic canonical MACs such as `prfMAC`. -/
 noncomputable def eufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
     ProbComp Bool := do
@@ -319,8 +319,9 @@ noncomputable def eufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.signingOracle sk)) (adversary n [])).run []
-  return (out.1.1.length == M.msgLen n) && !out.2.contains out.1.1 &&
-    M.verify sk out.1.1 out.1.2
+  let (msg, tag) := out.1
+  return (msg.length == M.msgLen n) && !out.2.contains msg &&
+    M.verify sk msg tag
 
 /-- Run the complete MAC EUF-CMA experiment on its unary security parameter for any oracle-PPT
 forger. -/
@@ -423,8 +424,9 @@ noncomputable def eufOneTimeGame (M : MACScheme) (adversary : Forger) (n : ℕ)
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.oneTimeSigningOracle sk)) (adversary n [])).run []
-  return (out.1.1.length == M.msgLen n) && !out.2.contains out.1.1 &&
-    M.verify sk out.1.1 out.1.2
+  let (msg, tag) := out.1
+  return (msg.length == M.msgLen n) && !out.2.contains msg &&
+    M.verify sk msg tag
 
 /-- Running an oracle-PPT forger against `oneTimeSigningOracle` is uniformly strict PPT in the
 unary security parameter and secret key. -/
@@ -640,8 +642,9 @@ noncomputable def sufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.signingPairOracle sk)) (adversary n [])).run []
-  return (out.1.1.length == M.msgLen n) && !out.2.contains out.1 &&
-    M.verify sk out.1.1 out.1.2
+  let (msg, tag) := out.1
+  return (msg.length == M.msgLen n) && !out.2.contains out.1 &&
+    M.verify sk msg tag
 
 /-- Running an oracle-PPT forger against `signingPairOracle` is uniformly strict PPT in the unary
 security parameter and secret key. -/
@@ -802,7 +805,7 @@ theorem eval_run_signingOracle_eq_map_fst_signingPairOracle (M : MACScheme)
     prog []).symm
 
 /-- `eufCmaGame` evaluates the same pair-logging execution `signingPairOracle` as `sufCmaGame`,
-checking message freshness `!(out.2.map Prod.fst).contains out.1.1` on the projected message log. -/
+checking message freshness `!(out.2.map Prod.fst).contains msg` on the projected message log. -/
 theorem eval_eufCmaGame_eq_signingPairOracle (M : MACScheme)
     (adversary : Forger) (n : ℕ) :
     ProbComp.eval (M.eufCmaGame adversary n) =
@@ -811,8 +814,9 @@ theorem eval_eufCmaGame_eq_signingPairOracle (M : MACScheme)
         let out ← (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
             (M.signingPairOracle sk)) (adversary n [])).run []
-        return (out.1.1.length == M.msgLen n) && !(out.2.map Prod.fst).contains out.1.1 &&
-          M.verify sk out.1.1 out.1.2) := by
+        let (msg, tag) := out.1
+        return (msg.length == M.msgLen n) && !(out.2.map Prod.fst).contains msg &&
+          M.verify sk msg tag) := by
   simp only [eufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure]
   refine PMF.bind_congr_on_support _ _ _ fun sk _ => ?_
   rw [M.eval_run_signingOracle_eq_map_fst_signingPairOracle sk (adversary n []), PMF.bind_map]
@@ -976,8 +980,9 @@ noncomputable def sufOneTimeGame (M : MACScheme) (adversary : Forger) (n : ℕ)
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.oneTimeSigningPairOracle sk)) (adversary n [])).run []
-  return (out.1.1.length == M.msgLen n) && !out.2.contains out.1 &&
-    M.verify sk out.1.1 out.1.2
+  let (msg, tag) := out.1
+  return (msg.length == M.msgLen n) && !out.2.contains out.1 &&
+    M.verify sk msg tag
 
 /-- Running an oracle-PPT forger against `oneTimeSigningPairOracle` is uniformly strict PPT in the
 unary security parameter and secret key. -/
@@ -1249,7 +1254,7 @@ theorem eval_run_oneTimeSigningOracle_eq_map_fst_oneTimeSigningPairOracle (M : M
     prog []).symm
 
 /-- `eufOneTimeGame` evaluates the same pair-logging execution `oneTimeSigningPairOracle` as
-`sufOneTimeGame`, checking message freshness `!(out.2.map Prod.fst).contains out.1.1` on the
+`sufOneTimeGame`, checking message freshness `!(out.2.map Prod.fst).contains msg` on the
 projected message log. -/
 theorem eval_eufOneTimeGame_eq_oneTimeSigningPairOracle (M : MACScheme)
     (adversary : Forger) (n : ℕ) :
@@ -1259,8 +1264,9 @@ theorem eval_eufOneTimeGame_eq_oneTimeSigningPairOracle (M : MACScheme)
         let out ← (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
             (M.oneTimeSigningPairOracle sk)) (adversary n [])).run []
-        return (out.1.1.length == M.msgLen n) && !(out.2.map Prod.fst).contains out.1.1 &&
-          M.verify sk out.1.1 out.1.2) := by
+        let (msg, tag) := out.1
+        return (msg.length == M.msgLen n) && !(out.2.map Prod.fst).contains msg &&
+          M.verify sk msg tag) := by
   simp only [eufOneTimeGame, ProbComp.eval_bind, ProbComp.eval_pure]
   refine PMF.bind_congr_on_support _ _ _ fun sk _ => ?_
   rw [M.eval_run_oneTimeSigningOracle_eq_map_fst_oneTimeSigningPairOracle sk (adversary n []),
@@ -1624,8 +1630,9 @@ def macToPrfDistinguisher (adversary : Forger) : OracleDistinguisher :=
         (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k)))
         (macLogHandler n))
       (adversary n [])).run []
-    if (out.1.1.length == n) && !out.2.contains out.1.1 then
-      (· == out.1.2) <$> (List.take n <$> ProbOracleComp.query ((), out.1.1))
+    let (msg, tag) := out.1
+    if (msg.length == n) && !out.2.contains msg then
+      (· == tag) <$> (List.take n <$> ProbOracleComp.query ((), msg))
     else
       pure false
 
@@ -2289,7 +2296,7 @@ noncomputable def signingPairOracle (M : NonceMACScheme) (sk : List Bool)
 the adaptive forger on `(n, [])` with oracle access to `M.signingPairOracle sk`, and accept when:
 1. the candidate message has length `M.msgLen n` and the candidate nonce has length `M.nonceLen n`,
 2. all nonces queried during the signing phase are pairwise distinct
-   (`decide (out.2.map (fun e => e.1.2)).Nodup`),
+   (`decide (out.2.map (fun ⟨⟨_, qnonce⟩, _⟩ => qnonce)).Nodup`),
 3. the candidate `((msg, nonce), tag)` triple was never returned by the tagging oracle
    (`!out.2.contains out.1`), and
 4. `M.verify sk msg nonce tag = true`. -/
@@ -2299,23 +2306,25 @@ noncomputable def sufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.signingPairOracle sk)) (adversary n [])).run []
-  return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) &&
-    decide (out.2.map (fun e => e.1.2)).Nodup && !out.2.contains out.1 &&
-    M.verify sk out.1.1.1 out.1.1.2 out.1.2
+  let ((msg, nonce), tag) := out.1
+  return (msg.length == M.msgLen n) && (nonce.length == M.nonceLen n) &&
+    decide (out.2.map (fun ⟨⟨_, qnonce⟩, _⟩ => qnonce)).Nodup && !out.2.contains out.1 &&
+    M.verify sk msg nonce tag
 
 /-- The fresh-message nonce-based MAC EUF-CMA experiment: identical to `sufCmaGame` except that the
-candidate message `out.1.1.1` must never have been queried during the signing phase
-(`!(out.2.map (fun e => e.1.1)).contains out.1.1.1`). -/
+candidate message `msg` must never have been queried during the signing phase
+(`!(out.2.map (fun ⟨⟨qmsg, _⟩, _⟩ => qmsg)).contains msg`). -/
 noncomputable def eufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) :
     ProbComp Bool := do
   let sk ← M.keyGen n
   let out ← (OracleComp.interpret
     (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
       (M.signingPairOracle sk)) (adversary n [])).run []
-  return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) &&
-    decide (out.2.map (fun e => e.1.2)).Nodup &&
-    !(out.2.map (fun e => e.1.1)).contains out.1.1.1 &&
-    M.verify sk out.1.1.1 out.1.1.2 out.1.2
+  let ((msg, nonce), tag) := out.1
+  return (msg.length == M.msgLen n) && (nonce.length == M.nonceLen n) &&
+    decide (out.2.map (fun ⟨⟨_, qnonce⟩, _⟩ => qnonce)).Nodup &&
+    !(out.2.map (fun ⟨⟨qmsg, _⟩, _⟩ => qmsg)).contains msg &&
+    M.verify sk msg nonce tag
 
 /-- Running an oracle-PPT nonce-MAC forger against `signingPairOracle` is uniformly strict PPT in
 the unary security parameter and secret key. -/
@@ -2572,7 +2581,7 @@ private theorem mem_support_signingPairOracle (M : NonceMACScheme) (sk : List Bo
 /-- For any `NonceMACScheme` whose valid tags on `M.msgLen n`-bit messages and `M.nonceLen n`-bit
 nonces under supported secret keys agree with every tag in the support of `M.sign`, strong
 triple-freshness (`!out.2.contains out.1`) in `sufCmaGame` is identical to `(msg, nonce)`-pair
-freshness (`!(out.2.map Prod.fst).contains out.1.1`). -/
+freshness (`!(out.2.map Prod.fst).contains pair`). -/
 theorem eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme)
     (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support →
       ∀ msg, msg.length = M.msgLen n →
@@ -2586,10 +2595,12 @@ theorem eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme)
         let out ← (OracleComp.interpret
           (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k))
             (M.signingPairOracle sk)) (adversary n [])).run []
-        return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) &&
-          decide (out.2.map (fun e => e.1.2)).Nodup &&
-          !(out.2.map Prod.fst).contains out.1.1 &&
-          M.verify sk out.1.1.1 out.1.1.2 out.1.2) := by
+        let (pair, tag) := out.1
+        let (msg, nonce) := pair
+        return (msg.length == M.msgLen n) && (nonce.length == M.nonceLen n) &&
+          decide (out.2.map (fun ⟨⟨_, qnonce⟩, _⟩ => qnonce)).Nodup &&
+          !(out.2.map Prod.fst).contains pair &&
+          M.verify sk msg nonce tag) := by
   simp only [sufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure]
   refine PMF.bind_congr_on_support _ _ _ fun sk hsk => ?_
   refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨⟨msg, nonce⟩, tag⟩, queriedTriples⟩ hout => ?_
diff --git a/Complexity/Crypto/Computational/MerkleTree.lean b/Complexity/Crypto/Computational/MerkleTree.lean
index 65ead06a51..e369572681 100644
--- a/Complexity/Crypto/Computational/MerkleTree.lean
+++ b/Complexity/Crypto/Computational/MerkleTree.lean
@@ -119,13 +119,16 @@ def merkleSibling (p : ℕ) : ℕ :=
 level and position. -/
 def merklePathStep (state : List (List Bool) × ℕ × List (List Bool)) :
     List (List Bool) × ℕ × List (List Bool) :=
-  (merkleParents H k state.1, state.2.1 / 2,
-    state.2.2 ++ [state.1.getD (merkleSibling state.2.1) []])
+  let (level, pos, path) := state
+  (merkleParents H k level, pos / 2,
+    path ++ [level.getD (merkleSibling pos) []])
 
 /-- The authentication path of position `i`: the sibling of each node on the way from leaf `i` up
 to the root, starting at the leaves ([BonehShoup2023], Figure 8.12). -/
 def merklePath (leaves : List (List Bool)) (i : ℕ) : List (List Bool) :=
-  ((merklePathStep H k)^[Nat.clog 2 leaves.length] (merkleLeafLevel H k leaves, i, [])).2.2
+  let (_, _, path) :=
+    (merklePathStep H k)^[Nat.clog 2 leaves.length] (merkleLeafLevel H k leaves, i, [])
+  path
 
 /-! ### Recomputing a root from an opening -/
 
diff --git a/Complexity/Crypto/Computational/MerkleTree/Binding.lean b/Complexity/Crypto/Computational/MerkleTree/Binding.lean
index 5343f1ed68..80d829eff0 100644
--- a/Complexity/Crypto/Computational/MerkleTree/Binding.lean
+++ b/Complexity/Crypto/Computational/MerkleTree/Binding.lean
@@ -259,9 +259,10 @@ variable (H : List Bool → List Bool → List Bool)
 /-- `out` breaks position binding under the key `k`: both openings are accepted at the same
 position of the same root, at the depth of the first path, and their leaves differ. -/
 def merkleBreaksBinding (k : List Bool) (out : MerkleBindingOutput) : Bool :=
-  merkleVerify H k out.2.1.2.length out.1.1 out.1.2 out.2.1.1 out.2.1.2 &&
-    merkleVerify H k out.2.1.2.length out.1.1 out.1.2 out.2.2.1 out.2.2.2 &&
-      out.2.1.1 != out.2.2.1
+  let ((root, i), (leaf₁, path₁), (leaf₂, path₂)) := out
+  merkleVerify H k path₁.length root i leaf₁ path₁ &&
+    merkleVerify H k path₁.length root i leaf₂ path₂ &&
+      leaf₁ != leaf₂
 
 /-- The position-binding experiment ([BonehShoup2023], Attack Game 8.2, for a keyed hash): sample
 a uniform `n`-bit key `k`, run the adversary on `(n, k)`, and accept when its output breaks
@@ -283,7 +284,8 @@ def MerklePositionBinding : Prop :=
 from its two openings with `extractMerkleCollision`. -/
 def merkleCollisionFinder (adversary : MerkleBindingAdversary) : CollisionFinder := fun n k => do
   let out ← adversary n k
-  return extractMerkleCollision H k out.2.1.1 out.2.2.1 out.1.2 out.2.1.2 out.2.2.2
+  let ((_, i), (leaf₁, path₁), (leaf₂, path₂)) := out
+  return extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂
 
 variable {H}
 
@@ -291,9 +293,9 @@ variable {H}
 `extractMerkleCollision` finds two different inputs with the same hash under `k`. -/
 theorem isCollision_of_merkleBreaksBinding {k : List Bool} {out : MerkleBindingOutput}
     (h : merkleBreaksBinding H k out = true) (n : ℕ) :
-    isCollision H (fun _ _ => true) n k
-      (extractMerkleCollision H k out.2.1.1 out.2.2.1 out.1.2 out.2.1.2 out.2.2.2).1
-      (extractMerkleCollision H k out.2.1.1 out.2.2.1 out.1.2 out.2.1.2 out.2.2.2).2 = true := by
+    let ((_, i), (leaf₁, path₁), (leaf₂, path₂)) := out
+    let col := extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂
+    isCollision H (fun _ _ => true) n k col.1 col.2 = true := by
   simp only [merkleBreaksBinding, Bool.and_eq_true, bne_iff_ne, ne_eq] at h
   exact isCollision_of_merkleVerify h.1.1 h.1.2 h.2 n
 
diff --git a/Complexity/Crypto/Computational/ZeroKnowledge.lean b/Complexity/Crypto/Computational/ZeroKnowledge.lean
index a283eb34be..675785157b 100644
--- a/Complexity/Crypto/Computational/ZeroKnowledge.lean
+++ b/Complexity/Crypto/Computational/ZeroKnowledge.lean
@@ -143,10 +143,10 @@ def GenerableZeroKnowledge {α : Type} (enc : α ↪ List Bool)
     (isWitness : α → List Bool → Bool) : Prop :=
   ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool),
     IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) →
+      (fun ⟨n, a, z⟩ => Vstar n a z) →
     ∃ S : ℕ → α → List Bool → ProbComp (List Bool),
       IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧
+        (fun ⟨n, a, z⟩ => S n a z) ∧
       ∀ (a : ℕ → α) (w z : ℕ → List Bool),
         ComputableInPolyTime a encUnary enc →
         ComputableInPolyTime w encUnary encBits →
@@ -172,10 +172,10 @@ def AuxiliaryInputZeroKnowledge {α : Type} (enc : α ↪ List Bool)
     (isWitness : α → List Bool → Bool) : Prop :=
   ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool),
     IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) →
+      (fun ⟨n, a, z⟩ => Vstar n a z) →
     ∃ S : ℕ → α → List Bool → ProbComp (List Bool),
       IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧
+        (fun ⟨n, a, z⟩ => S n a z) ∧
       ∀ (a : ℕ → α) (w z : ℕ → List Bool),
         PolynomiallyBounded (fun n => (enc (a n)).length) →
         PolynomiallyBounded (fun n => (w n).length) →
@@ -183,7 +183,7 @@ def AuxiliaryInputZeroKnowledge {α : Type} (enc : α ↪ List Bool)
         (∀ n, isWitness (a n) (w n) = true) →
         ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool,
           IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-            (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) →
+            (fun ⟨⟨n, a, z⟩, view⟩ => adversary n a z view) →
           Negligible (fun n => Game.advantage
             (distinguishingGame
               (((prover n (a n) (w n)).run (Vstar n (a n) (z n))
@@ -223,10 +223,10 @@ theorem GenerableZeroKnowledge.advantage_negligible {α : Type} {enc : α ↪ Li
     (h : GenerableZeroKnowledge enc prover isWitness)
     {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2)) :
+      (fun ⟨n, a, z⟩ => Vstar n a z)) :
     ∃ S : ℕ → α → List Bool → ProbComp (List Bool),
       IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧
+        (fun ⟨n, a, z⟩ => S n a z) ∧
       ∀ (a : ℕ → α) (w z : ℕ → List Bool),
         ComputableInPolyTime a encUnary enc →
         ComputableInPolyTime w encUnary encBits →
@@ -234,7 +234,7 @@ theorem GenerableZeroKnowledge.advantage_negligible {α : Type} {enc : α ↪ Li
         (∀ n, isWitness (a n) (w n) = true) →
         ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool,
           IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-            (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) →
+            (fun ⟨⟨n, a, z⟩, view⟩ => adversary n a z view) →
           Negligible (fun n => Game.advantage
             (distinguishingGame
               (((prover n (a n) (w n)).run (Vstar n (a n) (z n))
@@ -309,10 +309,10 @@ structure ZeroKnowledgeProof {α : Type} (enc : α ↪ List Bool) (A : Set α) w
   isPPT_interact :
     ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool),
       IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) →
+        (fun ⟨n, a, z⟩ => Vstar n a z) →
       IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits
-        (fun p : ℕ × α × List Bool × List Bool =>
-          interact p.1 p.2.1 p.2.2.1 (Vstar p.1 p.2.1 p.2.2.2))
+        (fun ⟨n, a, w, z⟩ =>
+          interact n a w (Vstar n a z))
   /-- Perfect completeness: for every valid witness `w` of `a`, the honest prover convinces the
   honest verifier with probability `1`. -/
   complete : ∀ n a w, isWitness a w = true → acceptProb (verifier n a) (prover n a w) = 1
@@ -381,16 +381,16 @@ theorem AuxiliaryInputZeroKnowledge.zero_knowledge_const {zk : ZeroKnowledgeProo
     (h : zk.AuxiliaryInputZeroKnowledge)
     {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2)) :
+      (fun ⟨n, a, z⟩ => Vstar n a z)) :
     ∃ S : ℕ → α → List Bool → ProbComp (List Bool),
       IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧
+        (fun ⟨n, a, z⟩ => S n a z) ∧
       ∀ a w (z : ℕ → List Bool),
         zk.isWitness a w = true →
         PolynomiallyBounded (fun n => (z n).length) →
         ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool,
           IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool
-            (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) →
+            (fun ⟨⟨n, a, z⟩, view⟩ => adversary n a z view) →
           Negligible (fun n => Game.advantage
             (distinguishingGame
               (((zk.prover n a w).run (Vstar n a (z n))
@@ -426,10 +426,10 @@ the real interaction output and simulator output are computationally indistingui
 theorem zero_knowledge_const (zk : ZeroKnowledgeProof enc A)
     {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2)) :
+      (fun ⟨n, a, z⟩ => Vstar n a z)) :
     ∃ S : ℕ → α → List Bool → ProbComp (List Bool),
       IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-        (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧
+        (fun ⟨n, a, z⟩ => S n a z) ∧
       ∀ a w (z : ℕ → List Bool),
         zk.isWitness a w = true →
         ComputableInPolyTime z encUnary encBits →