diff --git a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean b/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
index 90e496368..397a3b99b 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean b/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
index 824b3cee8..cefebe844 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean
+++ b/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]
diff --git a/Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean b/Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean
index cf0962866..f38b96205 100644
--- a/Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean
index 79095d14a..3d92f474f 100644
--- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean
+++ b/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`. -/
diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean
index f1a3e5193..1e4e48f7b 100644
--- a/Complexity/Computability/Complexity/Classes/IP.lean
+++ b/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'⟩
diff --git a/Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean b/Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean
index 2864ff24a..2640ad9e0 100644
--- a/Complexity/Computability/Complexity/Classes/IP/CoinFixing.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean b/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
index beb8f5edb..7898a3887 100644
--- a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Tokens.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Tokens.lean
index 79b75c240..b3b607d43 100644
--- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Tokens.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean b/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
index 700bea176..b2dae7d75 100644
--- a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean b/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean
index 8ded46fff..25d594997 100644
--- a/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean
+++ b/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]
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean
index 2b052da52..11ecbc7dd 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean b/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean
index 249ac321d..3fee1aaa6 100644
--- a/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/Oracle.lean b/Complexity/Computability/Complexity/Classes/Oracle.lean
index 94a052078..3753c556b 100644
--- a/Complexity/Computability/Complexity/Classes/Oracle.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean b/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean
index 8f83eba80..8adaf1c69 100644
--- a/Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Products.lean b/Complexity/Computability/Complexity/Classes/SharpP/Products.lean
index 872abd16e..76b3dcb17 100644
--- a/Complexity/Computability/Complexity/Classes/SharpP/Products.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean b/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean
index 1dce8e14f..7815c1f37 100644
--- a/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean
+++ b/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 =
diff --git a/Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean b/Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean
index 9ffdace10..628fa7a5e 100644
--- a/Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean
+++ b/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)
diff --git a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean b/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean
index 1f7cd22a4..b9fbe5243 100644
--- a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean
+++ b/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⟩⟩
 
diff --git a/Complexity/Computability/Complexity/Fagin/Converse.lean b/Complexity/Computability/Complexity/Fagin/Converse.lean
index 53655043d..5ce03eb7d 100644
--- a/Complexity/Computability/Complexity/Fagin/Converse.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Fagin/Ordered.lean b/Complexity/Computability/Complexity/Fagin/Ordered.lean
index 79ce4f7c6..38caac214 100644
--- a/Complexity/Computability/Complexity/Fagin/Ordered.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean b/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean
index 5ad17f272..fee414ce9 100644
--- a/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean
+++ b/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 :=
diff --git a/Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean b/Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean
index e49fe8547..90eea8c4f 100644
--- a/Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean
+++ b/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))
diff --git a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean b/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean
index 2ec5a845f..cd54246ae 100644
--- a/Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean
+++ b/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]
 
diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean
index d070809f1..06857e0db 100644
--- a/Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean
+++ b/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⟩⟩
diff --git a/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean b/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean
index 7c95c6bc9..c4d781faa 100644
--- a/Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean
+++ b/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
diff --git a/Complexity/Computability/Complexity/Problems/TQBF/Closed.lean b/Complexity/Computability/Complexity/Problems/TQBF/Closed.lean
index fbed2fd07..896d71dd7 100644
--- a/Complexity/Computability/Complexity/Problems/TQBF/Closed.lean
+++ b/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
 
diff --git a/Complexity/Computability/Kolmogorov/TimeBounded.lean b/Complexity/Computability/Kolmogorov/TimeBounded.lean
index dff4c94c0..90d9a6bad 100644
--- a/Complexity/Computability/Kolmogorov/TimeBounded.lean
+++ b/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
diff --git a/Complexity/Computability/PCP/Approximation/Hastad.lean b/Complexity/Computability/PCP/Approximation/Hastad.lean
index 1befe1026..25d805683 100644
--- a/Complexity/Computability/PCP/Approximation/Hastad.lean
+++ b/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
diff --git a/Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean b/Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean
index 68e09218f..8901229a1 100644
--- a/Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean
+++ b/Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean
@@ -116,13 +116,13 @@ def reduce (φ : CNF ℕ) : CNF ℕ :=
   if φ.any List.isEmpty then contradiction else toExactThreeSAT φ
 
 /-- Padding the clauses does not change the number of clauses an assignment falsifies. -/
-private theorem countUnsat_toExactThreeSAT (σ : ℕ → Bool) (φ : CNF ℕ) :
+theorem countUnsat_toExactThreeSAT (σ : ℕ → Bool) (φ : CNF ℕ) :
     (toExactThreeSAT φ).countUnsat σ = φ.countUnsat σ := by
   simp only [toExactThreeSAT, CNF.countUnsat, List.countP_map, Function.comp_def,
     ExactThreeSAT.eval_padClause]
 
 /-- Padding the clauses does not change the value of a formula. -/
-private theorem unsatVal_toExactThreeSAT (φ : CNF ℕ) :
+theorem unsatVal_toExactThreeSAT (φ : CNF ℕ) :
     (toExactThreeSAT φ).unsatVal = φ.unsatVal := by
   unfold CNF.unsatVal
   simp only [countUnsat_toExactThreeSAT]
diff --git a/Complexity/Computability/PCP/AssignmentTester.lean b/Complexity/Computability/PCP/AssignmentTester.lean
index 7b10ade18..a0a3ca3d2 100644
--- a/Complexity/Computability/PCP/AssignmentTester.lean
+++ b/Complexity/Computability/PCP/AssignmentTester.lean
@@ -270,7 +270,7 @@ def blrTest : LocalTest (ι → Bool) ((ι → Bool) × (ι → Bool)) (Fin 3) B
   Accepts _ a := (a 0 ^^ a 1) = a 2
 
 /-- The linearity test accepts with the probability `blrAcceptance`. -/
-private theorem acceptProb_blrTest [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
+theorem acceptProb_blrTest [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
     (blrTest ι).acceptProb f = blrAcceptance f := by
   simp only [LocalTest.acceptProb, Fintype.expect_prod_type, LocalTest.Passes, blrTest,
     blrAcceptance, Matrix.cons_val]
@@ -289,7 +289,7 @@ def tensorTest : LocalTest ((ι → Bool) ⊕ (ι × ι → Bool))
   Accepts _ a := (a 0 ^^ a 1) = ((a 2 ^^ a 3) && (a 4 ^^ a 5))
 
 /-- The tensor test accepts with the probability `tensorTestAcceptance`. -/
-private theorem acceptProb_tensorTest [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool)
+theorem acceptProb_tensorTest [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool)
     (g : (ι × ι → Bool) → Bool) :
     (tensorTest ι).acceptProb (Sum.elim f g) = tensorTestAcceptance f g := by
   simp only [LocalTest.acceptProb, Fintype.expect_prod_type, LocalTest.Passes, tensorTest,
@@ -308,7 +308,7 @@ def equationTest [Fintype κ] (A : κ → ι → Bool) (b : κ → Bool) :
   Accepts ω a := (a 0 ^^ a 1) = hadamardCode ω.1 b
 
 /-- The equation test accepts with the probability `equationTestAcceptance`. -/
-private theorem acceptProb_equationTest [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
+theorem acceptProb_equationTest [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
     (g : (ι → Bool) → Bool) (A : κ → ι → Bool) (b : κ → Bool) :
     (equationTest A b).acceptProb g = equationTestAcceptance g A b := by
   simp only [LocalTest.acceptProb, Fintype.expect_prod_type, LocalTest.Passes, equationTest,
diff --git a/Complexity/Computability/PCP/DegreeReduction.lean b/Complexity/Computability/PCP/DegreeReduction.lean
index 56a651d4c..61144a7fb 100644
--- a/Complexity/Computability/PCP/DegreeReduction.lean
+++ b/Complexity/Computability/PCP/DegreeReduction.lean
@@ -209,7 +209,7 @@ private theorem card_darts_degreeReduce :
 
 /-- The labelling of the half-edges by the labels of their vertices violates only the edge-links
 of the edges violated by the labelling of the vertices. -/
-private theorem card_unsatEdges_degreeReduce_comp_endpoint_le (σ : V → α) :
+theorem card_unsatEdges_degreeReduce_comp_endpoint_le (σ : V → α) :
     #((G.degreeReduce H).toConstraintGraph.unsatEdges (σ ∘ G.endpoint)) ≤
       2 * #(G.unsatEdges σ) := by
   classical
@@ -356,7 +356,7 @@ private theorem mul_card_filter_ne_le_card_filter_isRight [DecidableEq α]
 clouds have spectral expansion at most `μ`, every labelling of the half-edges violates a proportion
 of the darts at least `min 1 ((1 - μ) |D|) / (2 (1 + |D|))` times the value of `G`, whatever the
 alphabet. -/
-private theorem le_unsatFrac_degreeReduce [Nonempty α] (hH : ∀ v, (H v).spectralExpansion ≤ μ)
+theorem le_unsatFrac_degreeReduce [Nonempty α] (hH : ∀ v, (H v).spectralExpansion ≤ μ)
     (A : E × Bool → α) :
     min 1 ((1 - μ) * Fintype.card D) / (2 * (1 + Fintype.card D)) * G.unsatVal ≤
       (G.degreeReduce H).toConstraintGraph.unsatFrac A := by
diff --git a/Complexity/Computability/PCP/Encoded/Constraints.lean b/Complexity/Computability/PCP/Encoded/Constraints.lean
index e6977996d..2f1721183 100644
--- a/Complexity/Computability/PCP/Encoded/Constraints.lean
+++ b/Complexity/Computability/PCP/Encoded/Constraints.lean
@@ -156,7 +156,7 @@ theorem length_constraintTable_le [Fintype α] (table : α → α → Bool) :
 
 /-- Bounded growth per descriptor gives bounded total encoded growth. Both the inner edge
 encoding and the outer list framing are charged. -/
-private theorem length_encoding_mapConstraints_le (g : Graph C) (f : C → C') (bound : ℕ)
+theorem length_encoding_mapConstraints_le (g : Graph C) (f : C → C') (bound : ℕ)
     (hf : ∀ c, (enc' (f c)).length ≤ (enc c).length + bound) :
     (encoding enc' (g.mapConstraints f)).length ≤
       (encoding enc g).length + 2 * g.edges.length * bound := by
diff --git a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
index eed80b6e5..455cc5c53 100644
--- a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
+++ b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
@@ -51,7 +51,7 @@ def clauseHolds (κ : Clause ℕ) (a : Fin 3 → Bool) : Bool :=
   (List.finRange 3).any fun q => κ[q.val]?.elim false (fun l => a q == l.2)
 
 /-- The Boolean test agrees with the existing mathematical clause predicate. -/
-private theorem clauseHolds_eq_true (κ : Clause ℕ) (a : Fin 3 → Bool) :
+theorem clauseHolds_eq_true (κ : Clause ℕ) (a : Fin 3 → Bool) :
     clauseHolds κ a = true ↔ ConstraintGraph.ClauseHolds κ a := by
   simp only [clauseHolds, List.any_eq_true, List.mem_finRange, true_and,
     ConstraintGraph.ClauseHolds]
@@ -210,7 +210,7 @@ theorem satisfiable_ofCNF_iff (variableCount : ℕ) (φ : CNF ℕ)
   exact ConstraintGraph.satisfiable_ofCNF_iff φ h3
 
 /-- Bounded variable names ensure every generated endpoint lies in the declared vertex range. -/
-private theorem wellFormed_ofCNF (variableCount : ℕ) (φ : CNF ℕ)
+theorem wellFormed_ofCNF (variableCount : ℕ) (φ : CNF ℕ)
     (hvars : ∀ v ∈ φ.vars, v < variableCount) : (ofCNF variableCount φ).WellFormed := by
   intro e he
   obtain ⟨⟨j, q⟩, hp, rfl⟩ := List.mem_map.mp he
diff --git a/Complexity/Computability/PCP/Encoded/Verifier/Soundness.lean b/Complexity/Computability/PCP/Encoded/Verifier/Soundness.lean
index 6de5f464f..3e35ab9e0 100644
--- a/Complexity/Computability/PCP/Encoded/Verifier/Soundness.lean
+++ b/Complexity/Computability/PCP/Encoded/Verifier/Soundness.lean
@@ -106,7 +106,7 @@ theorem rejectProb_edgeVerifier (width : ℕ) (decode : (Fin width → Bool) →
     labels]
 
 /-- Rounding the edge sampling range to a power of two loses at most half the rejection rate. -/
-private theorem unsatFrac_div_two_le_rejectProb (width : ℕ) (decode : (Fin width → Bool) → α)
+theorem unsatFrac_div_two_le_rejectProb (width : ℕ) (decode : (Fin width → Bool) → α)
     (eval : C → α → α → Bool) (g : Graph C) (proof : List Bool) :
     (g.toGraph eval).unsatFrac (proofLabels width decode proof) / 2 ≤
       (((BitString.uniformList (Nat.clog 2 g.edges.length)).map
diff --git a/Complexity/Computability/PCP/ThreeSAT.lean b/Complexity/Computability/PCP/ThreeSAT.lean
index 760d8f826..11d115fd9 100644
--- a/Complexity/Computability/PCP/ThreeSAT.lean
+++ b/Complexity/Computability/PCP/ThreeSAT.lean
@@ -193,7 +193,7 @@ private theorem card_edges_ofCNF : Fintype.card (Fin φ.length × Fin 3) = 3 * 
 
 /-- **Soundness**: a labelling violates at least a third of the proportion of clauses that the
 assignment read off from it falsifies. -/
-private theorem countUnsat_div_le_unsatFrac (A : V ⊕ Fin φ.length → Fin 3 → Bool) :
+theorem countUnsat_div_le_unsatFrac (A : V ⊕ Fin φ.length → Fin 3 → Bool) :
     (φ.countUnsat (cnfAssignment A) : ℝ) / φ.length / 3 ≤ (ofCNF φ).unsatFrac A := by
   rw [unsatFrac, card_edges_ofCNF, Nat.cast_mul, div_div, mul_comm (φ.length : ℝ), Nat.cast_ofNat]
   gcongr
diff --git a/Complexity/Computability/TreeEval/Reader/Arith.lean b/Complexity/Computability/TreeEval/Reader/Arith.lean
index 8a7e75a2f..05e7806ec 100644
--- a/Complexity/Computability/TreeEval/Reader/Arith.lean
+++ b/Complexity/Computability/TreeEval/Reader/Arith.lean
@@ -84,7 +84,7 @@ variable [Fact p.Prime]
     simp [sgnVal, Iter.sgn, Nat.cast_sub this.le]
 
 /-- Fermat: a nonzero residue to the power `p - 2` is its inverse. -/
-private theorem pow_sub_two_eq_inv {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 2) = a⁻¹ := by
+theorem pow_sub_two_eq_inv {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 2) = a⁻¹ := by
   have hp := (Fact.out : p.Prime).two_le
   refine eq_inv_of_mul_eq_one_left ?_
   rw [← pow_succ, show p - 2 + 1 = p - 1 by omega, ZMod.pow_card_sub_one_eq_one ha]
diff --git a/Complexity/Computability/TreeEval/Reader/Correct.lean b/Complexity/Computability/TreeEval/Reader/Correct.lean
index b58fb964f..019e407ee 100644
--- a/Complexity/Computability/TreeEval/Reader/Correct.lean
+++ b/Complexity/Computability/TreeEval/Reader/Correct.lean
@@ -120,7 +120,7 @@ private theorem runFrom_leaf {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin
 
 /-- Sums over the positions of a table of `n` blocks of `ℓ` bits whose position within the block
 is `i`, as sums over the blocks. -/
-private theorem sum_range_mul_ite_mod {M : Type*} [AddCommMonoid M] (n : ℕ) {i : ℕ} (hi : i < ℓ)
+theorem sum_range_mul_ite_mod {M : Type*} [AddCommMonoid M] (n : ℕ) {i : ℕ} (hi : i < ℓ)
     (F : ℕ → M) :
     ∑ q ∈ Finset.range (n * ℓ), (if q % ℓ = i then F q else 0) =
       ∑ k ∈ Finset.range n, F (k * ℓ + i) := by
@@ -187,7 +187,7 @@ private theorem runFrom_scan_loop {p : ℕ} [Fact p.Prime] {fr : Frame} {st : Li
         · simp [hb, hi, modifyAt, List.getD_eq_getElem?_getD]
       · simp [hb, BitString.bitVal]
 
-private theorem mul_add_div_self (k : ℕ) (i : Fin ℓ) : (k * ℓ + i) / ℓ = k := by
+theorem mul_add_div_self (k : ℕ) (i : Fin ℓ) : (k * ℓ + i) / ℓ = k := by
   rw [Nat.add_comm, Nat.add_mul_div_right _ _ (Nat.zero_lt_of_lt i.isLt), Nat.div_eq_of_lt i.isLt,
     zero_add]
 
diff --git a/Complexity/MachineLearning/UniformLearning/Basic.lean b/Complexity/MachineLearning/UniformLearning/Basic.lean
index 21fcf1c89..777cbc4ed 100644
--- a/Complexity/MachineLearning/UniformLearning/Basic.lean
+++ b/Complexity/MachineLearning/UniformLearning/Basic.lean
@@ -119,7 +119,7 @@ theorem uniformError_le_one (f h : (ι → Bool) → Bool) : uniformError f h 
   exact_mod_cast this
 
 /-- The error is the probability that a uniform point is misclassified. -/
-private theorem toOuterMeasure_uniformOfFintype_ne (f h : (ι → Bool) → Bool) :
+theorem toOuterMeasure_uniformOfFintype_ne (f h : (ι → Bool) → Bool) :
     (PMF.uniformOfFintype (ι → Bool)).toOuterMeasure {x | h x ≠ f x} =
       ENNReal.ofReal (uniformError f h) := by
   rw [← ENNReal.ofReal_toReal (PMF.toOuterMeasure_ne_top _ _), PMF.toOuterMeasure_apply_toReal]