From 02a1ec431280ba948a183a8e6e79f7baa628983f Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 11:53:13 +0000
Subject: [PATCH 1/3] refactor(probability): replace positional projection
 chains in public declarations (#1764)

---
 .../Probabilistic/Oracle/Parameter.lean             |  9 ++++++---
 .../Probabilistic/Oracle/Substitution.lean          |  6 ++++--
 .../Probabilistic/OracleSimulation.lean             |  3 ++-
 .../Computability/Probabilistic/Presample.lean      |  6 ++++--
 .../Realization/OpenOracleSimulation.lean           |  6 ++++--
 .../Probabilistic/Realization/OracleSimulation.lean |  6 ++++--
 Complexity/Languages/Probabilistic/Forking.lean     | 13 +++++++------
 .../Languages/Probabilistic/Oracle/Simulation.lean  |  5 +++--
 Complexity/Languages/Probabilistic/Presample.lean   |  4 ++--
 Complexity/Languages/Probabilistic/Selection.lean   |  8 ++++----
 Complexity/Languages/Probabilistic/Simulation.lean  |  4 ++--
 .../UniformLearning/KushilevitzMansour.lean         |  8 +++++---
 Complexity/Probability/ApproximateCounting.lean     |  2 +-
 Complexity/Probability/CorrelatedSampling.lean      |  4 ++--
 .../CorrelatedSampling/Embeddability.lean           |  4 ++--
 Complexity/Probability/Guessing.lean                |  2 +-
 .../PairwiseIndependentHash/ComponentGap.lean       |  2 +-
 .../PairwiseIndependentHash/FrameChannel.lean       |  8 ++++----
 .../PairwiseIndependentHash/FrameRetention.lean     |  5 +++--
 .../PairwiseIndependentHash/FrameSubstitution.lean  |  4 ++--
 .../PairwiseIndependentHash/SliceGap.lean           |  2 +-
 Complexity/Tactic/PolyTime/Init.lean                |  2 +-
 22 files changed, 65 insertions(+), 48 deletions(-)

diff --git a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
index cb7fa7483c..cea8e28ff4 100644
--- a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
+++ b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
@@ -103,7 +103,8 @@ theorem IsOraclePPT.run_interpret_preprocess {Caller State : Type}
     (hprepare : ComputableTidilyInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -133,7 +134,8 @@ theorem IsOraclePPT.run_interpret_preprocess_open {External Caller State : Type}
     (hprepare : ComputableTidilyInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -163,7 +165,8 @@ theorem IsOraclePPT.run_interpret_preprocess_open' {External Caller State : Type
     (hprepare : ComputableInPolyTime prepare input (encPair encUnary encBits))
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
index 9bb338f638..b94dd670f9 100644
--- a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
+++ b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
@@ -68,7 +68,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open
     (hprepare : ComputableTidilyInPolyTime prepare input source)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -138,7 +139,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open'
     (hprepare : ComputableInPolyTime prepare input source)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/OracleSimulation.lean b/Complexity/Computability/Probabilistic/OracleSimulation.lean
index a2746f34ba..1f68bed715 100644
--- a/Complexity/Computability/Probabilistic/OracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/OracleSimulation.lean
@@ -57,7 +57,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess {Operation α β Caller State : T
     (hprepare : ComputableTidilyInPolyTime prepare input source)
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/Presample.lean b/Complexity/Computability/Probabilistic/Presample.lean
index 8f9dc374fb..52166855c4 100644
--- a/Complexity/Computability/Probabilistic/Presample.lean
+++ b/Complexity/Computability/Probabilistic/Presample.lean
@@ -55,7 +55,8 @@ theorem IsOraclePPTOn.run_interpret_withSampleList
     (horacle : IsPPTOn
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => oracle (Prod.fst pair.1) (Prod.snd pair.1) (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
@@ -115,7 +116,8 @@ theorem IsOraclePPT.run_interpret_withSampleList
     (horacle : IsPPTOn
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => oracle (Prod.fst pair.1) (Prod.snd pair.1) (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
diff --git a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
index eda4549801..5643a6dbc6 100644
--- a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
@@ -101,7 +101,8 @@ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)}
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) :
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2))) :
     IsOraclePPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) := by
@@ -160,7 +161,8 @@ theorem isOraclePPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hcount : ComputableInPolyTime count input encUnary)
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)
diff --git a/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean b/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
index 2a6dd0efc3..258fb37c06 100644
--- a/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
@@ -110,7 +110,8 @@ theorem isPPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     {handler : α → Operation × List Bool → State → ProbComp (List Bool × State)}
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) :
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2))) :
     IsPPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) :=
@@ -129,7 +130,8 @@ theorem isPPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hcount : ComputableInPolyTime count input encUnary)
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
-      (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2))
+      (encPair encBits stateEncoding)
+      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)
diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean
index b0919c3a11..12fe47afab 100644
--- a/Complexity/Languages/Probabilistic/Forking.lean
+++ b/Complexity/Languages/Probabilistic/Forking.lean
@@ -155,12 +155,13 @@ theorem runWithAnswers_run_interpret_invariant {ι σ β : Type} {spec : ι →
     (handler : (q : ι) → StateT σ (OracleComp (fun _ : Query => H)) (spec q))
     (answers : List H) (invariant : σ → List Query → Prop)
     (step : ∀ q s queries, invariant s queries →
-      invariant (runWithAnswers default ((handler q).run s) (answers.drop queries.length)).1.2
+      invariant
+        (Prod.snd (runWithAnswers default ((handler q).run s) (answers.drop queries.length)).1)
         (queries ++ (runWithAnswers default ((handler q).run s)
           (answers.drop queries.length)).2))
     (program : OracleComp spec β) (s : σ) (queries : List Query) (hs : invariant s queries) :
-    invariant (runWithAnswers default ((interpret handler program).run s)
-        (answers.drop queries.length)).1.2
+    invariant (Prod.snd (runWithAnswers default ((interpret handler program).run s)
+        (answers.drop queries.length)).1)
       (queries ++ (runWithAnswers default ((interpret handler program).run s)
         (answers.drop queries.length)).2) := by
   induction program using OracleComp.induction generalizing s queries with
@@ -334,7 +335,7 @@ def forkingAlgorithm {S β : Type} (default : H) (q : ℕ)
     (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) :
     Option (Fin q) × ((Option ℕ × β) × List Query) :=
   (validIndex q (runWithAnswers default (program s) (List.ofFn h)).2.length
-      (runWithAnswers default (program s) (List.ofFn h)).1.1,
+      (Prod.fst (runWithAnswers default (program s) (List.ofFn h)).1),
     runWithAnswers default (program s) (List.ofFn h))
 
 variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H]
@@ -349,7 +350,7 @@ theorem le_add_sqrt_fork (first : PMF S)
     ((do
       let s ← first
       let run ← (interpret countingUniform (program s)).run 0
-      return (validIndex q run.2 run.1.1).isSome : PMF Bool) true).toReal ≤
+      return (validIndex q run.2 (Prod.fst run.1)).isSome : PMF Bool) true).toReal ≤
       q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map
         Option.isSome true).toReal) := by
   have hacc : (do
@@ -377,7 +378,7 @@ theorem mem_support_fork {first : PMF S}
     ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧
       out = runWithAnswers default (program s) (List.ofFn h) ∧
       out' = runWithAnswers default (program s) (List.ofFn h') ∧
-      out.1.1 = some j.val ∧ out'.1.1 = some j.val ∧
+      Prod.fst out.1 = some j.val ∧ Prod.fst out'.1 = some j.val ∧
       out.2.take (j + 1) = out'.2.take (j + 1) ∧
       ∃ query, out.2[j.val]? = some query ∧ out'.2[j.val]? = some query := by
   obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork
diff --git a/Complexity/Languages/Probabilistic/Oracle/Simulation.lean b/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
index fe07a4a9dd..3e9830e622 100644
--- a/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
+++ b/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
@@ -194,8 +194,9 @@ theorem run_interpret_run_interpret {Query' : Type} {spec' : Query' → Type}
       (fun q state => ((OracleComp.interpret
         (handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
           ((inner q).run state.1)).run state.2).map
-            (fun result => (result.1.1, result.1.2, result.2)))) program).run
-        (hidden, external)).map (fun result => ((result.1, result.2.1), result.2.2)) := by
+            (fun result => (Prod.fst result.1, Prod.snd result.1, result.2)))) program).run
+        (hidden, external)).map
+          (fun result => ((result.1, Prod.fst result.2), Prod.snd result.2)) := by
   rw [OracleComp.run_interpret_run_interpret, _root_.PMF.monad_map_eq_map]
   congr 3
   funext q state
diff --git a/Complexity/Languages/Probabilistic/Presample.lean b/Complexity/Languages/Probabilistic/Presample.lean
index f9397bc3b3..bf37ceb21a 100644
--- a/Complexity/Languages/Probabilistic/Presample.lean
+++ b/Complexity/Languages/Probabilistic/Presample.lean
@@ -77,7 +77,7 @@ theorem IsQueryBounded.run_interpret_presample {program : ProbOracleComp spec α
     ((PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (withSampleList fallback oracle)) program).run (s, values)).map
-          fun result => (result.1, result.2.1)) =
+          fun result => (result.1, Prod.fst result.2)) =
       (interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (fun q state => source.bind fun value => oracle value q state)) program).run s := by
   induction h generalizing s with
@@ -137,7 +137,7 @@ theorem OracleComp.IsQueryBounded.run_interpret_presample {Query State Value γ
     (oracle : Value → (q : Query) → StateT State PMF (spec q)) (s : State) :
     ((Probability.PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (withSampleList fallback oracle) program).run (s, values)).map
-        fun result => (result.1, result.2.1)) =
+        fun result => (result.1, Prod.fst result.2)) =
       (interpret (m := StateT State PMF)
         (fun q state => source.bind fun value => oracle value q state) program).run s := by
   simpa only [interpret_interpret, ProbOracleComp.interpret_query] using
diff --git a/Complexity/Languages/Probabilistic/Selection.lean b/Complexity/Languages/Probabilistic/Selection.lean
index d200e06d9b..882551fce4 100644
--- a/Complexity/Languages/Probabilistic/Selection.lean
+++ b/Complexity/Languages/Probabilistic/Selection.lean
@@ -54,7 +54,7 @@ variable {Query : Type u} {spec : OracleSpec.{u, 0} Query}
 
 /-- Update the next index, best index, and best success count, preferring later indices on ties. -/
 def selectUpdate (state : ℕ × ℕ × ℕ) (successes : ℕ) : ℕ × ℕ × ℕ :=
-  (state.1 + 1, if state.2.2 ≤ successes then (state.1, successes) else state.2)
+  (state.1 + 1, if Prod.snd state.2 ≤ successes then (state.1, successes) else state.2)
 
 /-- Estimate one candidate and update the running empirical maximum. -/
 def selectStep (trials : ℕ) (test : ℕ → OracleComp spec Bool)
@@ -65,7 +65,7 @@ def selectStep (trials : ℕ) (test : ℕ → OracleComp spec Bool)
 When there are no candidates, return zero. -/
 def selectBest (count trials : ℕ) (test : ℕ → OracleComp spec Bool) :
     OracleComp spec ℕ :=
-  (fun state => state.2.1) <$> iterate count (selectStep trials test) (0, 0, 0)
+  (fun state => Prod.fst state.2) <$> iterate count (selectStep trials test) (0, 0, 0)
 
 /-- Select an empirically best value from a list, returning the fallback for an empty list. -/
 def selectFrom {α : Type} (values : List α) (trials : ℕ)
@@ -112,9 +112,9 @@ theorem sampleBest_support {α : Type} (count trials : ℕ) (source : ProbComp 
 /-- Candidate selection keeps both indices within the elapsed count and the success count within
 the trial budget on every execution, regardless of statistical estimation errors. -/
 theorem selectStep_bounded (trials : ℕ) (test : ℕ → ProbComp Bool) (i : ℕ)
-    (state : ℕ × ℕ × ℕ) (hstate : state.1 = i ∧ state.2.1 ≤ i ∧ state.2.2 ≤ trials)
+    (state : ℕ × ℕ × ℕ) (hstate : state.1 = i ∧ Prod.fst state.2 ≤ i ∧ Prod.snd state.2 ≤ trials)
     (next : ℕ × ℕ × ℕ) (hnext : next ∈ (eval (OracleComp.selectStep trials test state)).support) :
-    next.1 = i + 1 ∧ next.2.1 ≤ i + 1 ∧ next.2.2 ≤ trials := by
+    next.1 = i + 1 ∧ Prod.fst next.2 ≤ i + 1 ∧ Prod.snd next.2 ≤ trials := by
   rw [OracleComp.selectStep, eval_map, PMF.mem_support_map_iff] at hnext
   obtain ⟨successes, hsuccesses, rfl⟩ := hnext
   have hbound := countTrue_le trials (test state.1) hsuccesses
diff --git a/Complexity/Languages/Probabilistic/Simulation.lean b/Complexity/Languages/Probabilistic/Simulation.lean
index a8cf4ac8d8..05e4a9fd14 100644
--- a/Complexity/Languages/Probabilistic/Simulation.lean
+++ b/Complexity/Languages/Probabilistic/Simulation.lean
@@ -232,9 +232,9 @@ theorem run_interpret_run_interpret {κ : Type w} {target : OracleSpec.{w, v} κ
     (oracle : (q : κ) → StateT External m (target q))
     (program : OracleComp spec α) (hidden : Hidden) (external : External) :
     (interpret oracle ((interpret handler program).run hidden)).run external =
-      (fun result => ((result.1, result.2.1), result.2.2)) <$>
+      (fun result => ((result.1, Prod.fst result.2), Prod.snd result.2)) <$>
         (interpret (m := StateT (Hidden × External) m) (fun q state =>
-          (fun result => (result.1.1, result.1.2, result.2)) <$>
+          (fun result => (Prod.fst result.1, Prod.snd result.1, result.2)) <$>
             (interpret oracle ((handler q).run state.1)).run state.2) program).run
           (hidden, external) := by
   induction program using OracleComp.induction generalizing hidden external with
diff --git a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
index 6f0703524a..9a7d42a908 100644
--- a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
+++ b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
@@ -237,8 +237,9 @@ samples `ω j = (x, y, z)`: the average of `g (x, z) χ_S(x) g (y, z) χ_S(y)`,
 the coordinates in `J` from `x` and the others from `z`. -/
 noncomputable def bucketEstimate (g : (ι → Bool) → Bool)
     (ω : Fin m → (ι → Bool) × (ι → Bool) × (ι → Bool)) (J S : Finset ι) : ℝ :=
-  (∑ j, signVal (g (J.piecewise (ω j).1 (ω j).2.2)) * chi ℝ S (ω j).1 *
-    (signVal (g (J.piecewise (ω j).2.1 (ω j).2.2)) * chi ℝ S (ω j).2.1)) / m
+  (∑ j, signVal (g (J.piecewise (ω j).1 (Prod.snd (ω j).2))) * chi ℝ S (ω j).1 *
+    (signVal (g (J.piecewise (Prod.fst (ω j).2) (Prod.snd (ω j).2))) *
+      chi ℝ S (Prod.fst (ω j).2))) / m
 
 /-- The empirical Fourier coefficient of `g` on `S` from the first points of the samples. -/
 noncomputable def sampleCoeff (g : (ι → Bool) → Bool)
@@ -265,7 +266,8 @@ noncomputable def kmQueries (ω : Fin m → (ι → Bool) × (ι → Bool) × (
   (List.finRange m).map (fun j => (ω j).1) ++
     (searchLevels (univ : Finset ι).toList).flatMap fun J =>
       (List.finRange m).flatMap fun j =>
-        [J.piecewise (ω j).1 (ω j).2.2, J.piecewise (ω j).2.1 (ω j).2.2]
+        [J.piecewise (ω j).1 (Prod.snd (ω j).2),
+          J.piecewise (Prod.fst (ω j).2) (Prod.snd (ω j).2)]
 
 /-- The algorithm queries `m (2 n + 3)` points for `n` coordinates. -/
 theorem length_kmQueries (ω : Fin m → (ι → Bool) × (ι → Bool) × (ι → Bool)) :
diff --git a/Complexity/Probability/ApproximateCounting.lean b/Complexity/Probability/ApproximateCounting.lean
index 42c82ed5ea..8eb085dd73 100644
--- a/Complexity/Probability/ApproximateCounting.lean
+++ b/Complexity/Probability/ApproximateCounting.lean
@@ -100,7 +100,7 @@ structure AnswersCorrect (n c : ℕ) (a : ℕ → Prop) : Prop where
 instance : Decidable (AnswersCorrect n c a) :=
   decidable_of_iff ((a 0 ↔ 0 < c) ∧ (∀ j ≤ n, 8 * 2 ^ j ≤ c → a j) ∧
     ∀ j ≤ n, 8 * c ≤ 2 ^ j → ¬ a j)
-    ⟨fun h => ⟨h.1, h.2.1, h.2.2⟩, fun h => ⟨h.1, h.2, h.3⟩⟩
+    ⟨fun ⟨h1, h2, h3⟩ => ⟨h1, h2, h3⟩, fun h => ⟨h.1, h.2, h.3⟩⟩
 
 /-- The estimate from correct answers is at most `8` times the size of the set. -/
 theorem AnswersCorrect.estimate_le (ha : AnswersCorrect n c a) : estimate n a ≤ 8 * c := by
diff --git a/Complexity/Probability/CorrelatedSampling.lean b/Complexity/Probability/CorrelatedSampling.lean
index ae9ebd6474..e5ae0ef5cd 100644
--- a/Complexity/Probability/CorrelatedSampling.lean
+++ b/Complexity/Probability/CorrelatedSampling.lean
@@ -288,10 +288,10 @@ abbrev Cell := Σ s : S, {v // v ∈ values P s}
 noncomputable instance : DecidableEq (Cell P) := Classical.decEq _
 
 /-- The length of the interval of a cell. -/
-noncomputable def weight (c : Cell P) : ℝ≥0 := c.2.1 - predIn (values P c.1) c.2.1
+noncomputable def weight (c : Cell P) : ℝ≥0 := c.2.val - predIn (values P c.1) c.2.val
 
 /-- The cells under the graph of `t`. -/
-noncomputable def under (t : S → ℝ≥0) : Finset (Cell P) := univ.filter fun c => c.2.1 ≤ t c.1
+noncomputable def under (t : S → ℝ≥0) : Finset (Cell P) := univ.filter fun c => c.2.val ≤ t c.1
 
 /-- The cells under the graph of `P i`. -/
 noncomputable def region (i : I) : Finset (Cell P) := under P fun s => (P i s).toNNReal
diff --git a/Complexity/Probability/CorrelatedSampling/Embeddability.lean b/Complexity/Probability/CorrelatedSampling/Embeddability.lean
index 6f39fff27b..6a26a59ca8 100644
--- a/Complexity/Probability/CorrelatedSampling/Embeddability.lean
+++ b/Complexity/Probability/CorrelatedSampling/Embeddability.lean
@@ -72,11 +72,11 @@ def IsEmbeddable (P₀ : PMF (X × Y)) (P₁ : PMF ((X × Y) × (S × T))) (ε :
 
 /-- The conditional law of `s` given `x` under a joint law `J` of `((x, y), s)`. -/
 noncomputable def condX (J : PMF ((X × Y) × S)) : X → PMF S :=
-  conditionalSnd (J.map fun z => (z.1.1, z.2))
+  conditionalSnd (J.map fun z => (Prod.fst z.1, z.2))
 
 /-- The conditional law of `s` given `y` under a joint law `J` of `((x, y), s)`. -/
 noncomputable def condY (J : PMF ((X × Y) × S)) : Y → PMF S :=
-  conditionalSnd (J.map fun z => (z.1.2, z.2))
+  conditionalSnd (J.map fun z => (Prod.snd z.1, z.2))
 
 /-- The joint law `P ⊗ K` of `((x, y), s)` with `(x, y) ~ P` and `s ~ K (x, y)`. -/
 noncomputable abbrev withKernel (P : PMF (X × Y)) (K : X × Y → PMF S) : PMF ((X × Y) × S) :=
diff --git a/Complexity/Probability/Guessing.lean b/Complexity/Probability/Guessing.lean
index fe0693f576..50aeb895cb 100644
--- a/Complexity/Probability/Guessing.lean
+++ b/Complexity/Probability/Guessing.lean
@@ -50,7 +50,7 @@ theorem score_le_uniform_guess (real : PMF (Seed × (Prefix × Suffix))) (seed :
     (score : Seed → Prefix × Suffix → ℝ)
     (hscore : ∀ s z, 0 ≤ score s z ∧ score s z ≤ 1) :
     (∑ pair, (real pair).toReal * score pair.1 pair.2) ≤
-      2 * dist (real.map (fun pair => (pair.1, pair.2.1)))
+      2 * dist (real.map (fun pair => (pair.1, Prod.fst pair.2)))
         (seed.bind (fun s => (PMF.uniformOfFintype Prefix).map (s, ·))) +
       Fintype.card Suffix *
         ∑ s, (seed s).toReal * ∑ z,
diff --git a/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean b/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean
index 3c0046e9d7..6c275115ac 100644
--- a/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean
@@ -86,7 +86,7 @@ acting on the torus alone, `w ↦ (1 + E_ab) w` and `w ↦ w + e_i`. -/
 
 @[simp]
 theorem torusMove_inl (p : {p : Fin H × Fin H // p.1 ≠ p.2}) (w : Fin H → ZMod M) :
-    torusMove H M (.inl p) w = update w p.1.1 (w p.1.1 + w p.1.2) := by
+    torusMove H M (.inl p) w = update w p.val.1 (w p.val.1 + w p.val.2) := by
   simp only [torusMove, affineGenerator, Sum.elim_inl, affineSL_apply,
     SpecialLinearGroup.map_transvection, SpecialLinearGroup.transvection_mulVec, map_one, one_mul]
   exact funext fun _ ↦ by simp
diff --git a/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean b/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean
index c42f9dad82..ff6243bd4a 100644
--- a/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean
@@ -112,14 +112,14 @@ variable {P H r}
 /-- The value `a₀ + ∑ j, y ^ (j + 1) • F j` of the channel `A = (a₀, F)` at the identifier
 `y`. -/
 @[expose] def FrameChannel.eval (A : FrameChannel P H r) (y : ZMod P) : Fin H → ZMod P :=
-  A.1 + ∑ j : Fin r, y ^ (j.val + 1) • A.2.1 j
+  A.1 + ∑ j : Fin r, y ^ (j.val + 1) • A.2.val j
 
 /-- **Coordinates of a channel at `y`**: its value at `y` and its frame. The constant column is
 recovered as the value minus the frame part. -/
 @[expose] def FrameChannel.evalEquiv (y : ZMod P) :
     FrameChannel P H r ≃ (Fin H → ZMod P) × Frame P H r where
   toFun A := (A.eval y, A.2)
-  invFun p := (p.1 - ∑ j : Fin r, y ^ (j.val + 1) • p.2.1 j, p.2)
+  invFun p := (p.1 - ∑ j : Fin r, y ^ (j.val + 1) • p.2.val j, p.2)
   left_inv A := by simp [FrameChannel.eval]
   right_inv p := by simp [FrameChannel.eval]
 
@@ -202,13 +202,13 @@ value at `y`, which ranges over the whole box `ZMod L ^ H`. -/
 
 @[simp]
 theorem sliceEquiv_apply [NeZero L] (hL : L ≤ P) (y : ZMod P) (A : RetentionSlice P H r L y) :
-    sliceEquiv hL y A = (A.1.2, fun i ↦ ((A.1.eval y i).val : ZMod L)) :=
+    sliceEquiv hL y A = (A.val.2, fun i ↦ ((A.1.eval y i).val : ZMod L)) :=
   rfl
 
 /-- The frame of a channel is its frame coordinate on the slice. -/
 @[simp]
 theorem sliceEquiv_symm_apply_snd [NeZero L] (hL : L ≤ P) (y : ZMod P)
-    (p : Frame P H r × (Fin H → ZMod L)) : ((sliceEquiv hL y).symm p).1.2 = p.1 := by
+    (p : Frame P H r × (Fin H → ZMod L)) : ((sliceEquiv hL y).symm p).val.2 = p.1 := by
   have h := congrArg Prod.fst ((sliceEquiv hL y).apply_symm_apply p)
   rwa [sliceEquiv_apply] at h
 
diff --git a/Complexity/Probability/PairwiseIndependentHash/FrameRetention.lean b/Complexity/Probability/PairwiseIndependentHash/FrameRetention.lean
index 736755dd56..ba8e5224f1 100644
--- a/Complexity/Probability/PairwiseIndependentHash/FrameRetention.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/FrameRetention.lean
@@ -164,7 +164,7 @@ def polyChannelEval (s : (Fin r → Fin H → ZMod P) × (Fin H → ZMod P)) (y
 /-- A frame-conditioned channel evaluates as the unrestricted polynomial channel with the same
 columns. -/
 theorem FrameChannel.eval_eq_polyChannelEval (A : FrameChannel P H r) (y : ZMod P) :
-    A.eval y = polyChannelEval (A.2.1, A.1) y :=
+    A.eval y = polyChannelEval (A.2.val, A.1) y :=
   add_comm _ _
 
 /-- The coefficient part `M ↦ (y ↦ ∑ j, y ^ (j + 1) • M j)` of a polynomial channel, as an
@@ -208,7 +208,8 @@ has, under frame conditioning, at most its unrestricted probability divided by t
 `q_fr` [OpenAI2026LogSpace, proof of Lemma 3.1]. -/
 theorem dens_frameChannel_le (E : (Fin r → Fin H → ZMod P) × (Fin H → ZMod P) → Prop)
     [DecidablePred E] :
-    (dens {A : FrameChannel P H r | E (A.2.1, A.1)} : ℝ) ≤ dens {s | E s} / frameDensity P H r := by
+    (dens {A : FrameChannel P H r | E (A.2.val, A.1)} : ℝ) ≤
+      dens {s | E s} / frameDensity P H r := by
   have hinj : #{A : FrameChannel P H r | E (A.2.1, A.1)} ≤ #{s | E s} :=
     card_le_card_of_injOn (fun A ↦ (A.2.1, A.1)) (fun A hA ↦ by simpa using hA)
       fun A _ B _ h ↦ by
diff --git a/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean b/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean
index 30f94d1726..a1b5b8f2de 100644
--- a/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean
@@ -132,8 +132,8 @@ variable {α : ZMod P} (β : ZMod P) (hα : α ≠ 0)
 /-- The channel obtained by **substituting `α y + β`** into `A`, for `α ≠ 0`: its value at `y` is
 the value of `A` at `α y + β` (`eval_affineSubst`). -/
 def affineSubst (A : FrameChannel P H r) : FrameChannel P H r :=
-  (A.1 + ∑ j, β ^ (j.val + 1) • A.2.1 j,
-    ⟨substColumns α β A.2.1, linearIndependent_substColumns β hα A.2.2⟩)
+  (A.1 + ∑ j, β ^ (j.val + 1) • A.2.val j,
+    ⟨substColumns α β A.2.val, linearIndependent_substColumns β hα A.2.property⟩)
 
 /-- **Substitution**: the substituted channel evaluates `y` as the original channel evaluates
 `α y + β`. -/
diff --git a/Complexity/Probability/PairwiseIndependentHash/SliceGap.lean b/Complexity/Probability/PairwiseIndependentHash/SliceGap.lean
index 32f3716df8..73f0e5d587 100644
--- a/Complexity/Probability/PairwiseIndependentHash/SliceGap.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/SliceGap.lean
@@ -231,7 +231,7 @@ theorem affineMove_inl {r : ℕ} (p : {p : Fin H × Fin H // p.1 ≠ p.2})
     (q : Frame P H r × (Fin H → ZMod L)) :
     affineMove P H L r (.inl p) q =
       (Frame.mapSL (SpecialLinearGroup.transvection p.2 1) q.1,
-        update q.2 p.1.1 (q.2 p.1.1 + q.2 p.1.2)) := by
+        update q.2 p.val.1 (q.2 p.val.1 + q.2 p.val.2)) := by
   simp only [affineMove, affineGenerator, coordMove, Sum.elim_inl, Equiv.prodCongr_apply,
     Prod.map, affineSL_apply, SpecialLinearGroup.map_transvection,
     SpecialLinearGroup.transvection_mulVec, map_one, one_mul]
diff --git a/Complexity/Tactic/PolyTime/Init.lean b/Complexity/Tactic/PolyTime/Init.lean
index bcda24d45d..1908a44aaa 100644
--- a/Complexity/Tactic/PolyTime/Init.lean
+++ b/Complexity/Tactic/PolyTime/Init.lean
@@ -250,7 +250,7 @@ def applyCertificates (predicate : Name) : Aesop.RuleTac := fun input => input.g
         successProbability? := none }
     catch _ => pure ()
     finally initial.restore
-  if applications.isEmpty then throwError "no certificate for `{key.2.1}` applies"
+  if applications.isEmpty then throwError "no certificate for `{Prod.fst key.2}` applies"
   return ⟨applications⟩
 
 /-- Apply a rule with known arguments, leaving all remaining hypotheses as goals. -/

From edbbbd6117ff4b12bf27f9661d277f4ec478ab0b Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 16:29:48 +0000
Subject: [PATCH 2/3] refactor(Probabilistic): replace Prod.fst/Prod.snd
 respellings with pattern binders and accessors

---
 .../Probabilistic/Oracle/Parameter.lean       |  6 +-
 .../Probabilistic/Oracle/Substitution.lean    |  4 +-
 .../Probabilistic/OracleSimulation.lean       |  2 +-
 .../Probabilistic/Presample.lean              |  4 +-
 .../Realization/OpenOracleSimulation.lean     |  4 +-
 .../Realization/OracleSimulation.lean         |  4 +-
 .../Probabilistic/Selection.lean              | 40 +++++++------
 .../Languages/Probabilistic/Forking.lean      | 22 ++++---
 .../Probabilistic/Oracle/Simulation.lean      |  4 +-
 .../Languages/Probabilistic/Presample.lean    |  4 +-
 .../Languages/Probabilistic/Selection.lean    | 39 +++++++------
 .../Languages/Probabilistic/Simulation.lean   |  4 +-
 .../UniformLearning/KushilevitzMansour.lean   | 57 ++++++++++++-------
 .../CorrelatedSampling/Embeddability.lean     |  4 +-
 Complexity/Probability/Guessing.lean          | 12 ++--
 Complexity/Tactic/PolyTime/Init.lean          |  4 +-
 16 files changed, 124 insertions(+), 90 deletions(-)

diff --git a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
index cea8e28ff4..b57810256b 100644
--- a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
+++ b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean
@@ -104,7 +104,7 @@ theorem IsOraclePPT.run_interpret_preprocess {Caller State : Type}
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -135,7 +135,7 @@ theorem IsOraclePPT.run_interpret_preprocess_open {External Caller State : Type}
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -166,7 +166,7 @@ theorem IsOraclePPT.run_interpret_preprocess_open' {External Caller State : Type
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
index b94dd670f9..0139a19bba 100644
--- a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
+++ b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean
@@ -69,7 +69,7 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
@@ -140,7 +140,7 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open'
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/OracleSimulation.lean b/Complexity/Computability/Probabilistic/OracleSimulation.lean
index 1f68bed715..7392720b7f 100644
--- a/Complexity/Computability/Probabilistic/OracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/OracleSimulation.lean
@@ -58,7 +58,7 @@ theorem IsOraclePPTOn.run_interpret_preprocess {Operation α β Caller State : T
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
     (hresources : ComputableTidilyInPolyTime (fun pair => resources pair.1 pair.2)
diff --git a/Complexity/Computability/Probabilistic/Presample.lean b/Complexity/Computability/Probabilistic/Presample.lean
index 52166855c4..bb66f79232 100644
--- a/Complexity/Computability/Probabilistic/Presample.lean
+++ b/Complexity/Computability/Probabilistic/Presample.lean
@@ -56,7 +56,7 @@ theorem IsOraclePPTOn.run_interpret_withSampleList
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => oracle (Prod.fst pair.1) (Prod.snd pair.1) (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨⟨caller, value⟩, ⟨request, state⟩⟩ => oracle caller value request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
@@ -117,7 +117,7 @@ theorem IsOraclePPT.run_interpret_withSampleList
       (encPair (encPair input valueEncoding)
         (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => oracle (Prod.fst pair.1) (Prod.snd pair.1) (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨⟨caller, value⟩, ⟨request, state⟩⟩ => oracle caller value request state))
     (hinitial : ComputableTidilyInPolyTime initial input stateEncoding)
     (hvalues : ComputableTidilyInPolyTime values input (encList valueEncoding))
     (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a))
diff --git a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
index 5643a6dbc6..80396002dc 100644
--- a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean
@@ -102,7 +102,7 @@ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2))) :
+      (fun ⟨caller, request, state⟩ => handler caller request state)) :
     IsOraclePPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) := by
@@ -162,7 +162,7 @@ theorem isOraclePPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hhandler : IsOraclePPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)
diff --git a/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean b/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
index 258fb37c06..fb597538d5 100644
--- a/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
+++ b/Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean
@@ -111,7 +111,7 @@ theorem isPPTOn_step [Fintype Operation] {input : α ↪ List Bool}
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2))) :
+      (fun ⟨caller, request, state⟩ => handler caller request state)) :
     IsPPTOn (encPair input (encPair encFiniteConfig stateEncoding))
       (encPair encFiniteConfig stateEncoding)
       (fun pair => step machine handler pair.1 pair.2) :=
@@ -131,7 +131,7 @@ theorem isPPTOn_run [Finite Operation] {input : α ↪ List Bool}
     (hhandler : IsPPTOn
       (encPair input (encPair (encPair operationEncoding encBits) stateEncoding))
       (encPair encBits stateEncoding)
-      (fun pair => handler pair.1 (Prod.fst pair.2) (Prod.snd pair.2)))
+      (fun ⟨caller, request, state⟩ => handler caller request state))
     (hinitial : ComputableInPolyTime initial input stateEncoding)
     (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a))
     {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources)
diff --git a/Complexity/Computability/Probabilistic/Selection.lean b/Complexity/Computability/Probabilistic/Selection.lean
index f3510bb746..1a42a7174f 100644
--- a/Complexity/Computability/Probabilistic/Selection.lean
+++ b/Complexity/Computability/Probabilistic/Selection.lean
@@ -61,27 +61,33 @@ theorem IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool}
       (fun pair => OracleComp.selectStep (trials pair.1) (test pair.1) pair.2) := by
     unfold OracleComp.selectStep
     apply (htest'.countTrue htrials').map_with
-    dsimp only [OracleComp.selectUpdate, stateEncoding]
-    apply ComputableInPolyTime.prod
-    · exact ComputableInPolyTime.unary_succ.comp (by fun_prop)
-    · have hc := ComputableInPolyTime.unary_le'
-        (by fun_prop : ComputableInPolyTime
-          (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.1.2.2.2)
-          (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
-          encUnary)
-        (by fun_prop : ComputableInPolyTime
-          (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.2)
-          (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
-          encUnary)
-      simpa only [decide_eq_true_eq] using hc.ite (by fun_prop) (by fun_prop)
+    have hupd : ComputableInPolyTime
+        (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ =>
+          (pair.1.2.1 + 1,
+            if pair.1.2.2.2 ≤ pair.2 then (pair.1.2.1, pair.2) else pair.1.2.2))
+        (encPair (encPair input stateEncoding) encUnary) stateEncoding := by
+      dsimp only [stateEncoding]
+      apply ComputableInPolyTime.prod
+      · exact ComputableInPolyTime.unary_succ.comp (by fun_prop)
+      · have hc := ComputableInPolyTime.unary_le'
+          (by fun_prop : ComputableInPolyTime
+            (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.1.2.2.2)
+            (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
+            encUnary)
+          (by fun_prop : ComputableInPolyTime
+            (fun pair : (α × (ℕ × ℕ × ℕ)) × ℕ => pair.2)
+            (encPair (encPair input (encPair encUnary (encPair encUnary encUnary))) encUnary)
+            encUnary)
+        simpa only [decide_eq_true_eq] using hc.ite (by fun_prop) (by fun_prop)
+    exact hupd.of_enc_eq fun ⟨⟨_, ⟨_, _, _⟩⟩, _⟩ => rfl
   have horacle := IsOraclePPTOn.iterateWith_spec' (Operation := Empty)
     (stateEncoding := stateEncoding) (initial := fun _ => (0, 0, 0))
     (step := fun a s => ProbOracleComp.sample (OracleComp.selectStep (trials a) (test a) s))
     hcount (by dsimp only [stateEncoding]; fun_prop)
     (hstep.isOraclePPTOn (Operation := Empty))
     (fun a i state => state.1 = i ∧ state.2.1 ≤ i ∧ state.2.2 ≤ trials a)
-    (by simp) (fun a i state _ hstate next hnext =>
-      ProbComp.selectStep_bounded (trials a) (test a) i state hstate next
+    (by simp) (fun a i ⟨next, best, count⟩ _ hstate ⟨next', best', count'⟩ hnext =>
+      ProbComp.selectStep_bounded (trials a) (test a) i next best count hstate next' best' count'
         ((ProbOracleComp.support_sample _).subset hnext))
     (size := fun a => 4 * count a + trials a + 2)
     (ComputableInPolyTime.polyBounded (by fun_prop)) (by
@@ -94,7 +100,9 @@ theorem IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool}
         (OracleComp.selectStep (trials a) (test a)) (0, 0, 0)) := by
     apply IsOraclePPTOn.isPPTOn
     simpa only [ProbOracleComp.sample, OracleComp.interpret_iterate] using horacle.1
-  exact hloop.map (by dsimp only [stateEncoding]; fun_prop)
+  have hproj : ComputableInPolyTime (fun s : ℕ × ℕ × ℕ => s.2.1) stateEncoding encUnary := by
+    dsimp only [stateEncoding]; fun_prop
+  exact hloop.map (hproj.of_enc_eq fun ⟨_, _, _⟩ => rfl)
 
 /-- Selecting from an efficiently computed list charges for the whole list and each test. -/
 @[program_certificate]
diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean
index 12fe47afab..53de4254de 100644
--- a/Complexity/Languages/Probabilistic/Forking.lean
+++ b/Complexity/Languages/Probabilistic/Forking.lean
@@ -147,6 +147,9 @@ theorem IsQueryBounded.length_runWithAnswers_le (default : H)
     rw [runWithAnswers_query_bind, List.length_cons]
     exact Nat.succ_le_succ (ih _ _)
 
+/-- The final handler state produced by `runWithAnswers` on a stateful handler execution. -/
+abbrev runWithAnswersState {σ β : Type} (out : (β × σ) × List Query) : σ := out.1.2
+
 /-- **An invariant of a handler's run on a list of answers.** A program runs through a stateful
 handler whose calls are oracle programs, and the resulting program runs on a list of answers. A
 property of the handler's state and of the queries asked so far that every handler call
@@ -156,12 +159,13 @@ theorem runWithAnswers_run_interpret_invariant {ι σ β : Type} {spec : ι →
     (answers : List H) (invariant : σ → List Query → Prop)
     (step : ∀ q s queries, invariant s queries →
       invariant
-        (Prod.snd (runWithAnswers default ((handler q).run s) (answers.drop queries.length)).1)
+        (runWithAnswersState (runWithAnswers default ((handler q).run s)
+          (answers.drop queries.length)))
         (queries ++ (runWithAnswers default ((handler q).run s)
           (answers.drop queries.length)).2))
     (program : OracleComp spec β) (s : σ) (queries : List Query) (hs : invariant s queries) :
-    invariant (Prod.snd (runWithAnswers default ((interpret handler program).run s)
-        (answers.drop queries.length)).1)
+    invariant (runWithAnswersState (runWithAnswers default ((interpret handler program).run s)
+        (answers.drop queries.length)))
       (queries ++ (runWithAnswers default ((interpret handler program).run s)
         (answers.drop queries.length)).2) := by
   induction program using OracleComp.induction generalizing s queries with
@@ -329,14 +333,16 @@ theorem validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q}
     subst h
     exact ⟨rfl, hp.2⟩
 
+/-- The named query position returned by a forking-lemma program execution. -/
+abbrev forkNamedPosition {β γ : Type} (out : (Option ℕ × β) × γ) : Option ℕ := out.1.1
+
 /-- A program with explicit coins as an algorithm on coins and `q` answers, for the general
 forking lemma: the validly named position, and the result with the queries. -/
 def forkingAlgorithm {S β : Type} (default : H) (q : ℕ)
     (program : S → OracleComp (fun _ : Query => H) (Option ℕ × β)) (s : S) (h : Fin q → H) :
     Option (Fin q) × ((Option ℕ × β) × List Query) :=
-  (validIndex q (runWithAnswers default (program s) (List.ofFn h)).2.length
-      (Prod.fst (runWithAnswers default (program s) (List.ofFn h)).1),
-    runWithAnswers default (program s) (List.ofFn h))
+  let run := runWithAnswers default (program s) (List.ofFn h)
+  (validIndex q run.2.length (forkNamedPosition run), run)
 
 variable {S β : Type} [Fintype H] [Nonempty H] [DecidableEq H]
 
@@ -350,7 +356,7 @@ theorem le_add_sqrt_fork (first : PMF S)
     ((do
       let s ← first
       let run ← (interpret countingUniform (program s)).run 0
-      return (validIndex q run.2 (Prod.fst run.1)).isSome : PMF Bool) true).toReal ≤
+      return (validIndex q run.2 (forkNamedPosition run)).isSome : PMF Bool) true).toReal ≤
       q / Fintype.card H + √(q * ((Forking.fork first (forkingAlgorithm default q program)).map
         Option.isSome true).toReal) := by
   have hacc : (do
@@ -378,7 +384,7 @@ theorem mem_support_fork {first : PMF S}
     ∃ s ∈ first.support, ∃ h h' : Fin q → H, (∀ i < j, h i = h' i) ∧ h j ≠ h' j ∧
       out = runWithAnswers default (program s) (List.ofFn h) ∧
       out' = runWithAnswers default (program s) (List.ofFn h') ∧
-      Prod.fst out.1 = some j.val ∧ Prod.fst out'.1 = some j.val ∧
+      forkNamedPosition out = some j.val ∧ forkNamedPosition out' = some j.val ∧
       out.2.take (j + 1) = out'.2.take (j + 1) ∧
       ∃ query, out.2[j.val]? = some query ∧ out'.2[j.val]? = some query := by
   obtain ⟨s, hs, h, h', hagree, hne, hrun, hrun'⟩ := Forking.mem_support_fork hfork
diff --git a/Complexity/Languages/Probabilistic/Oracle/Simulation.lean b/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
index 3e9830e622..9f06db8086 100644
--- a/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
+++ b/Complexity/Languages/Probabilistic/Oracle/Simulation.lean
@@ -194,9 +194,9 @@ theorem run_interpret_run_interpret {Query' : Type} {spec' : Query' → Type}
       (fun q state => ((OracleComp.interpret
         (handler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle)
           ((inner q).run state.1)).run state.2).map
-            (fun result => (Prod.fst result.1, Prod.snd result.1, result.2)))) program).run
+            (fun ⟨⟨a, b⟩, c⟩ => (a, b, c)))) program).run
         (hidden, external)).map
-          (fun result => ((result.1, Prod.fst result.2), Prod.snd result.2)) := by
+          (fun ⟨a, b, c⟩ => ((a, b), c)) := by
   rw [OracleComp.run_interpret_run_interpret, _root_.PMF.monad_map_eq_map]
   congr 3
   funext q state
diff --git a/Complexity/Languages/Probabilistic/Presample.lean b/Complexity/Languages/Probabilistic/Presample.lean
index bf37ceb21a..4dbde95e12 100644
--- a/Complexity/Languages/Probabilistic/Presample.lean
+++ b/Complexity/Languages/Probabilistic/Presample.lean
@@ -77,7 +77,7 @@ theorem IsQueryBounded.run_interpret_presample {program : ProbOracleComp spec α
     ((PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (withSampleList fallback oracle)) program).run (s, values)).map
-          fun result => (result.1, Prod.fst result.2)) =
+          fun (result, next, _) => (result, next)) =
       (interpret (handler (fun k => StateT.lift (ProbComp.unifOracle k))
         (fun q state => source.bind fun value => oracle value q state)) program).run s := by
   induction h generalizing s with
@@ -137,7 +137,7 @@ theorem OracleComp.IsQueryBounded.run_interpret_presample {Query State Value γ
     (oracle : Value → (q : Query) → StateT State PMF (spec q)) (s : State) :
     ((Probability.PMF.iid source n).map List.ofFn).bind (fun values =>
       ((interpret (withSampleList fallback oracle) program).run (s, values)).map
-        fun result => (result.1, Prod.fst result.2)) =
+        fun (result, next, _) => (result, next)) =
       (interpret (m := StateT State PMF)
         (fun q state => source.bind fun value => oracle value q state) program).run s := by
   simpa only [interpret_interpret, ProbOracleComp.interpret_query] using
diff --git a/Complexity/Languages/Probabilistic/Selection.lean b/Complexity/Languages/Probabilistic/Selection.lean
index 882551fce4..3e53e9a412 100644
--- a/Complexity/Languages/Probabilistic/Selection.lean
+++ b/Complexity/Languages/Probabilistic/Selection.lean
@@ -53,8 +53,9 @@ universe u
 variable {Query : Type u} {spec : OracleSpec.{u, 0} Query}
 
 /-- Update the next index, best index, and best success count, preferring later indices on ties. -/
-def selectUpdate (state : ℕ × ℕ × ℕ) (successes : ℕ) : ℕ × ℕ × ℕ :=
-  (state.1 + 1, if Prod.snd state.2 ≤ successes then (state.1, successes) else state.2)
+def selectUpdate : ℕ × ℕ × ℕ → ℕ → ℕ × ℕ × ℕ
+  | (next, best, count), successes =>
+    (next + 1, if count ≤ successes then (next, successes) else (best, count))
 
 /-- Estimate one candidate and update the running empirical maximum. -/
 def selectStep (trials : ℕ) (test : ℕ → OracleComp spec Bool)
@@ -65,7 +66,7 @@ def selectStep (trials : ℕ) (test : ℕ → OracleComp spec Bool)
 When there are no candidates, return zero. -/
 def selectBest (count trials : ℕ) (test : ℕ → OracleComp spec Bool) :
     OracleComp spec ℕ :=
-  (fun state => Prod.fst state.2) <$> iterate count (selectStep trials test) (0, 0, 0)
+  (fun (_, best, _) => best) <$> iterate count (selectStep trials test) (0, 0, 0)
 
 /-- Select an empirically best value from a list, returning the fallback for an empty list. -/
 def selectFrom {α : Type} (values : List α) (trials : ℕ)
@@ -112,15 +113,16 @@ theorem sampleBest_support {α : Type} (count trials : ℕ) (source : ProbComp 
 /-- Candidate selection keeps both indices within the elapsed count and the success count within
 the trial budget on every execution, regardless of statistical estimation errors. -/
 theorem selectStep_bounded (trials : ℕ) (test : ℕ → ProbComp Bool) (i : ℕ)
-    (state : ℕ × ℕ × ℕ) (hstate : state.1 = i ∧ Prod.fst state.2 ≤ i ∧ Prod.snd state.2 ≤ trials)
-    (next : ℕ × ℕ × ℕ) (hnext : next ∈ (eval (OracleComp.selectStep trials test state)).support) :
-    next.1 = i + 1 ∧ Prod.fst next.2 ≤ i + 1 ∧ Prod.snd next.2 ≤ trials := by
+    (next best count : ℕ) (hstate : next = i ∧ best ≤ i ∧ count ≤ trials)
+    (next' best' count' : ℕ)
+    (hnext : (next', best', count') ∈
+      (eval (OracleComp.selectStep trials test (next, best, count))).support) :
+    next' = i + 1 ∧ best' ≤ i + 1 ∧ count' ≤ trials := by
   rw [OracleComp.selectStep, eval_map, PMF.mem_support_map_iff] at hnext
-  obtain ⟨successes, hsuccesses, rfl⟩ := hnext
-  have hbound := countTrue_le trials (test state.1) hsuccesses
-  dsimp only [OracleComp.selectUpdate]
-  split_ifs <;> simp_all
-  lia
+  obtain ⟨successes, hsuccesses, hupdate⟩ := hnext
+  have hbound := countTrue_le trials (test next) hsuccesses
+  dsimp only [OracleComp.selectUpdate] at hupdate
+  split_ifs at hupdate <;> simp_all <;> lia
 
 private def SelectionInvariant (trials : ℕ) (rate : ℕ → ℝ) (ε : ℝ)
     (i : ℕ) (state : ℕ × ℕ × ℕ) : Prop :=
@@ -132,12 +134,13 @@ private theorem SelectionInvariant.update {trials i : ℕ} {rate : ℕ → ℝ}
     {state : ℕ × ℕ × ℕ} (hstate : SelectionInvariant trials rate ε i state)
     (successes : ℕ) (haccurate : |(successes : ℝ) / trials - rate i| ≤ ε) :
     SelectionInvariant trials rate ε (i + 1) (OracleComp.selectUpdate state successes) := by
+  rcases state with ⟨next, best, count⟩
   obtain ⟨hindex, hzero, hchosen, hall⟩ := hstate
   obtain ⟨hlower, hupper⟩ := abs_le.mp haccurate
   have htrials : (0 : ℝ) ≤ trials := by positivity
-  dsimp only [SelectionInvariant, OracleComp.selectUpdate]
+  dsimp only [SelectionInvariant, OracleComp.selectUpdate] at hindex hzero hchosen hall ⊢
   split_ifs with hscore
-  · have hcompare : (state.2.2 : ℝ) / trials ≤ successes / trials :=
+  · have hcompare : (count : ℝ) / trials ≤ successes / trials :=
       div_le_div_of_nonneg_right (by exact_mod_cast hscore) htrials
     refine ⟨by lia, by simp, fun _ => ⟨by lia, ?_⟩, ?_⟩
     · simpa only [hindex] using (show (successes : ℝ) / trials ≤ rate i + ε by linarith)
@@ -152,10 +155,10 @@ private theorem SelectionInvariant.update {trials i : ℕ} {rate : ℕ → ℝ}
         linarith
   · have hi : 0 < i := by
       by_contra h
-      have hz := hzero (by lia)
-      simp [hz] at hscore
-    have hcompare : (successes : ℝ) / trials ≤ state.2.2 / trials :=
-      div_le_div_of_nonneg_right (by exact_mod_cast (show successes ≤ state.2.2 by lia)) htrials
+      obtain ⟨rfl, rfl⟩ := hzero (by lia)
+      simp at hscore
+    have hcompare : (successes : ℝ) / trials ≤ count / trials :=
+      div_le_div_of_nonneg_right (by exact_mod_cast (show successes ≤ count by lia)) htrials
     obtain ⟨hchosenIndex, hchosenRate⟩ := hchosen hi
     refine ⟨by lia, by simp, fun _ => ⟨by lia, hchosenRate⟩, ?_⟩
     intro j hj
@@ -194,7 +197,7 @@ theorem selectBest_error_le (count trials : ℕ) (hcount : 0 < count)
   refine le_trans ?_ hrun
   apply ENNReal.toReal_mono (Probability.PMF.toOuterMeasure_ne_top _ _)
   apply MeasureTheory.measure_mono
-  intro state hbad hstate
+  rintro ⟨next, best, count⟩ hbad hstate
   obtain ⟨_, _, hchosen, hall⟩ := hstate
   obtain ⟨hindex, hselected⟩ := hchosen hcount
   apply hbad
diff --git a/Complexity/Languages/Probabilistic/Simulation.lean b/Complexity/Languages/Probabilistic/Simulation.lean
index 05e4a9fd14..58692ee1a9 100644
--- a/Complexity/Languages/Probabilistic/Simulation.lean
+++ b/Complexity/Languages/Probabilistic/Simulation.lean
@@ -232,9 +232,9 @@ theorem run_interpret_run_interpret {κ : Type w} {target : OracleSpec.{w, v} κ
     (oracle : (q : κ) → StateT External m (target q))
     (program : OracleComp spec α) (hidden : Hidden) (external : External) :
     (interpret oracle ((interpret handler program).run hidden)).run external =
-      (fun result => ((result.1, Prod.fst result.2), Prod.snd result.2)) <$>
+      (fun ⟨a, b, c⟩ => ((a, b), c)) <$>
         (interpret (m := StateT (Hidden × External) m) (fun q state =>
-          (fun result => (Prod.fst result.1, Prod.snd result.1, result.2)) <$>
+          (fun ⟨⟨a, b⟩, c⟩ => (a, b, c)) <$>
             (interpret oracle ((handler q).run state.1)).run state.2) program).run
           (hidden, external) := by
   induction program using OracleComp.induction generalizing hidden external with
diff --git a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
index 9a7d42a908..bfbb34cd67 100644
--- a/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
+++ b/Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean
@@ -237,9 +237,10 @@ samples `ω j = (x, y, z)`: the average of `g (x, z) χ_S(x) g (y, z) χ_S(y)`,
 the coordinates in `J` from `x` and the others from `z`. -/
 noncomputable def bucketEstimate (g : (ι → Bool) → Bool)
     (ω : Fin m → (ι → Bool) × (ι → Bool) × (ι → Bool)) (J S : Finset ι) : ℝ :=
-  (∑ j, signVal (g (J.piecewise (ω j).1 (Prod.snd (ω j).2))) * chi ℝ S (ω j).1 *
-    (signVal (g (J.piecewise (Prod.fst (ω j).2) (Prod.snd (ω j).2))) *
-      chi ℝ S (Prod.fst (ω j).2))) / m
+  (∑ j,
+    let (x, y, z) := ω j
+    signVal (g (J.piecewise x z)) * chi ℝ S x *
+      (signVal (g (J.piecewise y z)) * chi ℝ S y)) / m
 
 /-- The empirical Fourier coefficient of `g` on `S` from the first points of the samples. -/
 noncomputable def sampleCoeff (g : (ι → Bool) → Bool)
@@ -266,15 +267,20 @@ noncomputable def kmQueries (ω : Fin m → (ι → Bool) × (ι → Bool) × (
   (List.finRange m).map (fun j => (ω j).1) ++
     (searchLevels (univ : Finset ι).toList).flatMap fun J =>
       (List.finRange m).flatMap fun j =>
-        [J.piecewise (ω j).1 (Prod.snd (ω j).2),
-          J.piecewise (Prod.fst (ω j).2) (Prod.snd (ω j).2)]
+        let (x, y, z) := ω j
+        [J.piecewise x z, J.piecewise y z]
 
 /-- The algorithm queries `m (2 n + 3)` points for `n` coordinates. -/
 theorem length_kmQueries (ω : Fin m → (ι → Bool) × (ι → Bool) × (ι → Bool)) :
     (kmQueries ω).length = m * (2 * Fintype.card ι + 3) := by
+  have hlen (J : Finset ι) :
+      ((List.finRange m).map fun j =>
+        (let (x, y, z) := ω j; [J.piecewise x z, J.piecewise y z]).length) =
+      (List.finRange m).map fun _ => 2 :=
+    List.map_congr_left fun j _ => by rcases ω j with ⟨x, y, z⟩; rfl
   simp only [kmQueries, List.length_append, List.length_map, List.length_finRange,
-    List.length_flatMap, List.length_cons, List.length_nil, List.map_const', List.sum_replicate,
-    smul_eq_mul, length_searchLevels, length_toList, card_univ]
+    List.length_flatMap, hlen, List.map_const', List.sum_replicate, smul_eq_mul,
+    length_searchLevels, length_toList, card_univ]
   ring
 
 /-- The hypothesis depends only on the answers at the queried points. -/
@@ -287,19 +293,22 @@ theorem kmHypothesis_congr (θ : ℝ) (ω : Fin m → (ι → Bool) × (ι → B
     funext S
     simp only [sampleCoeff, empiricalCoeff, examples_apply, hx]
   have hmem (J : Finset ι) (hJ : J ∈ searchLevels (univ : Finset ι).toList) (j : Fin m)
-      (x : ι → Bool)
-      (hx : x ∈ [J.piecewise (ω j).1 (ω j).2.2, J.piecewise (ω j).2.1 (ω j).2.2]) :
-      g x = g' x :=
-    h x (List.mem_append_right _ (List.mem_flatMap.2
-      ⟨J, hJ, List.mem_flatMap.2 ⟨j, List.mem_finRange j, hx⟩⟩))
+      (p : ι → Bool)
+      (hp : p ∈ (let (x, y, z) := ω j; [J.piecewise x z, J.piecewise y z])) :
+      g p = g' p :=
+    h p (List.mem_append_right _ (List.mem_flatMap.2
+      ⟨J, hJ, List.mem_flatMap.2 ⟨j, List.mem_finRange j, hp⟩⟩))
   have hcand : kmCandidates g θ ω = kmCandidates g' θ ω := by
     refine bucketSearch_congr fun J hJ S => ?_
-    have h₁ (j : Fin m) : g (J.piecewise (ω j).1 (ω j).2.2) = g' (J.piecewise (ω j).1 (ω j).2.2) :=
-      hmem J hJ j _ (by simp)
-    have h₂ (j : Fin m) :
-        g (J.piecewise (ω j).2.1 (ω j).2.2) = g' (J.piecewise (ω j).2.1 (ω j).2.2) :=
-      hmem J hJ j _ (by simp)
-    simp only [bucketEstimate, h₁, h₂]
+    simp only [bucketEstimate]
+    congr 1
+    refine Finset.sum_congr rfl fun j _ => ?_
+    rcases hωj : ω j with ⟨x, y, z⟩
+    have h₁ : g (J.piecewise x z) = g' (J.piecewise x z) :=
+      hmem J hJ j _ (by simp [hωj])
+    have h₂ : g (J.piecewise y z) = g' (J.piecewise y z) :=
+      hmem J hJ j _ (by simp [hωj])
+    simp only [h₁, h₂]
   simp only [kmHypothesis, hcoeff, hcand]
 
 variable (ι m) in
@@ -420,10 +429,14 @@ theorem uniform_not_accurate_le (f : (ι → Bool) → Bool) (θ : ℝ) (m : ℕ
   have hbucket (J S : Finset ι) :
       μ {ω | θ ^ 2 / 4 ≤ |bucketEstimate f ω J S - bucketWeight F J S|} ≤ ENNReal.ofReal c := by
     have h := PMF.uniform_abs_sum_div_sub_expect_ge_le
-      (fun p : (ι → Bool) × (ι → Bool) × (ι → Bool) =>
-        F (J.piecewise p.1 p.2.2) * chi ℝ S p.1 * (F (J.piecewise p.2.1 p.2.2) * chi ℝ S p.2.1))
-      (fun p => abs_signVal_mul_chi_mul_le_one _ _ S _ _) hm hγ
-    rw [← bucketWeight_eq_expect_sample, hexp] at h
+      (fun ((x, y, z) : (ι → Bool) × (ι → Bool) × (ι → Bool)) =>
+        F (J.piecewise x z) * chi ℝ S x * (F (J.piecewise y z) * chi ℝ S y))
+      (fun (x, y, z) => abs_signVal_mul_chi_mul_le_one _ _ S _ _) hm hγ
+    rw [show (𝔼 p : (ι → Bool) × (ι → Bool) × (ι → Bool),
+        let (x, y, z) := p
+        F (J.piecewise x z) * chi ℝ S x * (F (J.piecewise y z) * chi ℝ S y)) =
+        bucketWeight F J S by
+      rw [bucketWeight_eq_expect_sample], hexp] at h
     exact h
   -- one sample coefficient
   have hcoeff (S : Finset ι) :
diff --git a/Complexity/Probability/CorrelatedSampling/Embeddability.lean b/Complexity/Probability/CorrelatedSampling/Embeddability.lean
index 6a26a59ca8..d38a134c5e 100644
--- a/Complexity/Probability/CorrelatedSampling/Embeddability.lean
+++ b/Complexity/Probability/CorrelatedSampling/Embeddability.lean
@@ -72,11 +72,11 @@ def IsEmbeddable (P₀ : PMF (X × Y)) (P₁ : PMF ((X × Y) × (S × T))) (ε :
 
 /-- The conditional law of `s` given `x` under a joint law `J` of `((x, y), s)`. -/
 noncomputable def condX (J : PMF ((X × Y) × S)) : X → PMF S :=
-  conditionalSnd (J.map fun z => (Prod.fst z.1, z.2))
+  conditionalSnd (J.map (Prod.map Prod.fst id))
 
 /-- The conditional law of `s` given `y` under a joint law `J` of `((x, y), s)`. -/
 noncomputable def condY (J : PMF ((X × Y) × S)) : Y → PMF S :=
-  conditionalSnd (J.map fun z => (Prod.snd z.1, z.2))
+  conditionalSnd (J.map (Prod.map Prod.snd id))
 
 /-- The joint law `P ⊗ K` of `((x, y), s)` with `(x, y) ~ P` and `s ~ K (x, y)`. -/
 noncomputable abbrev withKernel (P : PMF (X × Y)) (K : X × Y → PMF S) : PMF ((X × Y) × S) :=
diff --git a/Complexity/Probability/Guessing.lean b/Complexity/Probability/Guessing.lean
index 50aeb895cb..c8a3addef0 100644
--- a/Complexity/Probability/Guessing.lean
+++ b/Complexity/Probability/Guessing.lean
@@ -50,7 +50,7 @@ theorem score_le_uniform_guess (real : PMF (Seed × (Prefix × Suffix))) (seed :
     (score : Seed → Prefix × Suffix → ℝ)
     (hscore : ∀ s z, 0 ≤ score s z ∧ score s z ≤ 1) :
     (∑ pair, (real pair).toReal * score pair.1 pair.2) ≤
-      2 * dist (real.map (fun pair => (pair.1, Prod.fst pair.2)))
+      2 * dist (real.map (fun (s, p, _) => (s, p)))
         (seed.bind (fun s => (PMF.uniformOfFintype Prefix).map (s, ·))) +
       Fintype.card Suffix *
         ∑ s, (seed s).toReal * ∑ z,
@@ -65,8 +65,11 @@ theorem score_le_uniform_guess (real : PMF (Seed × (Prefix × Suffix))) (seed :
     (Classical.choose_spec (Finset.exists_max_image Finset.univ
       (fun suffix => score s (initial, suffix)) Finset.univ_nonempty)).2 suffix (Finset.mem_univ _)
   let ideal := seed.bind (fun s => (PMF.uniformOfFintype Prefix).map (s, ·))
+  have hmap : (fun pair : Seed × (Prefix × Suffix) => (pair.1, pair.2.1)) =
+      fun (s, p, _) => (s, p) :=
+    funext fun ⟨_, _, _⟩ => rfl
   have hchange := abs_sum_mul_sub_le
-    (real.map (fun pair => (pair.1, pair.2.1))) ideal best
+    (real.map (fun (s, p, _) => (s, p))) ideal best
     (bound := 1) (fun pair => by
       rw [abs_of_nonneg (hscore _ _).1]
       exact (hscore _ _).2)
@@ -92,8 +95,9 @@ theorem score_le_uniform_guess (real : PMF (Seed × (Prefix × Suffix))) (seed :
     _ ≤ ∑ pair, (real pair).toReal * best (pair.1, pair.2.1) :=
       Finset.sum_le_sum (fun pair _ =>
         mul_le_mul_of_nonneg_left (hbest _ _ _) ENNReal.toReal_nonneg)
-    _ = ∑ pair, ((real.map (fun pair => (pair.1, pair.2.1))) pair).toReal * best pair :=
-      (sum_map_mul _ _ _).symm
+    _ = ∑ pair, ((real.map (fun (s, p, _) => (s, p))) pair).toReal * best pair := by
+      rw [← hmap]
+      exact (sum_map_mul _ _ _).symm
     _ ≤ (∑ pair, (ideal pair).toReal * best pair) + 2 * dist _ ideal := by
       have h := (le_abs_self _).trans hchange
       linarith
diff --git a/Complexity/Tactic/PolyTime/Init.lean b/Complexity/Tactic/PolyTime/Init.lean
index 1908a44aaa..60d2750aa0 100644
--- a/Complexity/Tactic/PolyTime/Init.lean
+++ b/Complexity/Tactic/PolyTime/Init.lean
@@ -231,7 +231,7 @@ metavariable assignments until the surrounding proof search has also succeeded.
 def applyCertificates (predicate : Name) : Aesop.RuleTac := fun input => input.goal.withContext do
   let target := (← instantiateMVars (← input.goal.getType)).consumeMData
   unless target.isAppOf predicate do throwError "expected an efficiency goal for {predicate}"
-  let key ← efficiencyKey target
+  let key@(_, head, _) ← efficiencyKey target
   let initial ← saveState
   let mut applications := #[]
   for (certificate, eager) in (certificateExt.getState (← getEnv)).getD key #[] do
@@ -250,7 +250,7 @@ def applyCertificates (predicate : Name) : Aesop.RuleTac := fun input => input.g
         successProbability? := none }
     catch _ => pure ()
     finally initial.restore
-  if applications.isEmpty then throwError "no certificate for `{Prod.fst key.2}` applies"
+  if applications.isEmpty then throwError "no certificate for `{head}` applies"
   return ⟨applications⟩
 
 /-- Apply a rule with known arguments, leaving all remaining hypotheses as goals. -/

From 8b4dd3bde4893e0197769a36d195e7d69dfc2eea Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 31 Oct 2026 16:34:38 +0000
Subject: [PATCH 3/3] refactor(Languages/Probabilistic/Forking): add
 runWithAnswersOutput depth-1 accessor

---
 Complexity/Languages/Probabilistic/Forking.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Complexity/Languages/Probabilistic/Forking.lean b/Complexity/Languages/Probabilistic/Forking.lean
index 53de4254de..354b3dfc10 100644
--- a/Complexity/Languages/Probabilistic/Forking.lean
+++ b/Complexity/Languages/Probabilistic/Forking.lean
@@ -147,8 +147,12 @@ theorem IsQueryBounded.length_runWithAnswers_le (default : H)
     rw [runWithAnswers_query_bind, List.length_cons]
     exact Nat.succ_le_succ (ih _ _)
 
+/-- The result component of a `runWithAnswers` output pair `(result, queries)`. -/
+abbrev runWithAnswersOutput {α γ : Type} (out : α × γ) : α := out.1
+
 /-- The final handler state produced by `runWithAnswers` on a stateful handler execution. -/
-abbrev runWithAnswersState {σ β : Type} (out : (β × σ) × List Query) : σ := out.1.2
+abbrev runWithAnswersState {σ β : Type} (out : (β × σ) × List Query) : σ :=
+  (runWithAnswersOutput out).2
 
 /-- **An invariant of a handler's run on a list of answers.** A program runs through a stateful
 handler whose calls are oracle programs, and the resulting program runs on a list of answers. A
@@ -334,7 +338,8 @@ theorem validIndex_eq_some {q count : ℕ} {position : Option ℕ} {j : Fin q}
     exact ⟨rfl, hp.2⟩
 
 /-- The named query position returned by a forking-lemma program execution. -/
-abbrev forkNamedPosition {β γ : Type} (out : (Option ℕ × β) × γ) : Option ℕ := out.1.1
+abbrev forkNamedPosition {β γ : Type} (out : (Option ℕ × β) × γ) : Option ℕ :=
+  (runWithAnswersOutput out).1
 
 /-- A program with explicit coins as an algorithm on coins and `q` answers, for the general
 forking lemma: the validly named position, and the result with the queries. -/