diff --git a/Complexity/Crypto/Computational/GMW/PolyTime.lean b/Complexity/Crypto/Computational/GMW/PolyTime.lean
index 1fbf5a5f7d..e2d8525377 100644
--- a/Complexity/Crypto/Computational/GMW/PolyTime.lean
+++ b/Complexity/Crypto/Computational/GMW/PolyTime.lean
@@ -517,7 +517,7 @@ theorem isPPTOn_runTwoRound {α Caller : Type} {enc : α ↪ List Bool} {input :
     {reply1 reply2 : Caller × List Bool → List Bool}
     {bound : Caller → ℕ}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hprep : ComputableInPolyTime prepare input (encPair encUnary (encPair enc encBits)))
     (hr1 : ComputableInPolyTime reply1 (encPair input encBits) encBits)
     (hr2 : ComputableInPolyTime reply2 (encPair input encBits) encBits)
@@ -578,7 +578,7 @@ theorem isPPTOn_runTwoRound_prover {α Caller : Type} {enc : α ↪ List Bool}
     {openFlags bits ch_guess : Caller → List Bool}
     {seeds pads : Caller → List (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hg : ComputableInPolyTime generator encBits encBits)
     (hn : ComputableInPolyTime n input encUnary)
     (hs : ComputableInPolyTime s input encUnary)
@@ -666,11 +666,11 @@ noncomputable def gmwSimWithPads (generator : List Bool → List Bool) (s m : 
     ProbComp (List Bool) := do
   let ch_guess ← BitString.sampleList 3
   let coins ← gmwSampleSimCoins s φ ch_guess
-  let p ← runTwoRound
+  let (view, _, challenge) ← runTwoRound
     (fun r => proverReply1 generator m r (allOpenFlags φ ch_guess coins.1) coins.1 coins.2 pads)
     (fun _ => proverReply2 s φ ch_guess coins.1 coins.2)
     prog (0, [false, false, false])
-  return if p.2.2 == ch_guess then true :: p.1 else []
+  return if challenge == ch_guess then true :: view else []
 
 /-- One attempt of the GMW zero-knowledge simulator (without any witness). -/
 noncomputable def gmwSimAttempt (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ)
@@ -693,7 +693,7 @@ private theorem isPPTOn_gmwSimWithPads {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableTidilyInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) (encList encBits)) encBits
       (fun p : (ℕ × α × List Bool) × List (List Bool) =>
         gmwSimWithPads generator (p.1.1 + 7) (length (p.1.1 + 7))
@@ -719,7 +719,7 @@ private theorem isPPTOn_gmwSimAttempt {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableTidilyInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
       (fun p : ℕ × α × List Bool =>
         gmwSimAttempt generator (p.1 + 7) (length (p.1 + 7))
@@ -742,10 +742,10 @@ theorem isPPTOn_gmwSimulator {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2)) :
+      (fun (n, a, z) => Vstar n a z)) :
     IsPPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p : ℕ × α × List Bool =>
-        gmwSimulator generator length f Vstar p.1 p.2.1 p.2.2) := by
+      (fun (n, a, z) =>
+        gmwSimulator generator length f Vstar n a z) := by
   have hg := hg.tidy
   have hf := hf.tidy
   have hattempt := isPPTOn_gmwSimAttempt hg hlen hf hV
@@ -794,7 +794,7 @@ private theorem isPPTOn_runTwoRound_honest {α Caller : Type} {enc : α ↪ List
     {n s m : Caller → ℕ} {a : Caller → α} {z : Caller → List Bool}
     {φ : Caller → CNF ℕ} {coins : Caller → List Bool × List (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hg : ComputableTidilyInPolyTime generator encBits encBits)
     (hn : ComputableTidilyInPolyTime n input encUnary)
     (hs : ComputableTidilyInPolyTime s input encUnary)
@@ -827,11 +827,15 @@ theorem isPPTOn_gmwInteract {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => 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 =>
-        gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1
-          (Vstar p.1 p.2.1 p.2.2.2)) := by
+      (fun (n, a, w, z) =>
+        gmwInteract generator (n + 7) (length (n + 7)) (f a) w
+          (Vstar n a z)) := by
+  change IsPPTOn (encPair encUnary (encPair enc (encPair encBits encBits))) encBits
+    (fun p : ℕ × α × List Bool × List Bool =>
+      gmwInteract generator (p.1 + 7) (length (p.1 + 7)) (f p.2.1) p.2.2.1
+        (Vstar p.1 p.2.1 p.2.2.2))
   have hgPlain := hg
   have hfPlain := hf
   have hg := hg.tidy
diff --git a/Complexity/Crypto/Computational/GMW/Simulator.lean b/Complexity/Crypto/Computational/GMW/Simulator.lean
index 4b8a0221ed..84a8cf86ed 100644
--- a/Complexity/Crypto/Computational/GMW/Simulator.lean
+++ b/Complexity/Crypto/Computational/GMW/Simulator.lean
@@ -474,11 +474,11 @@ noncomputable def gmwRealWithPads (generator : List Bool → List Bool) (s m : 
   let bits := realBits φ w m₀ m₁ m₂
   let openFlags := allOpenFlags φ ch_guess bits
   let seeds ← OracleComp.replicate (totalLen φ) (BitString.sampleList s)
-  let p ← runTwoRound
+  let (view, _, challenge) ← runTwoRound
     (fun r => proverReply1 generator m r openFlags bits seeds pads)
     (fun _ => proverReply2 s φ ch_guess bits seeds)
     prog (0, [false, false, false])
-  return if p.2.2 == ch_guess then true :: p.1 else []
+  return if challenge == ch_guess then true :: view else []
 
 /-- Single-attempt hybrid with pseudorandom unopened pads. -/
 noncomputable def gmwRealPRGPads (generator : List Bool → List Bool) (s m : ℕ) (φ : CNF ℕ)
@@ -862,7 +862,7 @@ private theorem isPPTOn_gmwRealWithPads {α Param : Type} {enc : α ↪ List Boo
     {φ : Param → CNF ℕ} {pads : Param → List (List Bool)}
     (hg : ComputableTidilyInPolyTime generator encBits encBits)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hn : ComputableTidilyInPolyTime n input encUnary)
     (hs : ComputableTidilyInPolyTime s input encUnary)
     (hm : ComputableTidilyInPolyTime m input encUnary)
@@ -918,14 +918,13 @@ theorem isPPTOn_gmwViewReduction {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : 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)) :
     IsPPTOn
       (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) encBool
-      (fun p : (ℕ × (α × (List Bool × List Bool))) × List Bool =>
-        gmwViewReduction generator length f Vstar adversary
-          p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) := by
+      (fun ((n, a, w, z), challenge) =>
+        gmwViewReduction generator length f Vstar adversary n a w z challenge) := by
   have hgPlain := hg
   have hfPlain := hf
   have hg := hg.tidy
@@ -1027,9 +1026,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool}
     (hlen : ∀ s, (generator s).length = length s.length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : 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))
     (hPRG : ∀ test : (ℕ × (α × (List Bool × List Bool))) × List Bool → ProbComp Bool,
       IsPPTOn
         (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits)
@@ -1060,8 +1059,9 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool}
   have hf := hf.tidy
   have hclock := isPPTOn_gmwViewReduction (.of_tidy hg) hlen (.of_tidy hf) hV hadv
   have hneg := hPRG
-    (fun p => gmwViewReduction generator length f Vstar adversary
-      p.1.1 p.1.2.1 p.1.2.2.1 p.1.2.2.2 p.2) hclock a w z ha hw hz
+    (fun ((n, a, w, z), challenge) =>
+      gmwViewReduction generator length f Vstar adversary n a w z challenge)
+    hclock a w z ha hw hz
   have hcount : ComputableTidilyInPolyTime (fun a => totalLen (f a)) enc encUnary :=
     (computableInPolyTime_totalLen (.of_tidy hf)).tidy
   have hsize : PolyBounded id (fun n => (enc (a n)).length) :=
@@ -1111,9 +1111,9 @@ theorem AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool}
     (hAdv : AdvicePRG enc generator length)
     (hf : ComputableInPolyTime f enc encCNF)
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     (hadv : 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))
     {a : ℕ → α} {w z : ℕ → List Bool}
     (ha : PolynomiallyBounded (fun n => (enc (a n)).length))
     (hw : PolynomiallyBounded (fun n => (w n).length))
@@ -1139,7 +1139,7 @@ theorem gmwView_indistinguishable_gmwSimulator {α : Type} {enc : α ↪ List Bo
     {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF)
     {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)}
     (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits
-      (fun p => Vstar p.1 p.2.1 p.2.2))
+      (fun (n, a, z) => Vstar n a z))
     {a : ℕ → α} {w z : ℕ → List Bool}
     (ha : ComputableInPolyTime a encUnary enc)
     (hw_comp : ComputableInPolyTime w encUnary encBits)
diff --git a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean
index 944d2e2fd4..7112e29ba5 100644
--- a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean
+++ b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean
@@ -1674,9 +1674,17 @@ theorem run_idealLazyHandler_good_le_realLazyHandler {α : Type}
     (program : OracleComp (EvenMansourSpec G) α) (P : α → Prop) (k : G × G)
     {c_e c_π c : Cache G} (hrel : CacheRel k c_e c_π c) :
     ((OracleComp.interpret idealLazyHandler program).run (c_e, c_π)).toOuterMeasure
-      {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} ≤
+      {(r, c_e', c_π') : α × Cache G × Cache G |
+        P r ∧ isBadEvenMansourKey c_e' c_π' k = false} ≤
     ((OracleComp.interpret (realLazyHandler k) program).run c).toOuterMeasure
       {res | P res.1} := by
+  have hset :
+      {(r, c_e', c_π') : α × Cache G × Cache G |
+        P r ∧ isBadEvenMansourKey c_e' c_π' k = false} =
+      {res | P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} := by
+    ext ⟨_, _, _⟩
+    simp
+  rw [hset]
   induction program generalizing c_e c_π c with
   | pure a =>
     change (PMF.pure (a, (c_e, c_π))).toOuterMeasure
@@ -1912,8 +1920,16 @@ private theorem idealGame_apply_le_realGame_add_of_keyDist (keyDist : PMF (G ×
           MeasureTheory.measure_union_le _ _
       _ ≤ ((OracleComp.interpret (realLazyHandler k) program).run []).toOuterMeasure
             (Prod.fst ⁻¹' {b}) +
-          M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} :=
-          add_le_add
+          M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true} := by
+          have hset :
+              {res : Bool × (Cache G × Cache G) |
+                res.1 = b ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false} =
+              {(r, c_e', c_π') : Bool × Cache G × Cache G |
+                r = b ∧ isBadEvenMansourKey c_e' c_π' k = false} := by
+            ext ⟨_, _, _⟩
+            simp
+          rw [hset]
+          exact add_le_add
             (run_idealLazyHandler_good_le_realLazyHandler program (· = b) k (cacheRel_nil k))
             le_rfl
   have hsum_ideal : ∑' k : G × G, keyDist k * evenMansourIdealGame program b =
diff --git a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
index 204a62be58..180012189f 100644
--- a/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
+++ b/Complexity/Crypto/Protocols/MPC/CircuitEval.lean
@@ -148,7 +148,8 @@ and applying `finish` at `.done`. -/
     .message (sender := p.1) (receiver := p.2)
       (fun st => st.1 p.2)
       ((msgStepsWith finish L).mapState fun i st =>
-        (st.1.1, st.1.2 + extractMsg p i st.2))
+        let (toSend, acc) := st.1
+        (toSend, acc + extractMsg p i st.2))
 
 /-- All-to-all message exchange: party `s` sends `toSend s r` to party `r`, and party `i` applies
 `finish i` to the vector `fun s => toSend s i` of received messages. -/
@@ -636,18 +637,19 @@ private theorem eval_progDist_restrict_of_ne_univ {m inputCount g : ℕ} [NeZero
     (recv : (Round.message (spec := spec) s r Bool).Received i) : Bool :=
   if h : i = r then recv h else 0
 
-/-- Gather `Bool` shares at receiver `r` from senders `S`, preserving `st.1` and `st.2.1` and
+/-- Gather `Bool` shares at receiver `r` from senders `S`, preserving `state` and `myShare` and
 applying `finish` at `.done`. -/
 @[expose] def gatherStepsWith {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type}
     (r : Fin m) (finish : (i : Fin m) → State i → Bool → Out i) :
     (S : List (Fin m)) →
       Steps (fun i => State i × Bool × Bool) Out (gatherSchedule m (spec := spec) r S)
-  | [] => .done (fun i st => finish i st.1 st.2.2)
+  | [] => .done (fun i (state, _, acc) => finish i state acc)
   | s :: S =>
     .message (sender := s) (receiver := r)
-      (fun st => st.2.1)
+      (fun (_, myShare, _) => myShare)
       ((gatherStepsWith r finish S).mapState fun i st =>
-        (st.1.1, st.1.2.1, st.1.2.2 + extractBitFor s r i st.2))
+        let (state, myShare, acc) := st.1
+        (state, myShare, acc + extractBitFor s r i st.2))
 
 /-- Sum of party `i`'s received bits along `gatherSchedule m r S`. -/
 @[expose] def sumGatherBits {m : ℕ} {spec : MultiOracleSpec} (r : Fin m) :
diff --git a/Complexity/Crypto/Protocols/MPC/Composition.lean b/Complexity/Crypto/Protocols/MPC/Composition.lean
index 57b3c57250..51f5f9370c 100644
--- a/Complexity/Crypto/Protocols/MPC/Composition.lean
+++ b/Complexity/Crypto/Protocols/MPC/Composition.lean
@@ -429,16 +429,18 @@ first state component. -/
     .message (sender := parties s₀) (receiver := parties r₀)
       (fun st_sender => send (st_sender.2 s₀ rfl))
       ((Steps.embed parties Outer next).mapState fun _ st_i =>
-        (st_i.1.1, fun s hs =>
-          (st_i.1.2 s hs,
-            pullRoundReceived parties (.message s₀ r₀ Msg) hs st_i.2)))
+        let ((outer_i, st_k_i), recv_i) := st_i
+        (outer_i, fun s hs =>
+          (st_k_i s hs,
+            pullRoundReceived parties (.message s₀ r₀ Msg) hs recv_i)))
   | .oracle (op := op) (parties := subParties) query next =>
     .oracle (op := op) (parties := subParties.trans parties)
       (fun t st_party => query t (st_party.2 (subParties t) rfl))
       ((Steps.embed parties Outer next).mapState fun _ st_i =>
-        (st_i.1.1, fun s hs =>
-          (st_i.1.2 s hs,
-            pullRoundReceived parties (.oracle op subParties) hs st_i.2)))
+        let ((outer_i, st_k_i), recv_i) := st_i
+        (outer_i, fun s hs =>
+          (st_k_i s hs,
+            pullRoundReceived parties (.oracle op subParties) hs recv_i)))
 
 @[simp] private theorem outputAt_embed {k m : ℕ} {spec : MultiOracleSpec}
     (parties : Fin k ↪ Fin m) (Outer : Fin m → Type)
@@ -515,16 +517,19 @@ execution of `(Sub op).steps` along `parties`. -/
     .message (sender := s₀) (receiver := r₀)
       (fun st_sender => send st_sender.1)
       ((Steps.compose Sub next).mapState fun _ st_i =>
-        ((st_i.1.1, st_i.2), st_i.1.2))
+        let ((state_i, coins_i), recv_i) := st_i
+        ((state_i, recv_i), coins_i))
   | .oracle (op := op) (parties := parties) (sc := rest) query next =>
     (((Steps.embed parties (fun i => State i × Schedule.SubCoins Coins₂ rest i)
         (Sub op).steps).mapState
       (fun i st_i =>
-        ((st_i.1, st_i.2.2),
+        let (state_i, slotCoins_i, restCoins_i) := st_i
+        ((state_i, restCoins_i),
           fun (s : Fin (spec₁.arity op)) (hs : parties s = i) =>
-            (query s (hs.symm ▸ st_i.1), st_i.2.1 s hs)))).append
+            (query s (hs.symm ▸ state_i), slotCoins_i s hs)))).append
       ((Steps.compose Sub next).mapState fun _ st_i =>
-        ((st_i.1.1, st_i.2), st_i.1.2)))
+        let ((state_i, restCoins_i), subOut_i) := st_i
+        ((state_i, subOut_i), restCoins_i)))
 
 /-- Expand a simulated outer execution along `steps : Steps State Out sc₁` by invoking the inner
 simulator `S₂ op (subCoalition parties I)` at every `.oracle op parties` round (Goldreich Theorem
diff --git a/Complexity/Crypto/Protocols/MPC/PolyTime.lean b/Complexity/Crypto/Protocols/MPC/PolyTime.lean
index a6f99a722e..91a7a34a7d 100644
--- a/Complexity/Crypto/Protocols/MPC/PolyTime.lean
+++ b/Complexity/Crypto/Protocols/MPC/PolyTime.lean
@@ -357,8 +357,9 @@ packed coalition input bits `extendCoalitionBits I xI` and output bits
 def encFamilySimInput {α : Type} (enc : α ↪ List Bool) (m : ℕ) (n k : α → ℕ)
     (I : Finset (Fin m)) : FamilySimInput α m n k I ↪ List Bool where
   toFun inp :=
+    let ⟨a, xI, yI⟩ := inp
     encPair enc (encPair encBits encBits)
-      (inp.1, (extendCoalitionBits I inp.2.1, extendCoalitionBits I inp.2.2))
+      (a, (extendCoalitionBits I xI, extendCoalitionBits I yI))
   inj' := by
     rintro ⟨a₁, x₁, y₁⟩ ⟨a₂, x₂, y₂⟩ h
     obtain ⟨ha, hxy⟩ := Prod.ext_iff.1 ((encPair enc (encPair encBits encBits)).injective h)
@@ -499,13 +500,15 @@ def encGMWPartyView (m coins n k : ℕ)
   let (_, r_out) :=
     splitOTMulCompose (GMWCircuit.progSchedule m D.program)
       (GMWCircuit.outputSchedule m k) i r_prog_out
+  let (preludeCoins, (circuitCoins, _), otSubCoins) := v.coins
   encPair
     (encPair (encPair encBits encBits) (encPair encBits encBits))
     (encPair encBits (encPair encBits encBits))
-    (((List.ofFn v.input, List.ofFn v.coins.1),
+    (((List.ofFn v.input, List.ofFn preludeCoins),
       (List.ofFn
-        ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm v.coins.2.1.1),
-       encOTSubCoins _ i v.coins.2.2)),
+        ((Cslib.BitString.blocksEquiv (α := Bool) (m := N) (k := m - 1)).symm
+          circuitCoins),
+       encOTSubCoins _ i otSubCoins)),
      (encPairsMsgReceived i (GMWCircuit.allPairs m) r_in,
       (encOTOracleAnswers _ i v.received,
        encOutCoordsMsgReceived i (GMWCircuit.outCoords m k) r_out)))
@@ -5959,11 +5962,11 @@ theorem isPPTOn_gmwOT14RandomizedSim {α : Type} {enc : α ↪ List Bool}
     (hC : ComputableInPolyTime (fun a => (C a).code) enc Boolean.encCode)
     (I : Finset (Fin m)) :
     Cslib.Probability.IsPPTOn (encFamilySimInput enc m n k I) encBits
-      (fun inp =>
+      (fun ⟨a, xI, yI⟩ =>
         encodeCoalitionView
-          (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$>
-          gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1)
-            (C inp.1) I inp.2.1 inp.2.2) := by
+          (encGMWPartyView m (coins a) (n a) (k a) (C a)) I <$>
+          gmwOT14RandomizedSim m (coins a) (n a) (k a) (C a)
+            I xI yI) := by
   have hD := computableInPolyTime_code_comp_xorPreludeCircuit m hn hcoins hC
   exact (PolyTimeRunner.isPPTOn_simRunWord m I hcoins.tidy hn.tidy hk.tidy hD.tidy).congr
     (PolyTimeRunner.eval_simRunWord_eq_gmwOT14RandomizedSim m coins n k C I)
@@ -6008,11 +6011,11 @@ theorem exists_perfectSemiHonestPrivate_ot14_of_polyTime {α : Type} {enc : α 
             (fun _ y => List.ofFn y) inp.2) ∧
       (∀ (I : Finset (Fin m)), I ≠ Finset.univ →
         Cslib.Probability.IsPPTOn (encFamilySimInput enc m n k I) encBits
-          (fun inp =>
+          (fun ⟨a, xI, yI⟩ =>
             encodeCoalitionView
-              (encGMWPartyView m (coins inp.1) (n inp.1) (k inp.1) (C inp.1)) I <$>
-              gmwOT14RandomizedSim m (coins inp.1) (n inp.1) (k inp.1)
-                (C inp.1) I inp.2.1 inp.2.2)) := by
+              (encGMWPartyView m (coins a) (n a) (k a) (C a)) I <$>
+              gmwOT14RandomizedSim m (coins a) (n a) (k a) (C a)
+                I xI yI)) := by
   have h_in : ComputableInPolyTime (fun a => m * n a + coins a) enc encUnary := by
     have hmn := ComputableTidilyInPolyTime.comp' ComputableTidilyInPolyTime.unary_mul
       ((ComputableTidilyInPolyTime.const m).prod hn.tidy)
diff --git a/Complexity/Crypto/Protocols/MPC/SharedMul.lean b/Complexity/Crypto/Protocols/MPC/SharedMul.lean
index 4e4e42de4e..87ded645d3 100644
--- a/Complexity/Crypto/Protocols/MPC/SharedMul.lean
+++ b/Complexity/Crypto/Protocols/MPC/SharedMul.lean
@@ -171,7 +171,7 @@ def twoPartyMulOutput (i : Fin 2)
     (st : ((Bool × Bool) × Fin.cases Bool (fun _ => Unit) i) ×
       (Round.oracle (spec := ot14Spec) () (Function.Embedding.refl (Fin 2))).Received i) : Bool :=
   Fin.cases
-    (fun (st : ((Bool × Bool) × Bool) × _) => st.1.2)
+    (fun (((_, c₀), _) : ((Bool × Bool) × Bool) × _) => c₀)
     (fun j st => st.2 j.succ rfl) i st
 
 /-- Construction 7.3.7 (p. 643): 2-party shared multiplication in the `ot14Spec`-hybrid model.
@@ -301,10 +301,18 @@ theorem perfectSemiHonestPrivate_twoPartyMul :
 abbrev OrderedPair (m : ℕ) : Type :=
   { p : Fin m × Fin m // p.1 < p.2 }
 
-/-- Embedding of `Fin 2` into `Fin m` sending `0 ↦ p.1.1` and `1 ↦ p.1.2` for an ordered pair
+/-- First party `i` of an ordered pair `(i, j)` in `OrderedPair m`. -/
+abbrev OrderedPair.first {m : ℕ} (p : OrderedPair m) : Fin m :=
+  p.val.1
+
+/-- Second party `j` of an ordered pair `(i, j)` in `OrderedPair m`. -/
+abbrev OrderedPair.second {m : ℕ} (p : OrderedPair m) : Fin m :=
+  p.val.2
+
+/-- Embedding of `Fin 2` into `Fin m` sending `0 ↦ p.first` and `1 ↦ p.second` for an ordered pair
 `p : OrderedPair m`. -/
 def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where
-  toFun := Fin.cases p.1.1 (fun _ => p.1.2)
+  toFun := Fin.cases p.first (fun _ => p.second)
   inj' a b h := by
     fin_cases a <;> fin_cases b
     · rfl
@@ -313,19 +321,19 @@ def pairEmbedding {m : ℕ} (p : OrderedPair m) : Fin 2 ↪ Fin m where
     · rfl
 
 @[simp] theorem pairEmbedding_zero {m : ℕ} (p : OrderedPair m) :
-    pairEmbedding p 0 = p.1.1 := rfl
+    pairEmbedding p 0 = p.first := rfl
 
 @[simp] theorem pairEmbedding_one {m : ℕ} (p : OrderedPair m) :
-    pairEmbedding p 1 = p.1.2 := rfl
+    pairEmbedding p 1 = p.second := rfl
 
 /-- Joint 2-party shared-multiplication oracle round for `p : OrderedPair m`. -/
 @[reducible] def pairRound {m : ℕ} (p : OrderedPair m) : Round m (sharedMulSpec 2) :=
   .oracle () (pairEmbedding p)
 
-/-- A party `i` that is neither `p.1.1` nor `p.1.2` receives a subsingleton record in
+/-- A party `i` that is neither `p.first` nor `p.second` receives a subsingleton record in
 `pairRound p`. -/
 theorem subsingleton_received_pairRound {m : ℕ} (p : OrderedPair m) {i : Fin m}
-    (h1 : i ≠ p.1.1) (h2 : i ≠ p.1.2) : Subsingleton ((pairRound p).Received i) := by
+    (h1 : i ≠ p.first) (h2 : i ≠ p.second) : Subsingleton ((pairRound p).Received i) := by
   refine ⟨fun r₁ r₂ => Round.received_oracle_ext fun s hs => ?_⟩
   fin_cases s
   · exact (h1 hs.symm).elim
@@ -348,12 +356,12 @@ def orderedPairs (m : ℕ) : List (OrderedPair m) :=
   pairsSchedule (orderedPairs m)
 
 /-- Extract party `i`'s oracle answer share from `pairRound p` (`0` if `i` is not one of the
-two participating parties `p.1.1` or `p.1.2`). -/
+two participating parties `p.first` or `p.second`). -/
 def extractPairShare {m : ℕ} (p : OrderedPair m) (i : Fin m)
     (r : (pairRound p).Received i) : Bool :=
-  if h0 : p.1.1 = i then
+  if h0 : p.first = i then
     r 0 h0
-  else if h1 : p.1.2 = i then
+  else if h1 : p.second = i then
     r 1 h1
   else
     0
@@ -370,7 +378,8 @@ def pairsSteps {m : ℕ} :
     .oracle (op := ()) (parties := pairEmbedding p)
       (fun _ st => st.1)
       ((pairsSteps L).mapState fun i st =>
-        (st.1.1, st.1.2 + extractPairShare p i st.2))
+        let (xy, acc) := st.1
+        (xy, acc + extractPairShare p i st.2))
 
 /-- Construction 7.5.8 (p. 704): `m`-party shared multiplication in the 2-ary
 `sharedMulSpec 2`-hybrid model, invoking `sharedMulSpec 2` once for each pair `i < j`.
@@ -383,7 +392,8 @@ def multiPartyMulProtocol (m : ℕ) :
   sampleCoins _ := pure ()
   steps :=
     (pairsSteps (orderedPairs m)).mapState fun _ st =>
-      (st.1, m • (st.1.1 * st.1.2))
+      let (a, b) := st.1
+      ((a, b), m • (a * b))
 
 namespace MultiPartyMul
 
@@ -414,7 +424,7 @@ theorem outputOfView_multiPartyMulProtocol {m : ℕ} (i : Fin m)
 pairwise shares `row_i : Fin m → Bool`. -/
 def receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m) (row_i : Fin m → Bool) :
     (pairRound p).Received i :=
-  fun s _ => Fin.cases (row_i p.1.2) (fun _ => row_i p.1.1) s
+  fun s _ => Fin.cases (row_i p.second) (fun _ => row_i p.first) s
 
 /-- Construct party `i`'s received transcript along `pairsSchedule L` from party `i`'s row of
 pairwise shares `row_i : Fin m → Bool`. -/
@@ -426,8 +436,8 @@ def receivedScheduleOfRow {m : ℕ} (i : Fin m) (row_i : Fin m → Bool) :
 theorem extractPairShare_receivedPairOfRow {m : ℕ} (p : OrderedPair m) (i : Fin m)
     (row_i : Fin m → Bool) :
     extractPairShare p i (receivedPairOfRow p i row_i) =
-      (if p.1.1 = i then row_i p.1.2 else 0) +
-        (if p.1.2 = i then row_i p.1.1 else 0) := by
+      (if p.first = i then row_i p.second else 0) +
+        (if p.second = i then row_i p.first else 0) := by
   dsimp [extractPairShare, receivedPairOfRow]
   by_cases h0 : p.1.1 = i
   · have h1 : p.1.2 ≠ i := fun h => ne_of_lt p.2 (h0.trans h.symm)
@@ -477,7 +487,7 @@ theorem sumReceivedShares_receivedScheduleOfRow {m : ℕ} (i : Fin m)
     | nil => rfl
     | cons p L ih => simp [sumReceivedShares, receivedScheduleOfRow, ih]
   rw [hL, sum_map_orderedPairs]
-  simp only [extractPairShare_receivedPairOfRow, dite_eq_ite]
+  simp only [extractPairShare_receivedPairOfRow, OrderedPair.first, OrderedPair.second, dite_eq_ite]
   have hsplit : ∀ u v : Fin m,
       (if u < v then
         (if u = i then row_i v else 0) + (if v = i then row_i u else 0)
@@ -644,7 +654,7 @@ def viewOfRow {m : ℕ} (i : Fin m) (xi : Bool × Bool) (row_i : Fin m → Bool)
 /-- 2-party oracle answer tuple for pair `p` on input `x` and coin `b : Bool`. -/
 def pairAnswer {m : ℕ} (x : Fin m → Bool × Bool) (p : OrderedPair m) (b : Bool) :
     Fin 2 → Bool :=
-  completeShares 2 (pairTarget x p.1.1 p.1.2) (fun _ => b)
+  completeShares 2 (pairTarget x p.first p.second) (fun _ => b)
 
 theorem deliverOracle_pairAnswer_eq_receivedPairOfRow {m : ℕ}
     (x : Fin m → Bool × Bool) (r : OrderedPair m → Bool) (p : OrderedPair m) (i : Fin m) :
@@ -797,17 +807,17 @@ theorem evalWith_multiPartyMulProtocol (m : ℕ) (x : Fin m → Bool × Bool) :
 
 /-- Coin adjustment supported on pairs incident to the pivot party `ℓ : Fin m`. -/
 def delta {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) (p : OrderedPair m) : Bool :=
-  if p.1.1 = ℓ then w p.1.2
-  else if p.1.2 = ℓ then w p.1.1
+  if p.first = ℓ then w p.second
+  else if p.second = ℓ then w p.first
   else 0
 
 /-- Restriction-based presentation of `delta ℓ` depending only on `Finset.univ.erase ℓ`. -/
 def deltaErase {m : ℕ} (ℓ : Fin m) (u : (i : Finset.univ.erase ℓ) → Bool)
     (p : OrderedPair m) : Bool :=
-  if h1 : p.1.1 = ℓ then
-    u ⟨p.1.2, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩
-  else if h2 : p.1.2 = ℓ then
-    u ⟨p.1.1, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩
+  if h1 : p.first = ℓ then
+    u ⟨p.second, Finset.mem_erase.mpr ⟨ne_of_gt (h1 ▸ p.2), Finset.mem_univ _⟩⟩
+  else if h2 : p.second = ℓ then
+    u ⟨p.first, Finset.mem_erase.mpr ⟨ne_of_lt (h2 ▸ p.2), Finset.mem_univ _⟩⟩
   else 0
 
 theorem delta_eq_deltaErase_restrict {m : ℕ} (ℓ : Fin m) (w : Fin m → Bool) :
@@ -912,8 +922,8 @@ def extendOut {m : ℕ} (I : Finset (Fin m)) (yI : (i : I) → Bool) (j : Fin m)
 `matrixOfCoins (extendIn I (I.restrict x)) r i` for all `i ∈ I`. -/
 def sigmaShift {m : ℕ} (I : Finset (Fin m)) (x : Fin m → Bool × Bool)
     (p : OrderedPair m) : Bool :=
-  if p.1.2 ∈ I then
-    pairTarget x p.1.2 p.1.1 + pairTarget (extendIn I (I.restrict x)) p.1.2 p.1.1
+  if p.second ∈ I then
+    pairTarget x p.second p.first + pairTarget (extendIn I (I.restrict x)) p.second p.first
   else
     0
 
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean
index f6c4055806..fcc67e4bb2 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Abort.lean
@@ -77,7 +77,7 @@ noncomputable def acceptedTranscript (x : X) (y : Y) (c : C) : PMF (Option (T ×
 /-- An honest conversation with a uniform challenge, or `none` if the prover aborts. -/
 noncomputable def acceptedConversation [Fintype C] [Nonempty C] (x : X) (y : Y) :
     PMF (Option (T × C × Z)) :=
-  (P.conversation x y).map fun tcz => tcz.2.2.map fun z => (tcz.1, tcz.2.1, z)
+  (P.conversation x y).map fun (t, c, z?) => z?.map fun z => (t, c, z)
 
 /-- Completeness up to aborts: for every witness-statement pair in `R` and every challenge,
 every honest transcript in which the prover does not abort is accepting. -/
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
index e8b48e8d24..0b05350db6 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Basic.lean
@@ -190,12 +190,13 @@ variable {P}
 
 /-- Every honest conversation is accepting: the verifier always accepts the honest prover. -/
 theorem Complete.accepts_of_mem_support_conversation [Fintype C] [Nonempty C]
-    (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {tcz : T × C × Z}
-    (htcz : tcz ∈ (P.conversation x y).support) : P.Accepts y tcz.1 tcz.2.1 tcz.2.2 := by
+    (h : P.Complete R) {x : X} {y : Y} (hxy : R x y) {t : T} {c : C} {z : Z}
+    (htcz : (t, c, z) ∈ (P.conversation x y).support) :
+    P.Accepts y t c z := by
   rw [conversation_eq_bind_transcript] at htcz
   simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff,
-    PMF.mem_support_pure_iff] at htcz
-  obtain ⟨c, -, tz, htz, rfl⟩ := htcz
+    PMF.mem_support_pure_iff, Prod.mk.injEq] at htcz
+  obtain ⟨c, -, tz, htz, rfl, rfl, rfl⟩ := htcz
   exact h x y hxy c tz htz
 
 /-- With a uniform challenge, the simulator reproduces the honest conversation law
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean
index 1004242401..860d2b60ca 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Composition.lean
@@ -176,15 +176,18 @@ noncomputable def orProof (P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀) (P₁ : S
   respond _ y s c := match s with
     | .inl (x, s₀, c₁, z₁) => (c - c₁, P₀.respond x y.1 s₀ (c - c₁), z₁)
     | .inr (x, s₁, c₀, z₀) => (c₀, z₀, P₁.respond x y.2 s₁ (c - c₀))
-  verify y t c z := P₀.verify y.1 t.1 z.1 z.2.1 && P₁.verify y.2 t.2 (c - z.1) z.2.2
+  verify y t c
+    | (c₀, z₀, z₁) => P₀.verify y.1 t.1 c₀ z₀ && P₁.verify y.2 t.2 (c - c₀) z₁
 
 /-- The OR extractor uses the first side when the first side's challenges differ, and the
 second side otherwise. -/
 def orExtract [DecidableEq C] (extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀)
     (extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁) (y : Y₀ × Y₁) (t : T₀ × T₁) (c : C)
     (z : C × Z₀ × Z₁) (c' : C) (z' : C × Z₀ × Z₁) : X₀ ⊕ X₁ :=
-  if z.1 = z'.1 then .inr (extract₁ y.2 t.2 (c - z.1) z.2.2 (c' - z'.1) z'.2.2)
-  else .inl (extract₀ y.1 t.1 z.1 z.2.1 z'.1 z'.2.1)
+  let (c₀, z₀, z₁) := z
+  let (c₀', z₀', z₁') := z'
+  if c₀ = c₀' then .inr (extract₁ y.2 t.2 (c - c₀) z₁ (c' - c₀') z₁')
+  else .inl (extract₀ y.1 t.1 c₀ z₀ c₀' z₀')
 
 /-- The OR simulator splits the challenge uniformly and simulates both sides. -/
 noncomputable def orSimulate (simulate₀ : Y₀ → C → PMF (T₀ × Z₀))
@@ -201,9 +204,9 @@ variable {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁
 
 /-- An OR conversation `(c₀, z₀, z₁)` for the challenge `c` is accepting exactly when the first
 side accepts at `c₀` and the second at `c - c₀`. -/
-@[simp] theorem orProof_accepts_iff {y : Y₀ × Y₁} {t : T₀ × T₁} {c : C} {z : C × Z₀ × Z₁} :
-    (orProof P₀ P₁ simulate₀ simulate₁).Accepts y t c z ↔
-      P₀.Accepts y.1 t.1 z.1 z.2.1 ∧ P₁.Accepts y.2 t.2 (c - z.1) z.2.2 := by
+@[simp] theorem orProof_accepts_iff {y : Y₀ × Y₁} {t : T₀ × T₁} {c c₀ : C} {z₀ : Z₀} {z₁ : Z₁} :
+    (orProof P₀ P₁ simulate₀ simulate₁).Accepts y t c (c₀, z₀, z₁) ↔
+      P₀.Accepts y.1 t.1 c₀ z₀ ∧ P₁.Accepts y.2 t.2 (c - c₀) z₁ := by
   simp only [Accepts, orProof, Bool.and_eq_true]
 
 /-- With a witness for the first statement, the OR prover simulates the second side at a
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
index 39a83a0cbe..342449f69c 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean
@@ -157,9 +157,9 @@ noncomputable def reductionHandler :
     (q : M ⊕ (M × T)) → StateT (ReductionState M T C Z) (OracleComp (fun _ : M × T => C))
       (ForgerSpec M (M × T) (T × Z) C q)
   | .inl m => fun st =>
-    let v := st.transcripts.headD (Classical.arbitrary _)
-    pure ((v.1, v.2.2),
-      ⟨((m, v.1), v.2.1, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩)
+    let (t, c, z) := st.transcripts.headD (Classical.arbitrary _)
+    pure ((t, z),
+      ⟨((m, t), c, none) :: st.table, m :: st.signed, st.count, st.transcripts.tail⟩)
   | .inr x => fun st =>
     match st.table.lookup x with
     | some entry => pure (entry.1, ⟨st.table, st.signed, st.count, st.transcripts.tail⟩)
@@ -172,18 +172,20 @@ the position of the query for `(m, t)`. The verdict records the point, the chall
 response. -/
 def verdict (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × (T × Z)) × ReductionState M T C Z)
     (c : C) (position : Option ℕ) : Option ℕ × Bool × (M × T) × C × Z :=
-  (if P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1 then position
-    else none, P.verify y forged.1.2.1 c forged.1.2.2 && !forged.2.signed.contains forged.1.1,
-    (forged.1.1, forged.1.2.1), c, forged.1.2.2)
+  let ((m, t, z), state) := forged
+  (if P.verify y t c z && !state.signed.contains m then position
+    else none, P.verify y t c z && !state.signed.contains m,
+    (m, t), c, z)
 
 /-- Check a forgery, querying its point when the table lacks it. -/
 noncomputable def finish (P : SigmaProtocol X Y T C Z) (y : Y)
     (forged : (M × (T × Z)) × ReductionState M T C Z) :
     OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) :=
-  match forged.2.table.lookup (forged.1.1, forged.1.2.1) with
+  let ((m, t, _), state) := forged
+  match state.table.lookup (m, t) with
   | some entry => pure (verdict P y forged entry.1 entry.2)
-  | none => (fun c => verdict P y forged c (some forged.2.count)) <$>
-      OracleComp.query (forged.1.1, forged.1.2.1)
+  | none => (fun c => verdict P y forged c (some state.count)) <$>
+      OracleComp.query (m, t)
 
 /-- The forger, with simulated signing, as a program over the hash oracle with explicit coins: the
 statement, the forger's coins and the simulated transcripts. It names the query of the forgery's
@@ -191,7 +193,8 @@ point when the forger wins. -/
 noncomputable def forkingProgram (P : SigmaProtocol X Y T C Z)
     (A : Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) :
     OracleComp (fun _ : M × T => C) (Option ℕ × Bool × (M × T) × C × Z) :=
-  (interpret reductionHandler (A.forge s.1 s.2.1)).run ⟨[], [], 0, s.2.2⟩ >>= finish P s.1
+  let (y, coins, transcripts) := s
+  (interpret reductionHandler (A.forge y coins)).run ⟨[], [], 0, transcripts⟩ >>= finish P y
 
 /-- The coins of the forking program for the statement `y`: the forger's coins and `Q` simulated
 transcripts. -/
@@ -214,7 +217,9 @@ noncomputable def reduction [Nonempty X] (P : SigmaProtocol X Y T C Z)
       match result with
       | none => Classical.arbitrary X
       | some (_, out, out') =>
-        extract y out.1.2.2.1.2 out.1.2.2.2.1 out.1.2.2.2.2 out'.1.2.2.2.1 out'.1.2.2.2.2
+        let (_, _, (_, t), c, z) := out.1
+        let (_, _, _, c', z') := out'.1
+        extract y t c z c' z'
 
 end FiatShamir
 
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean
index 51b1e28c6d..f21e73ab5b 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Linear.lean
@@ -219,25 +219,26 @@ noncomputable def chaumPedersen (g : G) : SigmaProtocol (ZMod q) (G × G × G) (
 
 /-- The Chaum–Pedersen verification equations `z • g = t₁ + c • v` and `z • u = t₂ + c • w`
 ([BonehShoup2023], Section 19.5.2). -/
-@[simp] theorem chaumPedersen_accepts_iff {s : G × G × G} {t : G × G} {c : C} {z : ZMod q} :
-    (chaumPedersen ι g).Accepts s t c z ↔
-      z • g = t.1 + ι c • s.2.1 ∧ z • s.1 = t.2 + ι c • s.2.2 := by
+@[simp] theorem chaumPedersen_accepts_iff {u v w : G} {t : G × G} {c : C} {z : ZMod q} :
+    (chaumPedersen ι g).Accepts (u, v, w) t c z ↔
+      z • g = t.1 + ι c • v ∧ z • u = t.2 + ι c • w := by
   simp [chaumPedersen, Prod.ext_iff]
 
 /-- Theorem 19.10 of [BonehShoup2023]: completeness. -/
 theorem chaumPedersen_complete :
-    (chaumPedersen ι g).Complete fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2 :=
+    (chaumPedersen ι g).Complete fun β (u, v, w) => β • g = v ∧ β • u = w :=
   (linear_complete _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h
 
 /-- Theorem 19.10 of [BonehShoup2023]: special soundness. -/
 theorem chaumPedersen_specialSoundness [Fact q.Prime] :
-    (chaumPedersen ι g).SpecialSoundness (fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2)
+    (chaumPedersen ι g).SpecialSoundness
+      (fun β (u, v, w) => β • g = v ∧ β • u = w)
       (linearExtract ι) :=
   (linear_specialSoundness _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h
 
 /-- Theorem 19.10 of [BonehShoup2023]: special honest-verifier zero knowledge. -/
 theorem chaumPedersen_specialHVZK :
-    (chaumPedersen ι g).SpecialHVZK (fun β s => β • g = s.2.1 ∧ β • s.1 = s.2.2)
+    (chaumPedersen ι g).SpecialHVZK (fun β (u, v, w) => β • g = v ∧ β • u = w)
       (linearSimulate (fun s => (LinearMap.toSpanSingleton (ZMod q) G g).prod
         (LinearMap.toSpanSingleton (ZMod q) G s.1)) Prod.snd ι) :=
   (linear_specialHVZK _ _ ι).mono fun _ _ h => by simpa [Prod.ext_iff] using h
diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean
index 1f2f26dcff..54a4f59782 100644
--- a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean
+++ b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean
@@ -101,8 +101,9 @@ def lyubashevskyExtractList (input : LyubashevskyExtractInput) : List ℤ :=
       (if input.2.1.1.getD i false then (1 : ℤ) else 0))
 
 /-- Extraction always writes the two declared segments, even on malformed-length inputs. -/
-@[simp] theorem length_lyubashevskyExtractList (input : LyubashevskyExtractInput) :
-    (lyubashevskyExtractList input).length = input.1.1 + input.1.2 := by
+@[simp] theorem length_lyubashevskyExtractList (m k : ℕ)
+    (cz cz' : List Bool × Option (List ℤ)) :
+    (lyubashevskyExtractList ((m, k), cz, cz')).length = m + k := by
   simp [lyubashevskyExtractList]
 
 /-- One native extractor handles runtime dimensions and all binary integer magnitudes. -/