refactor(Complexity/Space): state PSPACE through ComputableInPolySpace, like P and L

CslibFrontier/Computability/Complexity/Classes/Counting/Space.lean

@@ -62,7 +62,7 @@ theorem PP_subset_PSPACE : PP enc ⊆ PSPACE enc := by
       ((ComputableInPolySpace.of_polyTime hpow).prod
         ((ComputableInPolySpace.of_polyTime hdouble).comp
           (SharpP.computableInPolySpace hf)))
-  exact mem_PSPACE_of_computableInPolySpace htest fun a => by simpa using hA a
+  exact ⟨_, htest, fun a => by simpa using hA a⟩
 
 /-- Testing whether a fixed modulus divides a #P count is in polynomial space. A quotient has
 at most one more bit than the verifier's certificate length, even for moduli zero and one. -/
@@ -87,9 +87,9 @@ theorem coModP_subset_PSPACE (k : ℕ) : coModP k enc ⊆ PSPACE enc := by
         (hle.comp ((ComputableInPolySpace.of_polyTime hright).prod hleft)))
   have hB : {x : α × List Bool | f x.1 = k * ofBits x.2} ∈
       PSPACE (encPair enc encBits) :=
-    mem_PSPACE_of_computableInPolySpace htest fun x => by
+    ⟨_, htest, fun x => by
       simp only [Set.mem_ofPred_eq, Bool.and_eq_true, decide_eq_true_eq]
-      exact le_antisymm_iff
+      exact le_antisymm_iff⟩
   have hbound : ComputableInPolyTime (fun a => p.eval (enc a).length + 1)
       enc encUnary := by fun_prop
   have h := setOf_exists_mem_PSPACE hB hbound

CslibFrontier/Computability/Complexity/Classes/IP/PSPACE.lean

@@ -620,7 +620,7 @@ theorem IP_subset_PSPACE (enc : α ↪ List Bool) : IP enc ⊆ PSPACE enc := by
     exact (ComputableInPolySpace.of_polyTime hpost).comp
       ((ComputableInPolySpace.of_polyTime hcap).prod
         (computableInPolySpace_evaluate M hfuel))
-  refine mem_PSPACE_of_computableInPolySpace hdec fun a => ?_
+  refine ⟨_, hdec, fun a => ?_⟩
   rw [mem_iff_two_pow_lt_value (fun a S oracle s => hreal a S oracle s) hA a, evaluate_eq,
     decide_eq_true_iff]
 

CslibFrontier/Computability/Complexity/Classes/LogSpace.lean

@@ -164,9 +164,8 @@ theorem L_subset_P : L enc ⊆ P enc := by
   exact ⟨f, hf.computableInPolyTime, hA⟩
 
 /-- **Deterministic logarithmic space is within polynomial space.** -/
-theorem L_subset_PSPACE : L enc ⊆ PSPACE enc := by
-  rintro A ⟨f, ⟨t, c, hf⟩, hA⟩
-  exact ⟨f, ⟨t, _, polyBounded_log (fun a => (enc a).length) c, hf⟩, hA⟩
+theorem L_subset_PSPACE : L enc ⊆ PSPACE enc :=
+  L_subset_P.trans P_subset_PSPACE
 
 /-- **Nondeterministic logarithmic space is within nondeterministic polynomial space.** -/
 theorem NL_subset_NPSPACE : NL enc ⊆ NPSPACE enc := by

CslibFrontier/Computability/Complexity/Classes/Space.lean

@@ -11,18 +11,23 @@ public import CslibFrontier.Computability.Complexity.Classes.P
 public import CslibFrontier.Computability.Complexity.Classes.Space.Basic
 public import CslibFrontier.Computability.Complexity.Reduction
 public import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.Nondeterministic
+public import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain
 import CslibFrontier.Foundations.Data.Nat.PolynomialBound.Exponential
 
 /-!
 # Polynomial space
 
-`Cslib.Complexity.PSPACE enc` consists of the problems decided by one deterministic machine with a
-binary alphabet and finitely many states that halts on every encoded instance `enc a` with output
-`[true]` or `[false]`, visiting at most `s a` work-tape cells for an `s` polynomially bounded in
-the length of `enc a` (upstream `Turing.MultiTapeTM.ComputableInTimeAndSpace`, with no tidiness
+`Cslib.Complexity.PSPACE enc` consists of the problems decided by a Boolean function computable
+within polynomial space (`Turing.MultiTapeTM.ComputableInPolySpace`), as `Cslib.Complexity.P` and
+`Cslib.Complexity.L` use polynomial time and logarithmic space: one deterministic machine with a
+binary alphabet and finitely many states halts on every encoded instance `enc a` with output
+`[true]` or `[false]`, visiting at most `s (enc a).length` work-tape cells for a polynomially
+bounded `s` (upstream `Turing.MultiTapeTM.ComputableInTimeAndSpace`, with no tidiness
 requirement). No bound on the time is imposed beyond halting. Equivalently
-(`Cslib.Complexity.mem_PSPACE_iff`), the problem is decidable within some time bound and such a
-space bound in the sense of upstream `Turing.MultiTapeTM.DecidableInTimeAndSpace`. The proposed
+(`Cslib.Complexity.mem_PSPACE_iff`), the problem is decidable within some time bound and a space
+bound polynomially bounded in the length of `enc a`, in the sense of upstream
+`Turing.MultiTapeTM.DecidableInTimeAndSpace`. The proposed
 upstream complexity classes (cslib pull request #767, open) build `DSPACE` on the same notion of
 decidability and define `PSPACE` as the union of the classes of space `O(n ^ k)`; their bounds
 are functions of the input length. For the local encoded-instance classes,
@@ -61,6 +66,9 @@ tape write-only [Sipser, Section 8.4 and Definition 8.21][Sipser2013].
 
 ## Main results
 
+* `Cslib.Complexity.mem_PSPACE`: a Boolean decider computable within polynomial space.
+* `Cslib.Complexity.mem_PSPACE_of_computableInTimeAndSpace`: a decider within a polynomially
+  bounded space bound.
 * `Cslib.Complexity.mem_PSPACE_iff`: `PSPACE` in terms of upstream `DecidableInTimeAndSpace`.
 * `Cslib.Complexity.mem_PSPACE_iff_exists_mem_DSPACE`: the union of `DSPACE (n ^ k)`.
 * `Cslib.Complexity.DSPACE_subset_PSPACE`: polynomially bounded space is within `PSPACE`.
@@ -84,19 +92,30 @@ open Turing Turing.MultiTapeTM
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
 /-- The problems decided by one deterministic machine within polynomial space, with respect to
-the encoding `enc`: a Boolean function deciding membership is computable (upstream
-`Turing.MultiTapeTM.ComputableInTimeAndSpace`) within some time and within space polynomially
-bounded in the length of the encoded instance [Sipser, Section 8.2][Sipser2013]. -/
+the encoding `enc`: a Boolean function deciding membership is computable within some time and
+within space polynomial in the length of the encoded instance
+(`Turing.MultiTapeTM.ComputableInPolySpace`) [Sipser, Section 8.2][Sipser2013]. -/
 def PSPACE (enc : α ↪ List Bool) : Set (Set α) :=
-  {A | ∃ f : α → Bool, (∃ t s, PolyBounded (fun a => (enc a).length) s ∧
-    ComputableInTimeAndSpace f enc encBool t s) ∧ ∀ a, a ∈ A ↔ f a = true}
+  {A | ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}
+
+theorem mem_PSPACE : A ∈ PSPACE enc ↔
+    ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true :=
+  Iff.rfl
+
+/-- A Boolean decider computable within some time and within a space bound polynomially bounded
+in the length of the encoded instance decides a problem in `PSPACE`. -/
+theorem mem_PSPACE_of_computableInTimeAndSpace {f : α → Bool} {t s : α → ℕ}
+    (hs : PolyBounded (fun a => (enc a).length) s)
+    (hf : ComputableInTimeAndSpace f enc encBool t s) (hA : ∀ a, a ∈ A ↔ f a = true) :
+    A ∈ PSPACE enc :=
+  ⟨f, .of_inSpace hs ⟨t, 1, hf.mono (fun _ => le_rfl) fun _ => by omega, fun _ => by simp⟩, hA⟩
 
 /-- Membership in `PSPACE` is upstream decidability within some time and polynomial space. -/
 theorem mem_PSPACE_iff : A ∈ PSPACE enc ↔
     ∃ t s, PolyBounded (fun a => (enc a).length) s ∧ DecidableInTimeAndSpace A enc t s := by
   simp only [decidableInTimeAndSpace_iff]
-  exact ⟨fun ⟨f, ⟨t, s, hs, hf⟩, hA⟩ => ⟨t, s, hs, f, hf, hA⟩,
-    fun ⟨t, s, hs, f, hf, hA⟩ => ⟨f, ⟨t, s, hs, hf⟩, hA⟩⟩
+  exact ⟨fun ⟨f, ⟨t, _, hs, hf, _⟩, hA⟩ => ⟨t, _, .of_polynomiallyBounded _ hs, f, hf, hA⟩,
+    fun ⟨_, _, hs, _, hf, hA⟩ => mem_PSPACE_of_computableInTimeAndSpace hs hf hA⟩
 
 /-- A space class of a polynomially bounded bound is within `PSPACE`. -/
 theorem DSPACE_subset_PSPACE {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ}
@@ -125,17 +144,15 @@ def NPSPACE (enc : α ↪ List Bool) : Set (Set α) :=
     (s : α → ℕ), PolyBounded (fun a => (enc a).length) s ∧ ntm.DecidesInSpace enc A s}
 
 /-- **Polynomial time is within polynomial space.** -/
-theorem P_subset_PSPACE : P enc ⊆ PSPACE enc := fun A hA => by
-  obtain ⟨f, hf, hA⟩ := mem_P.mp hA
-  obtain ⟨t, s, -, hs, hf⟩ := hf
-  exact ⟨f, ⟨_, _, .of_polynomiallyBounded _ hs, hf⟩, hA⟩
+theorem P_subset_PSPACE : P enc ⊆ PSPACE enc := fun _ ⟨f, hf, hA⟩ =>
+  ⟨f, .of_polyTime hf, hA⟩
 
 /-- **A deterministic polynomial-space machine is a nondeterministic one**, with one computation
 path (`Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace`). -/
 theorem PSPACE_subset_NPSPACE : PSPACE enc ⊆ NPSPACE enc := by
-  rintro A ⟨f, ⟨t, s, hs, hf⟩, hA⟩
+  rintro A ⟨f, ⟨t, s, hs, hf, -⟩, hA⟩
   obtain ⟨k, State, hfinite, ntm, h⟩ := hf.exists_decidesInSpace hA
-  exact ⟨k, State, hfinite, ntm, s, hs, h⟩
+  exact ⟨k, State, hfinite, ntm, _, .of_polynomiallyBounded _ hs, h⟩
 
 /-! ### Hardness and completeness -/
 

CslibFrontier/Computability/Complexity/Classes/Space/Closure.lean

@@ -24,9 +24,9 @@ import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpac
 # Characterizations and closure properties of `PSPACE`
 
 A problem is in `PSPACE` exactly when a Boolean function deciding it is computable within
-some time and space polynomial in the length of the encoded instance
-(`Cslib.Complexity.mem_PSPACE_iff_computableInO`,
-`Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`). `PSPACE` is closed under
+some time and space polynomial in the length of the encoded instance, in the quantitative calculus
+of `Turing.MultiTapeTM.ComputableInO` (`Cslib.Complexity.mem_PSPACE_iff_computableInO`). `PSPACE`
+is closed under
 complement, under polynomial-time reductions, and under polynomially bounded existential
 quantification [Arora and Barak, Chapter 4][AroraBarak09]. The existential quantifier over words
 `w` of length `ℓ` streams one candidate at a time and
@@ -35,8 +35,6 @@ reuses the space of the decider for each (`Turing.MultiTapeTM.ComputableInO.exis
 ## Main results
 
 * `Cslib.Complexity.mem_PSPACE_iff_computableInO`: `PSPACE` in the quantitative calculus.
-* `Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`,
-  `Cslib.Complexity.mem_PSPACE_of_computableInPolySpace`: `PSPACE` within polynomial space.
 * `Cslib.Complexity.compl_mem_PSPACE`, `Cslib.Complexity.PSPACE_eq_preimage_compl_PSPACE`,
   `Cslib.Complexity.inter_mem_PSPACE`,
   `Cslib.Complexity.union_mem_PSPACE`, `Cslib.Complexity.diff_mem_PSPACE`,
@@ -66,37 +64,17 @@ theorem mem_PSPACE_iff_computableInO : A ∈ PSPACE enc ↔ ∃ (f : α → Bool
     ComputableInO f enc encBool T S ∧ PolyBounded (fun a => (enc a).length) S ∧
       ∀ a, a ∈ A ↔ f a = true := by
   constructor
-  · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩
-    exact ⟨f, t, s, ⟨1, hf.mono (fun _ => by omega) fun _ => by omega, fun _ => by simp⟩, hs, hA⟩
-  · rintro ⟨f, T, S, ⟨c, hc, -⟩, hS, hA⟩
-    exact ⟨f, ⟨_, _, (PolyBounded.const c).mul (hS.add (.const 1)), hc⟩, hA⟩
-
-/-- **`PSPACE` within polynomial space**: a problem is in `PSPACE` exactly when a Boolean function
-deciding it is computable within space polynomial in the length of the encoded instance
-(`Turing.MultiTapeTM.ComputableInPolySpace`). -/
-theorem mem_PSPACE_iff_computableInPolySpace : A ∈ PSPACE enc ↔
-    ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true := by
-  constructor
-  · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩
-    obtain ⟨c, d, hcd⟩ := hs.exists_le
-    refine ⟨f, ⟨t, fun n => c * (n + 1) ^ d + 1, by fun_prop,
-      hf.mono (fun _ => le_rfl) fun a => (hcd a).trans (Nat.le_succ _),
-      fun _ => by simp⟩, hA⟩
   · rintro ⟨f, ⟨t, s, hs, hf, -⟩, hA⟩
-    exact ⟨f, ⟨t, _, .of_polynomiallyBounded _ hs, hf⟩, hA⟩
-
-/-- A Boolean function computable within polynomial space decides a problem in `PSPACE`. -/
-theorem mem_PSPACE_of_computableInPolySpace {f : α → Bool}
-    (hf : ComputableInPolySpace f enc encBool) (hA : ∀ a, a ∈ A ↔ f a = true) :
-    A ∈ PSPACE enc :=
-  mem_PSPACE_iff_computableInPolySpace.mpr ⟨f, hf, hA⟩
+    exact ⟨f, t, _, ⟨1, hf.mono (fun _ => by omega) fun _ => by omega, fun _ => by simp⟩,
+      .of_polynomiallyBounded _ hs, hA⟩
+  · rintro ⟨f, T, S, ⟨c, hc, hl⟩, hS, hA⟩
+    exact ⟨f, .of_inSpace hS ⟨_, c, hc, hl⟩, hA⟩
 
 /-- **`PSPACE` is closed under complement**: negate the answer. -/
 theorem compl_mem_PSPACE (hA : A ∈ PSPACE enc) : Aᶜ ∈ PSPACE enc := by
-  obtain ⟨f, hf, hA⟩ := mem_PSPACE_iff_computableInPolySpace.mp hA
-  exact mem_PSPACE_of_computableInPolySpace
-    ((ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_not).comp hf)
-    fun a => by simp [hA a]
+  obtain ⟨f, hf, hA⟩ := hA
+  exact ⟨_, (ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_not).comp hf,
+    fun a => by simp [hA a]⟩
 
 /-- `PSPACE` equals its preimage under complement. -/
 theorem PSPACE_eq_preimage_compl_PSPACE (enc : α ↪ List Bool) :
@@ -108,11 +86,10 @@ open scoped symmDiff
 /-- **`PSPACE` is closed under intersection.** -/
 theorem inter_mem_PSPACE {B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) :
     A ∩ B ∈ PSPACE enc := by
-  obtain ⟨f, hf, hA⟩ := mem_PSPACE_iff_computableInPolySpace.mp hA
-  obtain ⟨g, hg, hB⟩ := mem_PSPACE_iff_computableInPolySpace.mp hB
-  exact mem_PSPACE_of_computableInPolySpace
-    ((ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_and).comp (hf.prod hg))
-    fun a => by simp [hA a, hB a]
+  obtain ⟨f, hf, hA⟩ := hA
+  obtain ⟨g, hg, hB⟩ := hB
+  exact ⟨_, (ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_and).comp (hf.prod hg),
+    fun a => by simp [hA a, hB a]⟩
 
 /-- `PSPACE` as a Boolean subalgebra of `Set α`. -/
 def PSPACE.booleanSubalgebra (enc : α ↪ List Bool) : BooleanSubalgebra (Set α) :=
@@ -146,9 +123,8 @@ theorem symmDiff_mem_PSPACE {B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSP
 theorem PolyTimeReducible.mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set β}
     (h : PolyTimeReducible enc encB A B) (hB : B ∈ PSPACE encB) : A ∈ PSPACE enc := by
   obtain ⟨g, hg, hAB⟩ := h
-  obtain ⟨f, hf, hB⟩ := mem_PSPACE_iff_computableInPolySpace.mp hB
-  exact mem_PSPACE_of_computableInPolySpace (hf.comp (.of_polyTime hg))
-    fun a => (hAB a).trans (hB (g a))
+  obtain ⟨f, hf, hB⟩ := hB
+  exact ⟨_, hf.comp (.of_polyTime hg), fun a => (hAB a).trans (hB (g a))⟩
 
 /-- **`PSPACE` is closed under polynomially bounded existential quantification.** The candidates
 are streamed in place by `ComputableInO.exists_bits`, reusing the decider's workspace without a

CslibFrontier/Computability/Complexity/Classes/Space/Savitch.lean

@@ -54,8 +54,8 @@ theorem mem_PSPACE_of_recognizesInSpace {k : ℕ} {State : Type} [Finite State]
     A ∈ PSPACE enc := by
   obtain ⟨c, d, hcd⟩ := hs.exists_le
   obtain ⟨t, s', hs', hdecide⟩ := ntm.exists_polyBounded_space_savitchDecide enc c d
-  exact ⟨fun a => ntm.savitchDecide c d (enc a), ⟨t, s', hs', hdecide⟩,
-    fun a => (hA a).2.trans (MultiTapeNTM.savitchDecide_eq_true_iff (hA a).1 (hcd a)).symm⟩
+  exact mem_PSPACE_of_computableInTimeAndSpace hs' hdecide
+    fun a => (hA a).2.trans (MultiTapeNTM.savitchDecide_eq_true_iff (hA a).1 (hcd a)).symm
 
 /-- **Savitch's theorem for polynomial space**: every problem decided by a nondeterministic
 machine within polynomial space is decided by a deterministic machine within polynomial space,

CslibFrontier/Computability/Complexity/Classes/Space/TM2.lean

@@ -55,7 +55,6 @@ theorem mem_PSPACE_of_tm2 {α αΓ βΓ : Type} [Finite αΓ] [Finite βΓ]
     ha hb hspace hstacks
   have hbool := ComputableInPolyTime.of_finite (id : Bool → Bool)
     (encIn := (⟨eb, hb⟩ : Bool ↪ List βΓ).trans (encList (encFinite βΓ))) (encOut := encBool)
-  exact mem_PSPACE_of_computableInPolySpace ((ComputableInPolySpace.of_polyTime hbool).comp hf)
-    hA
+  exact ⟨_, (ComputableInPolySpace.of_polyTime hbool).comp hf, hA⟩
 
 end Cslib.Complexity

CslibFrontier/Computability/Complexity/Classes/Space/TQBF/Membership.lean

@@ -412,8 +412,7 @@ open Turing.MultiTapeTM
 space polynomial in the length of the encoded formula. -/
 theorem TQBF_mem_PSPACE : TQBF ∈ PSPACE encQBF := by
   obtain ⟨e, c, h, -⟩ := TQBF.exists_computableInO_evaluate
-  refine ⟨TQBF.evaluate, ⟨_, _, ?_, h⟩,
-    fun φ => TQBF.evaluate_eq_true_iff.symm⟩
+  refine mem_PSPACE_of_computableInTimeAndSpace ?_ h fun φ => TQBF.evaluate_eq_true_iff.symm
   refine PolyBounded.of_forall_le (2 * c) e fun φ => ?_
   have := Nat.one_le_pow e ((encQBF φ).length + 1) (by omega)
   nlinarith

CslibFrontier/Computability/Complexity/Problems/SAT/Space.lean

@@ -142,8 +142,8 @@ end SharpSAT
 /-- `SAT` lies in `PSPACE encCNF` by deterministic polynomial-space enumeration of all
 `2 ^ φ.numVars` assignments. -/
 theorem SAT.mem_PSPACE_of_enumeration : SAT ∈ PSPACE encCNF := by
-  refine mem_PSPACE_of_computableInPolySpace (f := fun φ : CNF ℕ => decide (0 < SharpSAT φ))
-    ?_ fun φ => by rw [SharpSAT.mem_SAT_iff, decide_eq_true_eq]
+  refine ⟨fun φ => decide (0 < SharpSAT φ), ?_, fun φ => by
+    rw [SharpSAT.mem_SAT_iff, decide_eq_true_eq]⟩
   have hpos : ComputableInPolyTime (fun n : ℕ => decide (0 < n)) encNat encBool := by fun_prop
   exact (ComputableInPolySpace.of_polyTime hpos).comp SharpSAT.computableInPolySpace_numVars
 
@@ -154,10 +154,9 @@ theorem UNSAT.mem_PSPACE_of_enumeration : UNSAT ∈ PSPACE encCNF :=
 /-- `USAT` lies in `PSPACE encCNF` by deterministic polynomial-space enumeration and checking
 `#SAT = 1`. -/
 theorem USAT.mem_PSPACE_of_enumeration : USAT ∈ PSPACE encCNF := by
-  refine mem_PSPACE_of_computableInPolySpace
-    (f := fun φ : CNF ℕ => decide (0 < SharpSAT φ) && decide (SharpSAT φ < 2)) ?_ fun φ => by
+  refine ⟨fun φ => decide (0 < SharpSAT φ) && decide (SharpSAT φ < 2), ?_, fun φ => by
     rw [SharpSAT.mem_USAT_iff, Bool.and_eq_true, decide_eq_true_eq, decide_eq_true_eq]
-    omega
+    omega⟩
   have heq1 : ComputableInPolyTime (fun n : ℕ => decide (0 < n) && decide (n < 2))
       encNat encBool := by fun_prop
   exact (ComputableInPolySpace.of_polyTime heq1).comp SharpSAT.computableInPolySpace_numVars

CslibFrontier/Computability/Machines/Turing/TM2/Reverse/Transfer.lean

@@ -172,7 +172,6 @@ theorem mem_PSPACE_iff_tm2 {α : Type} {encIn : α ↪ List Bool} {A : Set α} :
       (∀ stack, Finite (h.tm.Γ stack)) ∧
         (∃ space : α → ℕ, PolyBounded (fun a => (encIn a).length) space ∧
           h.StacksBounded space) ∧ (∀ a, a ∈ A ↔ f a = true) := by
-  rw [mem_PSPACE_iff_computableInPolySpace]
   constructor
   · rintro ⟨f, hf, hA⟩
     obtain ⟨h, hfinite, hspace⟩ := hf.exists_tm2Computable

CslibFrontierTests/InteractiveProofs.lean

@@ -192,8 +192,7 @@ example : ComputableInPolySpace (fun w => BitString.increment (BitString.increme
 
 -- A Boolean function computable within polynomial space decides a problem in `PSPACE`.
 example : {w : List Bool | w.headD false = true} ∈ PSPACE encBits :=
-  mem_PSPACE_of_computableInPolySpace (f := fun w => w.headD false)
-    (.of_polyTime (ComputableInPolyTime.headD false)) fun _ => Iff.rfl
+  ⟨fun w => w.headD false, .of_polyTime (ComputableInPolyTime.headD false), fun _ => Iff.rfl⟩
 
 -- The seven codes of length `3` decode to the seven words of length at most `2`, each once.
 example : (List.range (Interaction.codeCount 2)).map (fun i =>

CslibFrontierTests/MathlibTM2Reverse.lean

@@ -130,7 +130,6 @@ example : ∃ (f : List Bool → Bool) (h : TM2Computable (encList (encFinEnum B
           h.StacksBounded space) ∧
       (∀ xs, xs ∈ {xs : List Bool | xs.isEmpty = true} ↔ f xs = true) :=
   Cslib.Complexity.mem_PSPACE_iff_tm2.mp
-    (Cslib.Complexity.mem_PSPACE_of_computableInPolySpace
-      (.of_polyTime (.of_tidy (.listIsEmpty' (encFinEnum Bool)))) (fun _ => Iff.rfl))
+    ⟨_, .of_polyTime (.of_tidy (.listIsEmpty' (encFinEnum Bool))), fun _ => Iff.rfl⟩
 
 end CslibFrontierTests.MathlibTM2Reverse