refactor(Foundations,Probability,Machines): place shared helper lemmas

Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Init
 public import Complexity.Computability.Complexity.FineGrained.SparseParitySchedule
+import Complexity.Foundations.Data.Nat.Log
 import Mathlib.Analysis.Complex.ExponentialBounds
 
 /-!
@@ -92,7 +93,6 @@ public section
 namespace Cslib.Complexity.SubexponentialSAT.ReplacementParams
 
 open Cslib.Complexity.SubexponentialSAT
-open Cslib.Logic.PL (clog_two_le_two_mul_of_le_two_mul)
 
 /-! ### 1. Free-variable (`n / 2 ≤ n' ≤ n`) to original-variable (`n`) `rowCost` transfer -/
 
@@ -118,7 +118,7 @@ theorem Feasible.mul_rowCost_le_of_le_two_mul {β n n' b_occ w_width M' : ℕ}
   have hsqrt_le : Real.sqrt (Nat.clog 2 n) ≤ 2 * Real.sqrt (Nat.clog 2 n') := by
     have hclog_le : (Nat.clog 2 n : ℝ) ≤ (2 : ℝ) ^ 2 * (Nat.clog 2 n' : ℝ) := by
       have hnat : Nat.clog 2 n ≤ 2 * Nat.clog 2 n' :=
-        clog_two_le_two_mul_of_le_two_mul hn_le (by omega)
+        Nat.clog_two_le_two_mul_of_le_two_mul hn_le (by omega)
       have hcast : (Nat.clog 2 n : ℝ) ≤ 2 * (Nat.clog 2 n' : ℝ) := by exact_mod_cast hnat
       have hnn : (0 : ℝ) ≤ (Nat.clog 2 n' : ℝ) := Nat.cast_nonneg _
       linarith

Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Computability.Complexity.FineGrained.SparseBranchSchedule
 public import Complexity.Logics.Propositional.CNF.SparseParityCounter
+import Complexity.Foundations.Data.Nat.Log
 
 /-!
 # Section 6.3 compiled CNF parity-row schedule feasibility and domain-examination bounds
@@ -433,19 +434,6 @@ theorem CNF.exists_greedy_parityRowSystem_branch_schedule {β : ℕ} (hβ : 1 
 
 /-! ### 4. Unconditional polylogarithmic schedule discharge for `B ≤ C_B * (Nat.clog 2 n) ^ β_B` -/
 
-/-- When `n ≤ 2 * n'` and `2 ≤ n'`, `Nat.clog 2 n ≤ 2 * Nat.clog 2 n'`. -/
-theorem clog_two_le_two_mul_of_le_two_mul {n n' : ℕ} (hn : n ≤ 2 * n') (hn' : 2 ≤ n') :
-    Nat.clog 2 n ≤ 2 * Nat.clog 2 n' := by
-  have h1 : 1 ≤ Nat.clog 2 n' :=
-    (Nat.lt_clog_iff_pow_lt one_lt_two).mpr (by omega : 2 ^ 0 < n')
-  have h2 : n ≤ 2 ^ (Nat.clog 2 n' + 1) := by
-    calc n ≤ 2 * n' := hn
-      _ ≤ 2 * 2 ^ Nat.clog 2 n' := Nat.mul_le_mul_left 2 (Nat.le_pow_clog one_lt_two n')
-      _ = 2 ^ (Nat.clog 2 n' + 1) := (pow_succ' 2 _).symm
-  have h3 : Nat.clog 2 n ≤ Nat.clog 2 n' + 1 :=
-    (Nat.clog_le_iff_le_pow one_lt_two).mpr h2
-  omega
-
 /-- Coefficient for the polynomial bound on `initialRowWeightBound B m` when
 `B ≤ C_B * (Nat.clog 2 n) ^ β_B` and `m ≤ B * n`. -/
 def CNF.initialRowWeightCoeff (C_B β_B : ℕ) : ℕ :=
@@ -546,7 +534,7 @@ private theorem parityBranchThreshold_succ_and_width_le_clog_pow {n n' m B W k C
           ring
   have hlam_pow : lam ^ (2 * β_B + 4) ≤ 2 ^ (2 * β_B + 4) * lam' ^ (2 * β_B + 4) := by
     calc lam ^ (2 * β_B + 4) ≤ (2 * lam') ^ (2 * β_B + 4) :=
-          Nat.pow_le_pow_left (clog_two_le_two_mul_of_le_two_mul hn_le hn') _
+          Nat.pow_le_pow_left (Nat.clog_two_le_two_mul_of_le_two_mul hn_le hn') _
       _ = 2 ^ (2 * β_B + 4) * lam' ^ (2 * β_B + 4) := mul_pow 2 lam' _
   have hthresh_lam' :
       CNF.parityBranchThreshold k W n + 1 ≤ Nat.clog 2 n' ^ (2 * β_B + 5) := by

Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingData
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingCounts
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingClauseVertices
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!
@@ -67,7 +68,7 @@ private theorem placed_occurrence_routes (pcs : List PositivePlacedClause)
     rfl
   change pc.1.zipIdx.map (fun x => (pcs.getD i ([], (0, 0), [])).2.2.getD x.2 []) = _
   rw [hg]
-  exact map_getD_zipIdx pc.1 pc.2.2 [] (hc pc (List.mem_of_getElem? hi'))
+  exact List.map_getD_zipIdx pc.1 pc.2.2 [] (hc pc (List.mem_of_getElem? hi'))
 
 /-- The occurrence-indexed view has exactly the compiler's actual position and route lists. -/
 theorem positiveFormulaDrawing_drawing (φ : CNF ℕ) (d : Graph.OrthogonalDrawing) :

Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingClauseVertices.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingVertexBoxes
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 import Mathlib.Data.List.Nodup
 
@@ -43,24 +44,14 @@ theorem clauseGeometry_clause_length (φ : CNF ℕ) (d : Graph.OrthogonalDrawing
   simpa only [clauseGeometry, collaredPrefixGeometry, profilePrefixGeometry,
     LocalGeometry.toPrefix, List.length_map] using profileGeometry_clause_length (clauseProfile c)
 
-/-- Mapping `ys.getD a.2 fallback` over `xs.zipIdx` recovers `ys` when `ys.length = xs.length`. -/
-theorem map_getD_zipIdx {A B : Type*} (xs : List A) (ys : List B) (fallback : B)
-    (hlen : ys.length = xs.length) :
-    (xs.zipIdx.map fun a => ys.getD a.2 fallback) = ys := by
-  apply List.ext_getElem
-  · simpa using hlen.symm
-  · intro i hi hj
-    simp only [List.getElem_map, List.getElem_zipIdx, Nat.zero_add]
-    rw [List.getD_eq_getElem _ _ hj]
-
 /-- A clause block lists precisely the translated local clause positions in order. -/
 theorem positiveClauseBlock_positions (φ : CNF ℕ) (d : Graph.OrthogonalDrawing)
     (i : ℕ) (c : Clause ℕ) :
     ((positiveClauseBlock φ d i c).map fun pc => pc.2.1) =
       (clauseGeometry φ d i c).clausePositions.map (positiveBoxOrigin φ d i + ·) := by
   simp only [positiveClauseBlock, List.map_map, Function.comp_def]
   have he := congrArg (List.map (positiveBoxOrigin φ d i + ·))
-    (map_getD_zipIdx (profileFormula (clauseProfile c))
+    (List.map_getD_zipIdx (profileFormula (clauseProfile c))
       (clauseGeometry φ d i c).clausePositions (0, 0) (clauseGeometry_clause_length φ d i c))
   simpa only [List.map_map, Function.comp_def, LocalGeometry.clausePosition] using he
 

Complexity/Computability/Interactive/Plain.lean

@@ -142,12 +142,6 @@ private theorem runLaw_output {s : Spec} {StmtIn StmtOut : Type}
   · exact e.elim
   · rfl
 
-/-- A uniform upper bound on `(f a).toOuterMeasure t` bounds `(p.bind f).toOuterMeasure t`. -/
-theorem toOuterMeasure_bind_le {α β : Type} (p : PMF α) (f : α → PMF β) (t : Set β)
-    {K : ℝ≥0∞} (h : ∀ a, (f a).toOuterMeasure t ≤ K) : (p.bind f).toOuterMeasure t ≤ K := by
-  rw [PMF.toOuterMeasure_bind_apply]
-  exact Probability.PMF.tsum_mul_le_of_forall_le _ h
-
 private theorem toOuterMeasure_bind_pure {α β : Type} (p : PMF α) (g : α → β) (t : Set β) :
     (p.bind fun a => PMF.pure (g a)).toOuterMeasure t = p.toOuterMeasure (g ⁻¹' t) := by
   rw [← PMF.toOuterMeasure_map_apply]
@@ -176,7 +170,7 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s)
     simp [runStrategy, hw]
   | .prover M I :: s, smp, ε, S, wins, h, hS, _, st => by
     simp only [runStrategy, plainLaw_bind]
-    refine toOuterMeasure_bind_le _ _ _ fun p => ?_
+    refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun p => ?_
     rcases p with ⟨msg, st'⟩
     simp only [plainLaw_pure]
     rw [toOuterMeasure_bind_pure]
@@ -195,7 +189,7 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s)
         rw [Set.indicator_of_mem hc]
         exact Probability.PMF.toOuterMeasure_le_one _ _
       · rw [Set.indicator_of_notMem hc, zero_add]
-        refine toOuterMeasure_bind_le _ _ _ fun st' => ?_
+        refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun st' => ?_
         simp only [plainLaw_pure]
         rw [toOuterMeasure_bind_pure]
         exact rbrFrom_le s smp.2 ε.2 (fun p => S (some (c, p))) (fun τ => wins (c, τ)) (h.2 c) hc
@@ -220,7 +214,7 @@ theorem Verifier.RbrSound.sound {s : Spec} {StmtIn StmtOut : Type}
   obtain ⟨S, hinit, hround⟩ := h
   intro x hx α P
   rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_bind]
-  exact toOuterMeasure_bind_le _ _ _ fun st => rbrFrom_le s V.samplers ε (S x) _ (hround x)
-    (hinit x hx) st
+  exact Probability.PMF.toOuterMeasure_bind_le _ _ _ fun st =>
+    rbrFrom_le s V.samplers ε (S x) _ (hround x) (hinit x hx) st
 
 end Cslib.Interactive

Complexity/Computability/Interactive/Sequential.lean

@@ -716,7 +716,7 @@ theorem Verifier.KnowledgeSound.append {V₁ : Verifier OracleSpec.empty s₁ S
     congr 1
     ext r₂
     cases hout : V₁.outputOn x r₁.1 <;> simp [T₁, Spec.Transcript.split_append, hout]
-  · refine toOuterMeasure_bind_le _ _ _ fun r₁ => ?_
+  · refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun r₁ => ?_
     rw [PMF.toOuterMeasure_map_apply]
     cases hout : V₁.outputOn x r₁.1 with
     | none =>

Complexity/Computability/Machines/Turing/MultiTape/Encodings/Length.lean

@@ -23,6 +23,8 @@ certificate, in terms of the input.
 * `Turing.MultiTapeTM.length_encList`: the exact length.
 * `Turing.MultiTapeTM.sum_length_le_length_encList`: the encoded elements are no longer, in total,
   than the encoded list.
+* `Turing.MultiTapeTM.length_unframe_add_dropFrame_le`: the unframed prefix and remaining suffix
+  of any bit list satisfy `2 * (unframe v).length + (dropFrame v).length ≤ v.length`.
 -/
 
 @[expose] public section
@@ -50,4 +52,15 @@ theorem sum_length_le_length_encList (l : List α) :
   | nil => simp
   | cons a l ih => simp only [List.map_cons, List.sum_cons]; omega
 
+/-- The unframed prefix and remaining suffix of any bit list satisfy
+`2 * (unframe v).length + (dropFrame v).length ≤ v.length`. -/
+theorem length_unframe_add_dropFrame_le :
+    ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length
+  | [] | [true] => by simp [unframe, dropFrame]
+  | false :: v => by simp [unframe, dropFrame]
+  | true :: b :: v => by
+    have ih := length_unframe_add_dropFrame_le v
+    simp only [unframe, dropFrame, List.length_cons]
+    omega
+
 end Turing.MultiTapeTM

Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeLoops.lean

@@ -31,16 +31,6 @@ private theorem unaryWordCertificate {α : Type} {input : α ↪ List Bool} {cou
     ComputableInPolyTime (fun x => List.replicate (count x) true) input encBits := by
   exact h.of_enc_eq fun _ => rfl
 
-private theorem foldlCapture {π β α : Type} (par : π) (step : π → β → α → β)
-    (list : List α) (init : β) :
-    list.foldl (fun state value => (state.1, step state.1 state.2 value)) (par, init) =
-      (par, list.foldl (step par) init) := by
-  induction list generalizing init with
-  | nil => rfl
-  | cons a list ih =>
-    simp only [List.foldl_cons]
-    exact ih (step par init a)
-
 namespace ComputableInPolyTime
 
 /-- A unary-output certificate bounds the actual numeric value by a polynomial in input size. -/
@@ -49,6 +39,12 @@ theorem polyBounded {α : Type*} {input : α ↪ List Bool} {f : α → ℕ}
     PolyBounded (fun x => (input x).length) f := by
   simpa only [encUnary_apply, List.length_replicate] using hf.polyBounded_length
 
+/-- A unary-output polynomial-time function is polynomially bounded in its unary input. -/
+theorem polynomiallyBounded {f : ℕ → ℕ} (hf : ComputableInPolyTime f encUnary encUnary) :
+    PolynomiallyBounded f :=
+  (show PolyBounded (fun n : ℕ => n) f by
+    simpa only [encUnary_apply, List.length_replicate] using hf.polyBounded).polynomiallyBounded
+
 
 /-- A polynomial bound on the encoded accumulators of reachable prefixes suffices for a
 uniform polynomial-time fold. The list and callback encodings are preserved. -/
@@ -136,12 +132,12 @@ theorem foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪
     (step := fun state value => (state.1, step state.1 state.2 value))
     hlist hstart hjoint (B := C) (PolyBounded.of_forall_le c d hC) (by
       intro x i hi
-      simp only [foldlCapture, length_encPair]
+      simp only [List.foldl_keep_fst, length_encPair]
       dsimp [C]
       exact Nat.add_le_add_left (hstates x i hi) _)
   have hsecond : ComputableInPolyTime (fun p : π × β => p.2) (encPair encP encB) encB :=
     ComputableInPolyTime.snd encP encB
-  simpa only [Function.comp_def, foldlCapture] using ComputableInPolyTime.comp hsecond hfold
+  simpa only [Function.comp_def, List.foldl_keep_fst] using ComputableInPolyTime.comp hsecond hfold
 
 /-- A computed captured parameter and a unary loop count give a uniform loop when every
 reachable iterate has polynomially bounded encoded size. -/

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean

@@ -24,6 +24,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size
+import Complexity.Foundations.Data.List.Fold
 import Mathlib.Data.List.GetD
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
@@ -472,7 +473,7 @@ private theorem exists_computableInO_signedMeasJet :
         (evalMeasPayload (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 i, pa.1)).elim pa.2
           fun y => addJet pa.1.2.1.1 pa.1.2.1.2.1 pa.2 y) := by
       funext pa i; cases evalMeasPayload _ <;> rfl
-    rw [hfn]; exact foldl_keep_fst
+    rw [hfn]; exact List.foldl_keep_fst
       (fun (m : MeasStepCtx) (acc : JetRows) (i : ℕ) =>
         (evalMeasPayload (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 i, m)).elim acc
           (fun y => addJet m.2.1.1 m.2.1.2.1 acc y))
@@ -683,7 +684,7 @@ private theorem exists_computableInO_nodeJet :
       (eSubAcc (SubsetPairFold.runPrefix subsetPairStepBody qs.2.1.1 qs.1 j
         (qs.2, zeroJet qs.2.2.2.1.1 qs.2.2.2.1.2.1)).2.2).length ≤ B_sub qs := by
     intro qs j hj; rw [SubsetPairFold.runPrefix_acc]; simp only [subsetPairStepBody_eq]
-    rw [foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
+    rw [List.foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
       addJet s.2.2.1.1 s.2.2.1.2.1 acc
         (evalSignedMeasJet (SubsetPairFold.unrankSubsetPair qs.2.1.1 qs.1 i, s)))]
     have hf_le := length_encJetRows_foldl_optAddJet_le (J := qs.2.2.2.1.1) (ℓ := qs.2.2.2.1.2.1)
@@ -731,7 +732,7 @@ private theorem exists_computableInO_nodeJet :
         (Nat.mul_le_mul_left co (Nat.pow_le_pow_left (Nat.add_le_add_right hinp_len 1) do_))
       have hfst_eq : inp.2.1 = qs.2 := by
         dsimp only [inp]; rw [SubsetPairFold.runPrefix_acc]; simp only [subsetPairStepBody_eq]
-        rw [foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
+        rw [List.foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
           addJet s.2.2.1.1 s.2.2.1.2.1 acc
             (evalSignedMeasJet (SubsetPairFold.unrankSubsetPair qs.2.1.1 qs.1 i, s)))]
       have hdc_len : (eDC (inp.1, inp.2.1)).length ≤ L_dc qs := by

Complexity/Computability/PolyTime/CommonCountingAccum.lean

@@ -17,6 +17,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fo
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size
+import Complexity.Foundations.Data.List.Fold
 import Complexity.Foundations.Data.List.OfFn
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.List
@@ -451,14 +452,6 @@ theorem jetL1Norm_weightedProdJet_le (J ℓ : ℕ) (w : ℤ) (groups : List JetR
 
 section SharedHelpers
 
-theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
-    (par : π) (xs : List ι) (init : α) :
-    xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
-      (par, xs.foldl (step par) init) := by
-  induction xs generalizing init with
-  | nil => rfl
-  | cons _ _ ih => exact ih _
-
 private def rangeAddJet (J ℓ j : ℕ) (f : ℕ → JetRows) : JetRows :=
   (List.range j).foldl (fun acc i => addJet J ℓ acc (f i)) (zeroJet J ℓ)
 private theorem isTableShape_rangeAddJet (J ℓ j : ℕ) (f : ℕ → JetRows) :
@@ -742,7 +735,7 @@ private theorem streamGroupJetSumRunPrefix_snd_snd_foldl (J ℓ d j : ℕ) (ctx
     (BooleanFold.runPrefix (groupSumBody evalGroupProd) d j (((J, ℓ), ctx), zeroJet J ℓ)).2.2 =
       (((J, ℓ), ctx), rangeAddJet J ℓ j fun i => evalGroupProd (ctx, (d, lowBits d i))) :=
   (BooleanFold.prefix_accumulator (groupSumBody evalGroupProd) d j _).trans
-    (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc i =>
+    (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc i =>
       addJet par.1.1 par.1.2 acc (evalGroupProd (par.2, (d, lowBits d i))))
       ((J, ℓ), ctx) (List.range j) (zeroJet J ℓ))
 theorem streamGroupJetSumPrefix_eq_foldl (J ℓ d j : ℕ) (ctx : α) :
@@ -757,7 +750,7 @@ theorem toJetTable_streamGroupJetSum_eq_sum (J ℓ d : ℕ) (ctx : α) :
       (enumList d).foldl (fun acc w => addJet J ℓ acc (evalGroupProd (ctx, (d, w))))
         (zeroJet J ℓ) :=
     congrArg Prod.snd ((BooleanFold.run_accumulator (groupSumBody evalGroupProd) d _).trans
-      (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc w =>
+      (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc w =>
         addJet par.1.1 par.1.2 acc (evalGroupProd (par.2, (d, w))))
         ((J, ℓ), ctx) (enumList d) (zeroJet J ℓ)))
   rw [hfold, toJetTable_foldl_addJet, toJetTable_zeroJet, zero_add, enumList, List.map_map,
@@ -976,7 +969,7 @@ private theorem streamOuterJetAccumRunPrefix_snd_foldl (J ℓ j : ℕ) (ctx : α
       (((J, ℓ), ctx), rangeAddJet J ℓ j fun idx =>
         weightedProdJet J ℓ (evalRound (ctx, idx)).1 (evalRound (ctx, idx)).2) :=
   (IndexFold.run_accumulator (outerAccumBody evalRound) j _).trans
-    (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc idx =>
+    (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc idx =>
       combineOuterRound par.1.1 par.1.2 acc (evalRound (par.2, idx)))
       ((J, ℓ), ctx) (List.range j) (zeroJet J ℓ))
 theorem streamOuterJetAccumPrefix_eq_foldl (J ℓ j : ℕ) (ctx : α) :

Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean

@@ -174,9 +174,7 @@ theorem polynomiallyBounded_widths :
       (fun c : Σ m, Circuit Boolean.signature m 1 => (c.1, c.2.code))
       (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
   have htotal : PolynomiallyBounded (fun n => secretWidth n + ciphertextWidth n) :=
-    (show PolyBounded (fun n : ℕ => n) (fun n => secretWidth n + ciphertextWidth n) by
-      simpa only [encUnary_apply, List.length_replicate, Function.comp_def] using
-        (hview.fst'.comp hD).polyBounded_length).polynomiallyBounded
+    (hview.fst'.comp hD).polynomiallyBounded
   exact ⟨htotal.mono_of_le (fun n => Nat.le_add_right (secretWidth n) (ciphertextWidth n)),
     htotal.mono_of_le (fun n => Nat.le_add_left (ciphertextWidth n) (secretWidth n))⟩
 
@@ -189,11 +187,7 @@ theorem polynomiallyBounded_decryptionSize :
       (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
   have hlen : ComputableInPolyTime (fun n => (D.circuit n).code.1.length) encUnary encUnary :=
     (ComputableInPolyTime.length_list Boolean.encGate).comp (hview.snd'.fst'.comp hD)
-  have hlength : PolynomiallyBounded (fun n => (D.circuit n).code.1.length) :=
-    (show PolyBounded (fun n : ℕ => n) (fun n => (D.circuit n).code.1.length) by
-      simpa only [encUnary_apply, List.length_replicate] using
-        hlen.polyBounded_length).polynomiallyBounded
-  exact hlength.mono_of_le (fun n => (Circuit.length_code_fst (D.circuit n)).ge)
+  exact hlen.polynomiallyBounded.mono_of_le (fun n => (Circuit.length_code_fst (D.circuit n)).ge)
 
 include hkeyGen hencrypt in
 /-- The constructed scheme's actual key generator is strict PPT. -/