refactor(Classes,PCP,TreeEval,Kolmogorov): make 57 API and general declarations public again (#926)

Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean

@@ -321,7 +321,7 @@ theorem modBits_all_false_iff (l f : List Bool) :
   exact degree_polyOfBits_lt _
 
 /-- Every nonzero binary polynomial is monic. -/
-private theorem monic_of_ne_zero {q : (ZMod 2)[X]} (hq : q ≠ 0) : q.Monic :=
+theorem monic_of_ne_zero {q : (ZMod 2)[X]} (hq : q ≠ 0) : q.Monic :=
   (by decide : ∀ c : ZMod 2, c ≠ 0 → c = 1) _ (leadingCoeff_ne_zero.2 hq)
 
 private theorem natDegree_polyOfCode_eq_log (m : ℕ) : (polyOfCode m).natDegree = Nat.log 2 m := by

Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean

@@ -76,7 +76,7 @@ theorem repr_fieldOfBits (B : Basis (Fin n) (ZMod 2) F) (a : List Bool) (u : Fin
 theorem fieldOfBits_nil (B : Basis (Fin n) (ZMod 2) F) : fieldOfBits B [] = 0 := by
   simp [fieldOfBits]
 
-private theorem bitEquiv_symm_foldl_xor (l : List Bool) :
+theorem bitEquiv_symm_foldl_xor (l : List Bool) :
     bitEquiv.symm (l.foldl xor false) = (l.map bitEquiv.symm).sum := by
   rw [← map_list_sum]
   congr 1
@@ -245,7 +245,7 @@ theorem fieldOfBits_esymmCoords {B : Basis (Fin n) (ZMod 2) F} {tab : List (List
 
 /-- The trace is the trace of the multiplication matrix: the sum of the diagonal coordinates
 `[x * b i]_i`. -/
-private theorem trace_eq_sum_repr_mul {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+theorem trace_eq_sum_repr_mul {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
     {ι : Type*} [Fintype ι] (b : Basis ι R S) (x : S) :
     Algebra.trace R S x = ∑ i, b.repr (x * b i) i := by
   classical
@@ -289,7 +289,7 @@ input bits. -/
 def blockPos {r n N : ℕ} (h : r * n ≤ N) (q : Fin r × Fin n) : Fin N :=
   Fin.castLE h (finProdFinEquiv q)
 
-private theorem getD_take_drop (x : List Bool) {n u : ℕ} (hu : u < n) (i : ℕ) :
+theorem getD_take_drop (x : List Bool) {n u : ℕ} (hu : u < n) (i : ℕ) :
     ((x.drop (n * i)).take n).getD u false = x.getD (n * i + u) false := by
   rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_take_of_lt hu,
     List.getElem?_drop]

Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean

@@ -132,7 +132,7 @@ theorem updates_of_notMem {σ : V → Bool} {vs : List V} {x : V} (hx : x ∉ vs
       rw [updates, ih hx.2, Function.update_of_ne hx.1]
 
 /-- Updating distinct variables by as many values sets them to these values. -/
-private theorem map_updates {σ : V → Bool} {vs : List V} (hvs : vs.Nodup) {bs : List Bool}
+theorem map_updates {σ : V → Bool} {vs : List V} (hvs : vs.Nodup) {bs : List Bool}
     (hlen : bs.length = vs.length) : vs.map (updates σ vs bs) = bs := by
   induction vs generalizing σ bs with
   | nil => exact (List.length_eq_zero_iff.mp hlen).symm

Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean

@@ -85,12 +85,12 @@ namespace PublicCoin
 variable {n : ℕ}
 
 /-- Relabelling by a product of permutations is relabelling twice. -/
-private theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) :
+theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) :
     Matrix.reindex (σ * τ) (σ * τ) M = Matrix.reindex σ σ (Matrix.reindex τ τ M) :=
   (DFunLike.congr_fun (Matrix.reindex_trans τ τ σ σ) M).symm
 
 /-- Relabelling by the identity permutation does nothing. -/
-private theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M :=
+theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M :=
   Matrix.reindex_refl_refl M
 
 /-- `Matrix.reindex τ τ A = M` says that `τ` carries `A` to `M`. -/

Complexity/Computability/Complexity/Classes/IP.lean

@@ -161,7 +161,7 @@ theorem acceptProb_sample_bind {β : Type} (program : ProbComp β)
   rfl
 
 /-- A verifier none of whose possible results accepts has acceptance probability zero. -/
-private theorem acceptProb_eq_zero {verifier : WordOracleComp Operation Bool} (P : Prover Operation)
+theorem acceptProb_eq_zero {verifier : WordOracleComp Operation Bool} (P : Prover Operation)
     (h : ∀ x ∈ (P.run verifier P.init).support, x.1 = false) : acceptProb verifier P = 0 := by
   rw [acceptProb, PMF.apply_eq_zero_iff, PMF.support_map]
   rintro ⟨x, hx, hx'⟩

Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean

@@ -271,7 +271,7 @@ private theorem replay_coinStep (t : ℕ) (cfg : FiniteConfig k Bool Control Uni
         split_ifs with hm <;> simp [hm]
 
 /-- A fold in the state and exception monad is a fold of results. -/
-private theorem foldlM_run {σ ε β γ : Type} (g : β → γ → StateT σ (Except ε) β) (l : List γ)
+theorem foldlM_run {σ ε β γ : Type} (g : β → γ → StateT σ (Except ε) β) (l : List γ)
     (b : β) (s : σ) :
     (l.foldlM g b).run s =
       l.foldl (fun acc c => acc.bind fun p => (g p.1 c).run p.2) (.ok (b, s)) := by

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

@@ -98,7 +98,7 @@ zeros, a one, then `w`. -/
 def encodeWord (L : ℕ) (w : List Bool) : List Bool :=
   List.replicate (L - w.length) false ++ true :: w
 
-private theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) :
+theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) :
     (List.replicate n false ++ true :: w).idxOf true = n := by
   induction n with
   | zero => simp

Complexity/Computability/Complexity/Classes/IP/TQBF/Tokens.lean

@@ -138,7 +138,7 @@ theorem tokens_append_inj {e e' : ArithQBF ℕ} {r r' : List (Kind × ℕ)}
       exact ⟨rfl, rfl⟩
 
 /-- Linearizations come first in prefix order. -/
-private theorem tokens_lins (xs : List ℕ) (e : ArithQBF ℕ) :
+theorem tokens_lins (xs : List ℕ) (e : ArithQBF ℕ) :
     (lins xs e).tokens = xs.map (fun x => (Kind.lin, x)) ++ e.tokens := by
   induction xs with
   | nil => rfl

Complexity/Computability/Complexity/Classes/Ladner/Basic.lean

@@ -83,19 +83,19 @@ def word (j : ℕ) : List Bool := (j + 1).bits.dropLast
 `true`. -/
 def index (w : List Bool) : ℕ := w.foldr Nat.bit 1 - 1
 
-private theorem foldr_bit_one_ne_zero (w : List Bool) : w.foldr Nat.bit 1 ≠ 0 := by
+theorem foldr_bit_one_ne_zero (w : List Bool) : w.foldr Nat.bit 1 ≠ 0 := by
   induction w with
   | nil => simp
   | cons b w ih => exact Nat.bit_ne_zero b ih
 
-private theorem bits_foldr_bit_one (w : List Bool) : (w.foldr Nat.bit 1).bits = w ++ [true] := by
+theorem bits_foldr_bit_one (w : List Bool) : (w.foldr Nat.bit 1).bits = w ++ [true] := by
   induction w with
   | nil => simp
   | cons b w ih =>
     rw [List.foldr_cons, Nat.bits_append_bit _ _ fun h => absurd h (foldr_bit_one_ne_zero w), ih,
       List.cons_append]
 
-private theorem foldr_bit_one_lt (w : List Bool) : w.foldr Nat.bit 1 < 2 ^ (w.length + 1) := by
+theorem foldr_bit_one_lt (w : List Bool) : w.foldr Nat.bit 1 < 2 ^ (w.length + 1) := by
   induction w with
   | nil => simp
   | cons b w ih =>
@@ -138,7 +138,7 @@ theorem length_pad (u : List Bool) (k : ℕ) : (pad u k).length = u.length + 1 +
   simp only [pad, List.length_append, List.length_cons, List.length_replicate]
   omega
 
-private theorem idxOf_false_replicate_append (k : ℕ) (l : List Bool) :
+theorem idxOf_false_replicate_append (k : ℕ) (l : List Bool) :
     (List.replicate k true ++ false :: l).idxOf false = k := by
   induction k with
   | zero => simp
@@ -157,7 +157,7 @@ theorem pad_inj {u u' : List Bool} {k k' : ℕ} : pad u k = pad u' k' ↔ u = u'
   ⟨fun h => by simpa using congrArg unpad h, fun ⟨hu, hk⟩ => hu ▸ hk ▸ rfl⟩
 
 /-- A word with a `false` is a run of `true`s up to its first `false`, and what follows. -/
-private theorem eq_replicate_idxOf_false {l : List Bool} (hl : false ∈ l) :
+theorem eq_replicate_idxOf_false {l : List Bool} (hl : false ∈ l) :
     l = List.replicate (l.idxOf false) true ++ false :: l.drop (l.idxOf false + 1) := by
   induction l with
   | nil => simp at hl

Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean

@@ -346,7 +346,7 @@ def hstepB (T : List ℕ) : ℕ :=
     (List.range T.length).all fun j => agreesB T i j).getD (Nat.log 2 (Nat.log 2 T.length))
 
 /-- The least index below `m` passing a test, or `m`, as a search over `List.range m`. -/
-private theorem find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) :
+theorem find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) :
     ((List.range m).find? p).getD m = sInf {i | i = m ∨ p i = true} := by
   set v := ((List.range m).find? p).getD m with hv
   have hmem : v ∈ {i | i = m ∨ p i = true} ∧ ∀ i < v, i ∉ {i | i = m ∨ p i = true} := by
@@ -484,7 +484,7 @@ private theorem computableTidilyInPolyTime_verifier :
   fun_prop
 
 /-- Padding a certificate with `false` does not change the assignment it describes. -/
-private theorem assignment_append_replicate (φ : CNF ℕ) (w : List Bool) (k : ℕ) :
+theorem assignment_append_replicate (φ : CNF ℕ) (w : List Bool) (k : ℕ) :
     SAT.assignment φ (w ++ List.replicate k false) = SAT.assignment φ w := by
   funext v
   simp only [SAT.assignment, List.getD_eq_getElem?_getD, List.getElem?_append]

Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean

@@ -59,7 +59,7 @@ def boundDepth {α : Type*} : ∀ {k : ℕ}, L.BoundedFormula α k → ℕ
   | _, .imp φ ψ => max (boundDepth φ) (boundDepth ψ)
   | _, .all φ => boundDepth φ
 
-private theorem le_boundDepth {α : Type*} : ∀ {k : ℕ} (φ : L.BoundedFormula α k), k ≤ boundDepth φ
+theorem le_boundDepth {α : Type*} : ∀ {k : ℕ} (φ : L.BoundedFormula α k), k ≤ boundDepth φ
   | _, .falsum => le_rfl
   | _, .equal _ _ => le_rfl
   | _, .rel _ _ => le_rfl

Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean

@@ -110,12 +110,12 @@ private theorem eval_append_units (σ : ℕ → Bool) (φ : CNF ℕ) (answers :
     (φ ++ units answers).eval σ = true ↔ φ.eval σ = true ∧ ∀ l ∈ answers, σ l.1 = l.2 := by
   simp [units, CNF.eval_eq_true_iff, Clause.eval_eq_true_iff, or_imp, forall_and]
 
-private theorem length_encCNF_append (φ ψ : CNF ℕ) :
+theorem length_encCNF_append (φ ψ : CNF ℕ) :
     (encCNF (φ ++ ψ)).length = (encCNF φ).length + (encCNF ψ).length := by
   simp [encCNF]
 
 /-- A variable of a formula takes fewer bits than the formula. -/
-private theorem length_encNat_le_of_mem_vars {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :
+theorem length_encNat_le_of_mem_vars {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :
     (encNat v).length ≤ (encCNF φ).length := by
   obtain ⟨l, hl, rfl⟩ := List.mem_map.1 hv
   obtain ⟨c, hc, hl⟩ := List.mem_flatten.1 hl

Complexity/Computability/Complexity/Classes/Oracle.lean

@@ -105,7 +105,7 @@ def queriesWith (answer : (q : ι) → spec q) : OracleComp spec α → List ι
 
 /-- A sequence makes the requests of its first part, then those of the continuation selected by
 the first result. -/
-private theorem queriesWith_bind (answer : (q : ι) → spec q) (program : OracleComp spec α)
+theorem queriesWith_bind (answer : (q : ι) → spec q) (program : OracleComp spec α)
     (next : α → OracleComp spec β) :
     queriesWith answer (program >>= next) = queriesWith answer program ++
       queriesWith answer (next (interpret (m := Id) answer program)) := by

Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean

@@ -305,7 +305,7 @@ theorem decodeQBF_pt : Turing.MultiTapeTM.ComputableInPolyTime decodeQBF encBits
   .of_tidy ((ComputableTidilyInPolyTime.ite' isCode_pt.tidy ComputableTidilyInPolyTime.id'
     (ComputableTidilyInPolyTime.const (encQBF .bot))).of_enc_eq fun w => encQBF_decodeQBF w)
 
-private theorem decodeQBF_encQBF (φ : QBF ℕ) : decodeQBF (encQBF φ) = φ :=
+theorem decodeQBF_encQBF (φ : QBF ℕ) : decodeQBF (encQBF φ) = φ :=
   encQBF.injective (by simp [encQBF_decodeQBF, (isCode_iff _).mpr ⟨φ, rfl⟩])
 
 end Cslib.Complexity.TQBF

Complexity/Computability/Complexity/Classes/SharpP/Products.lean

@@ -144,7 +144,7 @@ theorem prod_sub_mul_eq_sum {n : ℕ} (f g : Fin n → ℤ) (c : ℤ) :
 
 /-- Expanding a product of differences over Boolean choices: each term selects `g i` where `w i` is
 true and `f i` where `w i` is false, weighted by `(-1)` to the number of true bits. -/
-private theorem prod_sub_eq_sum {n : ℕ} (f g : Fin n → ℤ) :
+theorem prod_sub_eq_sum {n : ℕ} (f g : Fin n → ℤ) :
     (∏ i, (f i - g i)) = ∑ w : Fin n → Bool,
       (-1 : ℤ) ^ (List.ofFn w).countP id * ∏ i, if w i then g i else f i := by
   simpa using prod_sub_mul_eq_sum f g 1

Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean

@@ -82,7 +82,7 @@ theorem tokens_conj (l : List (QBF ℕ)) :
   | nil => rfl
   | cons φ l ih => simpa [conj, tokens] using ih
 
-private theorem tokens_imp (φ ψ : QBF ℕ) :
+theorem tokens_imp (φ ψ : QBF ℕ) :
     (imp φ ψ).tokens = (Kind.or, 0) :: (Kind.not, 0) :: (φ.tokens ++ ψ.tokens) := rfl
 
 theorem tokens_iff (φ ψ : QBF ℕ) : (iff φ ψ).tokens =

Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean

@@ -644,7 +644,7 @@ theorem PPAD_subset_PPP : PPAD enc ⊆ PPP enc := by
 
 /-- Every directed end-of-line family search-reduces to its associated bipartite undirected parity
 family. -/
-private theorem endOfLineRel_searchReducible_leafRel {n : α → ℕ} {P S : α × List Bool → List Bool}
+theorem endOfLineRel_searchReducible_leafRel {n : α → ℕ} {P S : α × List Bool → List Bool}
     (hP_len : ∀ a u, u.length = n a → (P (a, u)).length = n a)
     (hS_len : ∀ a u, u.length = n a → (S (a, u)).length = n a) :
     SearchReducible enc enc (endOfLineRel n P S)

Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean

@@ -293,7 +293,7 @@ private theorem eval_hashCNF (σ : Var → Bool) (vars : List ℕ) (k : ℕ) (w
 
 /-- A sequence that starts at `c` and adds `f j` at each step `j < n` holds `c + ∑ j' < j, f j'`
 up to step `n`. -/
-private theorem eq_add_sum_of_step {z f : ℕ → Bool} {c : Bool} {n : ℕ} (h0 : z 0 = c)
+theorem eq_add_sum_of_step {z f : ℕ → Bool} {c : Bool} {n : ℕ} (h0 : z 0 = c)
     (hstep : ∀ j < n, z (j + 1) = (z j ^^ f j)) :
     ∀ j ≤ n, z j = c + ∑ j' ∈ Finset.range j, f j' := by
   intro j hj
@@ -401,7 +401,7 @@ private theorem mem_vars_hashCNF {vars : List ℕ} {k : ℕ} {w : List Bool} {u
 
 /-- **Soundness.** A satisfying assignment of the reduced formula restricts to one of `φ`: the
 equations only add constraints. -/
-private theorem satisfiable_of_satisfiable_reduceWith {φ : CNF ℕ} {k : ℕ} {w : List Bool}
+theorem satisfiable_of_satisfiable_reduceWith {φ : CNF ℕ} {k : ℕ} {w : List Bool}
     (h : (reduceWith φ k w).Satisfiable) : φ.Satisfiable := by
   obtain ⟨τ, hτ⟩ := h
   simp only [reduceWith, CNF.eval_relabel, CNF.eval_append, Bool.and_eq_true] at hτ
@@ -418,7 +418,7 @@ open Classical in
 noncomputable def solutions (φ : CNF ℕ) : Finset (BitString φ.vars.length) :=
   Finset.univ.filter fun x => ∃ σ : ℕ → Bool, φ.eval σ = true ∧ point φ.vars σ = x
 
-private theorem mem_solutions {φ : CNF ℕ} {x : BitString φ.vars.length} :
+theorem mem_solutions {φ : CNF ℕ} {x : BitString φ.vars.length} :
     x ∈ solutions φ ↔ ∃ σ : ℕ → Bool, φ.eval σ = true ∧ point φ.vars σ = x := by
   simp [solutions]
 
@@ -494,7 +494,7 @@ solutions, `2 ^ (log₂ s + 2)` lies between `2 s` and `4 s`. -/
 private noncomputable def goodRows (φ : CNF ℕ) : ℕ := Nat.log 2 (solutions φ).card + 2
 
 /-- A satisfiable formula has a solution. -/
-private theorem solutions_nonempty {φ : CNF ℕ} (hφ : φ.Satisfiable) : (solutions φ).Nonempty :=
+theorem solutions_nonempty {φ : CNF ℕ} (hφ : φ.Satisfiable) : (solutions φ).Nonempty :=
   let ⟨σ, hσ⟩ := hφ
   ⟨_, mem_solutions.2 ⟨σ, hσ, rfl⟩⟩
 

Complexity/Computability/Complexity/Fagin/Converse.lean

@@ -99,10 +99,10 @@ arities of `v`. -/
 def maxArity : ℕ :=
   Finset.univ.sup v.arity + 1
 
-private theorem one_le_maxArity : 1 ≤ v.maxArity :=
+theorem one_le_maxArity : 1 ≤ v.maxArity :=
   Nat.le_add_left 1 _
 
-private theorem arity_le_maxArity (i : Fin v.count) : v.arity i ≤ v.maxArity :=
+theorem arity_le_maxArity (i : Fin v.count) : v.arity i ≤ v.maxArity :=
   (Finset.le_sup (Finset.mem_univ i)).trans (Nat.le_add_right _ 1)
 
 /-- For a well-formed input `a` with `1 ≤ a.1`, the `m`-th prefix of `encStructure a` has length at

Complexity/Computability/Complexity/Fagin/Ordered.lean

@@ -61,7 +61,7 @@ theorem Definable.esoDefinable {L : Language.{u, v}} {K : Query L} (hK : Definab
 
 /-- The existing fixed-sentence encoding is exactly the new arbitrary-query encoding applied
 to the class defined by that sentence. Its size and shape rejection behavior is unchanged. -/
-private theorem encodedLanguage_sentence {L : Language} [L.IsRelational] (v : Vocabulary L)
+theorem encodedLanguage_sentence {L : Language} [L.IsRelational] (v : Vocabulary L)
     (φ : (language L).Sentence) :
     Query.encodedLanguage {M : Ordered.Structure L | φ.Realize M} v =
       queryLanguage v φ := rfl

Complexity/Computability/Complexity/Fagin/StrictVerifier.lean

@@ -74,7 +74,7 @@ theorem strictVerifier_eq_true_iff (enc : α ↪ List Bool) (p : Polynomial ℕ)
       w.length = p.eval (enc a).length ∧ V (a, w) = true := by
   simp [strictVerifier]
 
-private theorem length_eq_of_strictVerifier_eq_true {enc : α ↪ List Bool} {p : Polynomial ℕ}
+theorem length_eq_of_strictVerifier_eq_true {enc : α ↪ List Bool} {p : Polynomial ℕ}
     {V : α × List Bool → Bool} {a : α} {w : List Bool}
     (h : strictVerifier enc p V (a, w) = true) :
     w.length = p.eval (enc a).length :=

Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean

@@ -717,7 +717,7 @@ theorem computableInPolyTime_bussKernel :
   .of_tidy (computableTidilyInPolyTime_bussKernel)
 
 /-- Buss's kernel has target at most `k`, or `1`. -/
-private theorem bussKernel_snd_le (x : Graph × ℕ) : (bussKernel x).2 ≤ max x.2 1 := by
+theorem bussKernel_snd_le (x : Graph × ℕ) : (bussKernel x).2 ≤ max x.2 1 := by
   unfold bussKernel
   split_ifs with h
   · exact le_max_of_le_left ((param_le_cap x).trans (cap_le_snd x))

Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean

@@ -64,7 +64,7 @@ namespace Graph
 def adjIndex (G : Graph) (i j : ℕ) : Bool :=
   G.adjBool (G.distinctVertices.getD i 0) (G.distinctVertices.getD j 0)
 
-private theorem induced_adj_vertexEquiv (G : Graph) (i j : Fin G.distinctVertices.length) :
+theorem induced_adj_vertexEquiv (G : Graph) (i j : Fin G.distinctVertices.length) :
     G.induced.Adj (G.vertexEquiv i) (G.vertexEquiv j) ↔ G.adjIndex i j = true := by
   rw [induced_adj, adjIndex, adjBool_eq_true_iff, vertexEquiv_apply, vertexEquiv_apply]
 

Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean

@@ -92,7 +92,7 @@ private theorem eq_of_idxOf_eq {G : Graph} {u v : ℕ} (hv : v ∈ G.1)
   ((List.idxOf_inj hv).1 h.symm).symm
 
 /-- Gadget vertices of a declared vertex determine the vertex and the position in the gadget. -/
-private theorem splitVertex_eq_splitVertex_iff_of_mem {G : Graph} {u v r r' : ℕ} (hv : v ∈ G.1) :
+theorem splitVertex_eq_splitVertex_iff_of_mem {G : Graph} {u v r r' : ℕ} (hv : v ∈ G.1) :
     G.splitVertex u r = G.splitVertex v r' ↔ u = v ∧ r = r' := by
   rw [splitVertex_eq_splitVertex_iff]
   exact ⟨fun h => ⟨eq_of_idxOf_eq hv h.1, h.2⟩, fun h => ⟨h.1 ▸ rfl, h.2⟩⟩

Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean

@@ -81,7 +81,7 @@ theorem exists_maskSelect_eq {s l : List α} (h : s <+ l) :
     exact ⟨true :: w, by simp [hw], by simp [maskSelect_cons, hs]⟩
 
 /-- Unselected positions beyond the list do not change the selection. -/
-private theorem maskSelect_append_replicate_false (l : List α) (w : List Bool) (k : ℕ) :
+theorem maskSelect_append_replicate_false (l : List α) (w : List Bool) (k : ℕ) :
     maskSelect l (w ++ List.replicate k false) = maskSelect l w := by
   unfold maskSelect
   congr 2

Complexity/Computability/Complexity/Problems/TQBF/Closed.lean

@@ -67,7 +67,7 @@ theorem mem_freeVarList {φ : QBF ℕ} {x : ℕ} : x ∈ φ.freeVarList ↔ x 
   | all v φ ih => simp [freeVarList, ih, and_comm]
 
 /-- A formula is closed exactly when its list of free variables is empty. -/
-private theorem closed_iff_freeVarList_eq_nil {φ : QBF ℕ} : φ.Closed ↔ φ.freeVarList = [] := by
+theorem closed_iff_freeVarList_eq_nil {φ : QBF ℕ} : φ.Closed ↔ φ.freeVarList = [] := by
   rw [Closed, Finset.eq_empty_iff_forall_notMem, List.eq_nil_iff_forall_not_mem]
   exact forall_congr' fun x => not_congr mem_freeVarList.symm
 

Complexity/Computability/Kolmogorov/TimeBounded.lean

@@ -165,7 +165,7 @@ theorem mem_universalTMRunFor_iff_simulate {p x : List Bool} {t : ℕ} :
   rcases simulate (decodeDesc (unframe p)) ((dropFrame p).map eBit) t with ⟨out, _ | _⟩ <;>
     simp [eq_comm]
 
-private theorem universalTMRunFor_mono (p : List Bool) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {x : List Bool}
+theorem universalTMRunFor_mono (p : List Bool) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {x : List Bool}
     (h : x ∈ universalTMRunFor p t₁) :
     x ∈ universalTMRunFor p t₂ := by
   obtain ⟨out, hout, rfl⟩ := mem_universalTMRunFor_iff.mp h

Complexity/Computability/PCP/Approximation/Hastad.lean

@@ -84,7 +84,7 @@ section LabelCoverSoundness
 `W : I → α → ℝ`, and vertex-wise sub-probability distributions `p : ℕ → α → ℝ` (`0 ≤ p u a` and
 `∑ a, p u a ≤ 1`), choosing the best label at each vertex produces a deterministic assignment
 `f : ℕ → α` whose payoff is at least the expected payoff under `p`. -/
-private theorem exists_choice_sum_le {I α : Type*} [Fintype I] [Fintype α] [Nonempty α]
+theorem exists_choice_sum_le {I α : Type*} [Fintype I] [Fintype α] [Nonempty α]
     (v : I → ℕ) (W : I → α → ℝ) (hW : ∀ i a, 0 ≤ W i a)
     (p : ℕ → α → ℝ) (hp0 : ∀ u a, 0 ≤ p u a) (hp1 : ∀ u, ∑ a : α, p u a ≤ 1) :
     ∃ f : ℕ → α, (∑ i : I, ∑ a : α, p (v i) a * W i a) ≤ ∑ i : I, W i (f (v i)) := by