refactor(Circuit,Promise): reuse computes_single_iff for single-output circuits (#884)

Complexity/Computability/Circuit/Boolean/Correction.lean

@@ -186,14 +186,12 @@ private theorem complexityOn_pi_le (s : Set (BitString n)) (f : Fin k → Boolea
   choose c hc hsize using fun i =>
     exists_computesOn_size_eq_complexityOn (I := interpretation) (S := s) (f := single (f i))
   have hcongr : Set.EqOn (fun x i => f i x) (fun x i => (c i).eval interpretation x 0) s :=
-    fun x hx => funext fun i => (congrFun (hc i hx) 0).symm
+    fun x hx => funext fun i => (Circuit.computesOn_single_iff.mp (hc i) x hx).symm
   rw [complexityOn_congr hcongr]
   refine complexityOn_le_complexity.trans ((complexity_pi_le _).trans
     (sum_le_sum fun i _ => ?_))
   rw [← hsize i]
-  refine complexity_le_of_computes (c i) fun x => funext fun j => ?_
-  rw [Fin.fin_one_eq_zero j]
-  rfl
+  refine complexity_le_of_computes (c i) (Circuit.computes_single_iff.mpr fun _ => rfl)
 
 /-- **Sparse correction with separate labels.** If `f` and `g` agree outside `s`, and agree on
 every output outside the range of `select`, then their complexities differ by at most the

Complexity/Computability/Circuit/Boolean/SparseSynthesis.lean

@@ -681,10 +681,8 @@ theorem shatters_circuitSets (ε : ℝ) (hε : 0 < ε) :
   obtain ⟨c, hc, hsize⟩ := exists_computesOn_size_eq_complexityOn (I := interpretation)
     (S := (D : Set (BitString (2 * p)))) (f := single fun x => decide (x ∈ t))
   let u : Finset (BitString (2 * p)) := {x | c.eval interpretation x 0 = true}
-  refine ⟨u, mem_circuitSets.2 ⟨c, fun x => ?_, Nat.le_floor (hsize ▸ hp₀ p hp D hD _)⟩, ?_⟩
-  · funext j
-    rw [Fin.fin_one_eq_zero j]
-    simp [u]
+  refine ⟨u, mem_circuitSets.2 ⟨c, Circuit.computes_single_iff.2 fun x => by simp [u],
+    Nat.le_floor (hsize ▸ hp₀ p hp D hD _)⟩, ?_⟩
   · ext x
     simp only [mem_inter, u, mem_filter, mem_univ, true_and]
     constructor

Complexity/Computability/Circuit/Frontier/Reduction.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Circuit.Frontier.Compiler
+import Complexity.Computability.Circuit.Complexity
 public import Mathlib.Analysis.SpecialFunctions.Log.Base
 
 /-!
@@ -80,7 +81,7 @@ Boolean function, with `Acc = {true}`, the set of inputs it maps to `true`. -/
 theorem Circuit.Computes.decides {c : Circuit σ n 1} {I : Interpretation σ U}
     {f : (Fin n → U) → U} (h : c.Computes I (single f)) (Acc : Set U) :
     c.Decides I Acc {x | f x ∈ Acc} := fun x => by
-  rw [Set.mem_ofPred_eq, congrFun (h x) 0, single_apply]
+  rw [Set.mem_ofPred_eq, ← Circuit.computes_single_iff.mp h]
 
 namespace Frontier
 

Complexity/Computability/Complexity/Classes/Promise/Circuit.lean

@@ -72,9 +72,8 @@ private def familyLanguage (C : ∀ n, Circuit signature n 1) : Language Bool :=
   Language.ofSlices fun n x => (C n).eval interpretation x 0
 
 private theorem computes_familyLanguage (n : ℕ) :
-    (C n).Computes interpretation (single ((familyLanguage C).slice n)) := fun x => by
-  funext i
-  rw [Subsingleton.elim i 0, familyLanguage, Language.slice_ofSlices, single_apply]
+    (C n).Computes interpretation (single ((familyLanguage C).slice n)) :=
+  Circuit.computes_single_iff.2 fun _ => by rw [familyLanguage, Language.slice_ofSlices]
 
 /-- A family of circuits that solves `Q` accepts a completion of `Q`. -/
 private theorem familyLanguage_separates