diff --git a/Complexity/Computability/Circuit/Approximation.lean b/Complexity/Computability/Circuit/Approximation.lean
index 0e5e35c0a..fde5f723d 100644
--- a/Complexity/Computability/Circuit/Approximation.lean
+++ b/Complexity/Computability/Circuit/Approximation.lean
@@ -94,7 +94,7 @@ def programExceptions : ∀ {g : ℕ}, Program σ n g → Finset Sample
   rfl
 
 /-- There are at most as many exceptions as the total cost of the gates. -/
-private theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
+theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
     (S.programExceptions p).card ≤ p.cost S.errorCost := by
   induction p with
   | empty => simp
@@ -125,7 +125,7 @@ theorem program_correct {g : ℕ} (p : Program σ n g) {s : Sample}
     | castSucc w => simpa only [Program.trace_gate_castSucc] using ih hs.1 w
 
 /-- Away from the exceptions, every output of a circuit is correct. -/
-private theorem circuit_correct {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample}
+theorem circuit_correct {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample}
     (hs : s ∉ S.programExceptions C.program) :
     S.relation (C.eval exact (exactInput s) o) (decode (C.eval approx approxInput o) s) :=
   S.program_correct C.program hs (C.outputs o)
diff --git a/Complexity/Computability/Circuit/Clique.lean b/Complexity/Computability/Circuit/Clique.lean
index 41b776535..ba4e6dcce 100644
--- a/Complexity/Computability/Circuit/Clique.lean
+++ b/Complexity/Computability/Circuit/Clique.lean
@@ -152,7 +152,7 @@ theorem contains_ofColoring_iff {c : Fin n → Fin r} {s : Finset (Fin n)} :
 
 /-- A set with all edges inside in the graph of a colouring with `r` colours has at most `r`
 vertices. -/
-private theorem card_le_of_contains_ofColoring {c : Fin n → Fin r} {s : Finset (Fin n)}
+theorem card_le_of_contains_ofColoring {c : Fin n → Fin r} {s : Finset (Fin n)}
     (h : Contains (ofColoring c) s) : s.card ≤ r := by
   simpa using Finset.card_le_card_of_injOn c (fun _ _ => Finset.mem_univ _)
     (contains_ofColoring_iff.1 h)
diff --git a/Complexity/Computability/Circuit/Cyclic/Feedback.lean b/Complexity/Computability/Circuit/Cyclic/Feedback.lean
index 34d4afec9..7a375d6c6 100644
--- a/Complexity/Computability/Circuit/Cyclic/Feedback.lean
+++ b/Complexity/Computability/Circuit/Cyclic/Feedback.lean
@@ -55,7 +55,7 @@ def feedbackWire (feed : Fin k → Fin g) : Wire (n + k) g → Wire n g :=
   Wire.elim (Fin.addCases Wire.input (Wire.gate ∘ feed)) Wire.gate
 
 /-- Reading a feedback wire is reading the original wire with the selected gate values as state. -/
-private theorem elim_feedbackWire (feed : Fin k → Fin g) (input : Fin n → U) (state : Fin g → U)
+theorem elim_feedbackWire (feed : Fin k → Fin g) (input : Fin n → U) (state : Fin g → U)
     (wire : Wire (n + k) g) :
     Wire.elim input state (feedbackWire feed wire) =
       Wire.elim (Fin.append input (state ∘ feed)) state wire := by
diff --git a/Complexity/Computability/Circuit/Encoding/MapOp.lean b/Complexity/Computability/Circuit/Encoding/MapOp.lean
index 9fc6627c1..f0d37a4eb 100644
--- a/Complexity/Computability/Circuit/Encoding/MapOp.lean
+++ b/Complexity/Computability/Circuit/Encoding/MapOp.lean
@@ -29,7 +29,7 @@ namespace Cslib.Circuits
 variable {σ τ : Signature} (φ : σ.Hom τ) {n g m : ℕ}
 
 /-- The code of a translated line: the translated operation on the same wires. -/
-private theorem Line.code_mapOp (line : Line σ n g) :
+theorem Line.code_mapOp (line : Line σ n g) :
     (line.mapOp φ).code = (φ line.op, line.code.2) := by
   simp only [Line.code, Line.mapOp_op, Line.mapOp_wires]
   congr 1
@@ -37,7 +37,7 @@ private theorem Line.code_mapOp (line : Line σ n g) :
   simp
 
 /-- The code of a translated program: the operations of its gates translated. -/
-private theorem Program.code_mapOp (p : Program σ n g) :
+theorem Program.code_mapOp (p : Program σ n g) :
     (p.mapOp φ).code = p.code.map fun g => (φ g.1, g.2) := by
   induction p with
   | empty => rfl
diff --git a/Complexity/Computability/Circuit/Erase.lean b/Complexity/Computability/Circuit/Erase.lean
index 1683253c2..fb235978f 100644
--- a/Complexity/Computability/Circuit/Erase.lean
+++ b/Complexity/Computability/Circuit/Erase.lean
@@ -108,7 +108,7 @@ def Program.replaceGates : {s : ℕ} → Program σ n s → (Fin s → Option P)
       ((r (Fin.last _)).elim line.liftConstants Line.const)
 
 /-- The lines of a program with gates replaced by constants. -/
-private theorem Program.lines_replaceGates (p : Program σ n s) (r : Fin s → Option P) (g : Fin s) :
+theorem Program.lines_replaceGates (p : Program σ n s) (r : Fin s → Option P) (g : Fin s) :
     (p.replaceGates r).lines g = (r g).elim (p.lines g).liftConstants Line.const := by
   induction p with
   | empty => exact g.elim0
@@ -137,18 +137,18 @@ theorem Program.lines_eraseGates (p : Program σ n s) (g : Fin s) :
   rw [eraseGates, lines_replaceGates]
   split_ifs <;> rfl
 
-private theorem Program.lines_eraseGates_of_special (p : Program σ n s) {g : Fin s}
+theorem Program.lines_eraseGates_of_special (p : Program σ n s) {g : Fin s}
     (hg : special g) :
     (p.eraseGates special).lines g = Line.const ⟨g, hg⟩ := by
   simp only [lines_eraseGates, hg, ↓reduceDIte]
 
-private theorem Program.lines_eraseGates_of_not_special (p : Program σ n s) {g : Fin s}
+theorem Program.lines_eraseGates_of_not_special (p : Program σ n s) {g : Fin s}
     (hg : ¬special g) : (p.eraseGates special).lines g = (p.lines g).liftConstants := by
   simp only [lines_eraseGates, hg, ↓reduceDIte]
 
 /-- The arity of a gate of the erased program: zero for a special gate, and the arity of the
 gate otherwise. -/
-private theorem Program.arity_lines_eraseGates (p : Program σ n s) (g : Fin s) :
+theorem Program.arity_lines_eraseGates (p : Program σ n s) (g : Fin s) :
     (σ.withConstants {g // special g}).Arity ((p.eraseGates special).lines g).op =
       if special g then 0 else σ.Arity (p.lines g).op := by
   by_cases hg : special g
diff --git a/Complexity/Computability/Circuit/FanIn.lean b/Complexity/Computability/Circuit/FanIn.lean
index 09a2176b1..0db392b9a 100644
--- a/Complexity/Computability/Circuit/FanIn.lean
+++ b/Complexity/Computability/Circuit/FanIn.lean
@@ -240,7 +240,7 @@ theorem Circuit.essential_le_size
 
 /-- In a program of fan-in `r`, a wire of depth `d` is supported by at most `max 1 r ^ d`
 inputs. -/
-private theorem Program.card_wireSupport_le_pow {r : ℕ} :
+theorem Program.card_wireSupport_le_pow {r : ℕ} :
     ∀ {g : ℕ} {p : Program σ n g}, p.FanInAtMost r →
       ∀ w : Wire n g, (p.wireSupport w).card ≤ max 1 r ^ p.wireDepths w
   | _, .empty, _, .input i => by simp
diff --git a/Complexity/Computability/Circuit/Frontier/AverageCase.lean b/Complexity/Computability/Circuit/Frontier/AverageCase.lean
index ebcb1dff4..9d026c67e 100644
--- a/Complexity/Computability/Circuit/Frontier/AverageCase.lean
+++ b/Complexity/Computability/Circuit/Frontier/AverageCase.lean
@@ -88,7 +88,7 @@ section Finite
 variable [Finite ι] [Finite U]
 
 /-- Membership in `S` agrees with membership in `T` or with membership in `Tᶜ`. -/
-private theorem agreement_add_agreement_compl [Nonempty U] (S T : Set (ι → U)) :
+theorem agreement_add_agreement_compl [Nonempty U] (S T : Set (ι → U)) :
     agreement S T + agreement S Tᶜ = 1 := by
   have hN : (0 : ℝ) < Nat.card (ι → U) := by exact_mod_cast Nat.card_pos
   have hcompl : {x : ι → U | x ∈ S ↔ x ∈ Tᶜ} = {x | x ∈ S ↔ x ∈ T}ᶜ := by
diff --git a/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean b/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean
index 0e654bbcc..b30615577 100644
--- a/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean
+++ b/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean
@@ -238,7 +238,7 @@ private theorem smallSides_of_rectangleFree {K : ℕ} (hS : RectangleFree P.acce
 variable {P} in
 /-- Small sides force `K > 1` once some input is accepted: at the first layer both sides of an
 accepted input are nonempty. -/
-private theorem SmallSides.one_lt [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K)
+theorem SmallSides.one_lt [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K)
     (hne : P.accepted.Nonempty) : 1 < K := by
   obtain ⟨x, hx⟩ := hne
   rcases hS 0 (Nat.zero_le _) x hx with h | h
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/Basic.lean b/Complexity/Computability/Circuit/Frontier/Layouts/Basic.lean
index faf192318..7ce26f0d4 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/Basic.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/Basic.lean
@@ -41,7 +41,7 @@ namespace Cslib.Circuits.Frontier
 open Set
 
 /-- `log₂ N` is at most `ε N` plus a constant, for every `ε > 0`. -/
-private theorem exists_natLog_le_mul_add {ε : ℝ} (hε : 0 < ε) :
+theorem exists_natLog_le_mul_add {ε : ℝ} (hε : 0 < ε) :
     ∃ K : ℝ, ∀ N : ℕ, (Nat.log 2 N : ℝ) ≤ ε * N + K := by
   obtain ⟨k, hk⟩ := pow_unbounded_of_one_lt (1 / ε) one_lt_two
   refine ⟨k, fun N => ?_⟩
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/BoundedDegree.lean b/Complexity/Computability/Circuit/Frontier/Layouts/BoundedDegree.lean
index 46878f939..1914e8916 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/BoundedDegree.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/BoundedDegree.lean
@@ -59,7 +59,7 @@ noncomputable def degreeCoefficient (d : ℕ) : ℝ :=
   3 * d / (2 * d - 3) * vertexCoefficient d
 
 /-- The limiting adjacent correlation `2 √(d - 1) / d` is less than one for `d ≥ 3`. -/
-private theorem vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) : vertexCorrelation d < 1 := by
+theorem vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) : vertexCorrelation d < 1 := by
   have hD : (3 : ℝ) ≤ d := by exact_mod_cast hd
   have hs : √((d : ℝ) - 1) ^ 2 = d - 1 := sq_sqrt (by linarith)
   rw [vertexCorrelation, div_lt_one (by linarith)]
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/Gaussian/Basic.lean b/Complexity/Computability/Circuit/Frontier/Layouts/Gaussian/Basic.lean
index 123157414..0c4361653 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/Gaussian/Basic.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/Gaussian/Basic.lean
@@ -171,7 +171,7 @@ section Deviations
 variable {Ω κ : Type*} [Fintype κ]
 
 /-- The number of events that occur is the sum of their indicators. -/
-private theorem ncard_eq_sum_indicator (A : κ → Set Ω) (ω : Ω) :
+theorem ncard_eq_sum_indicator (A : κ → Set Ω) (ω : Ω) :
     ({k | ω ∈ A k}.ncard : ℝ) = ∑ k, (A k).indicator (1 : Ω → ℝ) ω := by
   classical
   simp only [indicator_apply, Pi.one_apply]
@@ -179,7 +179,7 @@ private theorem ncard_eq_sum_indicator (A : κ → Set Ω) (ω : Ω) :
 
 /-- Outside the event that the number of events that occur deviates from `m` by at least `c`,
 this number is below `m + c`. -/
-private theorem ncard_lt_of_not_le_abs {A : κ → Set Ω} {ω : Ω} {m c : ℝ}
+theorem ncard_lt_of_not_le_abs {A : κ → Set Ω} {ω : Ω} {m c : ℝ}
     (h : ¬c ≤ |∑ k, (A k).indicator (1 : Ω → ℝ) ω - m|) : ({k | ω ∈ A k}.ncard : ℝ) < m + c := by
   rw [ncard_eq_sum_indicator]
   linarith [le_abs_self (∑ k, (A k).indicator (1 : Ω → ℝ) ω - m), not_le.mp h]
@@ -248,7 +248,7 @@ variable {V : Type*} [Fintype V]
 
 /-- The product of standard Gaussians on `V → ℝ` carries an event about inner products to the
 same event under the standard Gaussian measure of `EuclideanSpace ℝ V`. -/
-private theorem measureReal_pi_eq {s : Set (EuclideanSpace ℝ V)} (hs : MeasurableSet s) :
+theorem measureReal_pi_eq {s : Set (EuclideanSpace ℝ V)} (hs : MeasurableSet s) :
     (Measure.pi fun _ : V => gaussianReal 0 1).real {ω | WithLp.toLp 2 ω ∈ s} =
       (stdGaussian (EuclideanSpace ℝ V)).real s :=
   (measurePreserving_toLp_pi_gaussianReal V).measureReal_preimage hs.nullMeasurableSet
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/General.lean b/Complexity/Computability/Circuit/Frontier/Layouts/General.lean
index d3a1ce823..cda517c9b 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/General.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/General.lean
@@ -60,7 +60,7 @@ def edgeRestrict (F : Set E) : Multigraph V F where
 variable {G}
 
 /-- Removing edges does not increase degrees. -/
-private theorem MaxDegreeLE.edgeRestrict [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) :
+theorem MaxDegreeLE.edgeRestrict [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) :
     (G.edgeRestrict F).MaxDegreeLE d := by
   intro v
   rw [← ncard_image_of_injective _ Subtype.val_injective]
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/Local.lean b/Complexity/Computability/Circuit/Frontier/Layouts/Local.lean
index 5678b994f..d5a2723e4 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/Local.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/Local.lean
@@ -73,7 +73,7 @@ variable {V E : Type*} (G : Multigraph V E)
 
 /-- **Independent sets count edges once.** If no edge has both endpoints in `I`, the edges of
 a set `X` at the vertices of `I` are the disjoint union of those at each vertex of `I`. -/
-private theorem ncard_inter_touching [Finite E] {I : Finset V}
+theorem ncard_inter_touching [Finite E] {I : Finset V}
     (hI : ∀ e, ¬(G.src e ∈ I ∧ G.tgt e ∈ I))
     (X : Set E) : (X ∩ G.touching I).ncard = ∑ v ∈ I, (X ∩ G.incidenceSet v).ncard := by
   classical
diff --git a/Complexity/Computability/Circuit/Frontier/Layouts/Median.lean b/Complexity/Computability/Circuit/Frontier/Layouts/Median.lean
index fb254b1dc..afc31e435 100644
--- a/Complexity/Computability/Circuit/Frontier/Layouts/Median.lean
+++ b/Complexity/Computability/Circuit/Frontier/Layouts/Median.lean
@@ -111,14 +111,14 @@ namespace IsMedian
 variable {score : E → α} {v : V} {m : α}
 
 /-- Some edge at `v` scores at most a median. -/
-private theorem exists_score_le (h : G.IsMedian score v m) :
+theorem exists_score_le (h : G.IsMedian score v m) :
     ∃ e ∈ G.incidenceSet v, score e ≤ m := by
   obtain ⟨e, he⟩ := nonempty_of_ncard_ne_zero (s := {e ∈ G.incidenceSet v | score e ≤ m})
     (by have := h.1; omega)
   exact ⟨e, he⟩
 
 /-- Some edge at `v` scores at least a median. -/
-private theorem exists_le_score (h : G.IsMedian score v m) :
+theorem exists_le_score (h : G.IsMedian score v m) :
     ∃ e ∈ G.incidenceSet v, m ≤ score e := by
   obtain ⟨e, he⟩ := nonempty_of_ncard_ne_zero (s := {e ∈ G.incidenceSet v | m ≤ score e})
     (by have := h.2; omega)
@@ -240,7 +240,7 @@ private theorem ncard_edgeCut_le_score_le [Finite V] (h3 : ∀ v, (G.incidenceSe
       (((hP _ hu).trans_lt ht).trans_le hle')
 
 /-- The endpoints of a set of edges number at most twice the edges. -/
-private theorem ncard_endpoints_le (F : Set E) :
+theorem ncard_endpoints_le (F : Set E) :
     {w | ∃ e ∈ F, G.src e = w ∨ G.tgt e = w}.ncard ≤ 2 * F.ncard := by
   refine (ncard_le_ncard (t := G.src '' F ∪ G.tgt '' F) ?_).trans
     ((ncard_union_le _ _).trans ?_)
diff --git a/Complexity/Computability/Circuit/Frontier/LowerBound.lean b/Complexity/Computability/Circuit/Frontier/LowerBound.lean
index 2bf274bc8..ac62c2a67 100644
--- a/Complexity/Computability/Circuit/Frontier/LowerBound.lean
+++ b/Complexity/Computability/Circuit/Frontier/LowerBound.lean
@@ -67,7 +67,7 @@ universe u v
 variable {U : Type u} [Finite U] [Nontrivial U]
 
 /-- A set of inputs has at most `|U| ^ n` elements: `log_|U| |S| ≤ n`. -/
-private theorem logb_ncard_le_self {n : ℕ} {S : Set (Fin n → U)} (hS : S.Nonempty) :
+theorem logb_ncard_le_self {n : ℕ} {S : Set (Fin n → U)} (hS : S.Nonempty) :
     Real.logb (Nat.card U) S.ncard ≤ n := by
   have hq : (1 : ℝ) < Nat.card U := by exact_mod_cast Finite.one_lt_card
   have hle : (S.ncard : ℝ) ≤ (Nat.card U : ℝ) ^ n := by
diff --git a/Complexity/Computability/Circuit/Frontier/Multigraph.lean b/Complexity/Computability/Circuit/Frontier/Multigraph.lean
index b7e1db6a9..1a1fb0e90 100644
--- a/Complexity/Computability/Circuit/Frontier/Multigraph.lean
+++ b/Complexity/Computability/Circuit/Frontier/Multigraph.lean
@@ -249,7 +249,7 @@ theorem edgeCut_union_of_edgeCut_eq_empty {K L : Set V} (hK : G.edgeCut K = ∅)
   · simp [mem_edgeCut, hs, mt hKe.2 hs]
 
 /-- The edges touching a closed set `W` are those with both endpoints in `W`. -/
-private theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W = ∅) :
+theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W = ∅) :
     G.touching W = {e | G.src e ∈ W ∧ G.tgt e ∈ W} := by
   ext e
   have := G.edgeCut_eq_empty_iff.1 hW e
@@ -259,7 +259,7 @@ private theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W =
 /-! ### Connected components -/
 
 /-- The endpoints of an edge lie in the same connected component. -/
-private theorem connectedComponentMk_src (e : E) :
+theorem connectedComponentMk_src (e : E) :
     G.toSimpleGraph.connectedComponentMk (G.src e) =
       G.toSimpleGraph.connectedComponentMk (G.tgt e) :=
   SimpleGraph.ConnectedComponent.sound (G.reachable_src_tgt e)
@@ -308,7 +308,7 @@ theorem MaxDegreeLE.induce [Finite E] {d : ℕ} (hG : G.MaxDegreeLE d) (W : Set
     Subtype.val_injective.injOn).trans (hG w)
 
 /-- The simple graph underlying an induced subgraph is the induced simple graph. -/
-private theorem toSimpleGraph_induce (W : Set V) :
+theorem toSimpleGraph_induce (W : Set V) :
     (G.induce W).toSimpleGraph = G.toSimpleGraph.induce W := by
   ext u v
   simp only [toSimpleGraph_adj, SimpleGraph.comap_adj, Function.Embedding.subtype_apply, ne_eq,
diff --git a/Complexity/Computability/Circuit/Frontier/Network.lean b/Complexity/Computability/Circuit/Frontier/Network.lean
index 804a4af91..dcd56318d 100644
--- a/Complexity/Computability/Circuit/Frontier/Network.lean
+++ b/Complexity/Computability/Circuit/Frontier/Network.lean
@@ -431,7 +431,7 @@ theorem unambiguous_branchingProgram
 
 /-- **Edges by width.** At a step that processes a vertex, an edge of the program is determined
 by the values of an assignment on the two frontiers and the inputs read at the vertex. -/
-private theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht : t < Nat.card V) :
+theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht : t < Nat.card V) :
     ((N.branchingProgram π).edges t).ncard ≤
       Nat.card U ^ ((N.frontier π t ∪ N.frontier π (t + 1)).ncard +
         (N.readAt (π.symm ⟨t, ht⟩)).ncard) := by
@@ -457,7 +457,7 @@ private theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht :
 
 /-- At the last step both frontiers are empty, so an edge of the program is determined by the
 unread inputs. -/
-private theorem ncard_edges_last_le [Finite ι] [Finite U] :
+theorem ncard_edges_last_le [Finite ι] [Finite U] :
     ((N.branchingProgram π).edges (Nat.card V)).ncard ≤ Nat.card U ^ N.readᶜ.ncard := by
   have hempty (s : ℕ) (hs : Nat.card V ≤ s) (α : E → U) :
       N.frontierValues π s α = fun _ => none := by
diff --git a/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean b/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean
index d62b6b457..cdd9417e1 100644
--- a/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean
+++ b/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean
@@ -155,7 +155,7 @@ variable [Finite U] [Nontrivial U]
 /-- **The cycle rank of the graph of a nondeterministic circuit** deciding a large
 `K`-rectangle-free set `S ⊆ U^n` is at most `(r - 1) s - n + log_q K + 1` for fan-in at most `r`,
 where `s` counts the inner gates. Only the `n` ordinary inputs are subtracted. -/
-private theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
+theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
     (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K)
     (hbig : Nat.card U * K ^ 2 ≤ S.ncard) :
     ((Compiler.graph c).cycleRank : ℝ) ≤
@@ -183,7 +183,7 @@ private theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
 /-- **Every layout of the graph of a nondeterministic circuit is wide.** For a circuit of fan-in
 at most `r ≥ 2` deciding a large `K`-rectangle-free set `S` nondeterministically, every layout `π`
 of its graph satisfies `log_q |S| ≤ width π + (r + 2) + 3 log_q K + log_q (|V| + 1)`. -/
-private theorem logb_ncard_le_width_of_nondeterministicDecides (hr : 2 ≤ r) (hfan : c.FanInAtMost r)
+theorem logb_ncard_le_width_of_nondeterministicDecides (hr : 2 ≤ r) (hfan : c.FanInAtMost r)
     (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K)
     (hbig : Nat.card U * K ^ 2 ≤ S.ncard) (π : Layout (Compiler.Vertex c)) :
     Real.logb (Nat.card U) S.ncard ≤
@@ -265,7 +265,7 @@ hypothesis for subcubic graphs with coefficient `A > 0`. Under the hypotheses of
 every circuit of fan-in at most two with any number of witness inputs deciding `S_n`
 nondeterministically, over any basis and interpretation on `U`, has more than `(1 + 1/A - ε) n`
 inner gates. -/
-private theorem eventually_lt_innerSize_of_nondeterministicDecides {A : ℝ} (hA : 0 < A)
+theorem eventually_lt_innerSize_of_nondeterministicDecides {A : ℝ} (hA : 0 < A)
     (hlayout : LayoutBound 3 A) (hfree : ∀ᶠ n in atTop, RectangleFree (S n) (K n))
     (hK : (fun n => Real.log (K n)) =o[atTop] fun n => (n : ℝ))
     (hdense : (fun n => n * Real.log (Nat.card U) - Real.log (S n).ncard) =o[atTop]
diff --git a/Complexity/Computability/Circuit/Frontier/Projection.lean b/Complexity/Computability/Circuit/Frontier/Projection.lean
index 01a0bcf72..0fb2a1a96 100644
--- a/Complexity/Computability/Circuit/Frontier/Projection.lean
+++ b/Complexity/Computability/Circuit/Frontier/Projection.lean
@@ -75,11 +75,11 @@ theorem satisfies_reindex_iff {x : ι' → U} {α : E → U} :
 theorem accepted_reindex : (N.reindex e).accepted = {x | x ∘ e ∈ N.accepted} :=
   rfl
 
-private theorem readAt_reindex (v : V) : (N.reindex e).readAt v = e '' N.readAt v := by
+theorem readAt_reindex (v : V) : (N.reindex e).readAt v = e '' N.readAt v := by
   rw [e.image_eq_preimage_symm]
   rfl
 
-private theorem read_reindex : (N.reindex e).read = e '' N.read := by
+theorem read_reindex : (N.reindex e).read = e '' N.read := by
   rw [e.image_eq_preimage_symm]
   rfl
 
diff --git a/Complexity/Computability/Circuit/Frontier/Rectangle.lean b/Complexity/Computability/Circuit/Frontier/Rectangle.lean
index 40a6f9988..1ce87cfda 100644
--- a/Complexity/Computability/Circuit/Frontier/Rectangle.lean
+++ b/Complexity/Computability/Circuit/Frontier/Rectangle.lean
@@ -294,7 +294,7 @@ theorem signedCount_eq_add_sdiff (S : Set (ι → U)) {R D : Set (ι → U)} (h
   ring
 
 /-- The signed count is twice the deviation of `|R ∩ S|` from `|R| / 2`. -/
-private theorem signedCount_eq_two_mul (S R : Set (ι → U)) :
+theorem signedCount_eq_two_mul (S R : Set (ι → U)) :
     signedCount S R = 2 * (((R ∩ S).ncard : ℝ) - R.ncard / 2) := by
   have : ((R ∩ S).ncard : ℝ) + (R \ S).ncard = R.ncard := by
     exact_mod_cast ncard_inter_add_ncard_sdiff_eq_ncard R S
diff --git a/Complexity/Computability/Circuit/Fusion/Basic.lean b/Complexity/Computability/Circuit/Fusion/Basic.lean
index bb02ceaeb..732578fd0 100644
--- a/Complexity/Computability/Circuit/Fusion/Basic.lean
+++ b/Complexity/Computability/Circuit/Fusion/Basic.lean
@@ -145,7 +145,7 @@ def Cover.ofProgram (p : Program σ n g) (I : Interpretation σ U) (P : W → U
   (p.cost_eq_sum weight).symm
 
 /-- Every program violating all candidate invariants pays at least the minimum cover cost. -/
-private theorem coverComplexity_le_program_cost (p : Program σ n g) (I : Interpretation σ U)
+theorem coverComplexity_le_program_cost (p : Program σ n g) (I : Interpretation σ U)
     (P : W → U → Prop) (input : Fin n → U) (hin : ∀ t i, P t (input i))
     (hfail : ∀ t, ∃ w, ¬ P t (p.trace I input w)) (weight : σ.Op → ℕ) :
     coverComplexity I P weight ≤ p.cost weight := by
diff --git a/Complexity/Computability/Circuit/Fusion/Converse.lean b/Complexity/Computability/Circuit/Fusion/Converse.lean
index 34ac03c0a..b49236cc8 100644
--- a/Complexity/Computability/Circuit/Fusion/Converse.lean
+++ b/Complexity/Computability/Circuit/Fusion/Converse.lean
@@ -106,7 +106,7 @@ theorem PairCover.exists_forallGuess {n : ℕ} (f : BooleanFunction n)
     exact Formula.eval_toCircuit _ _ _ _
 
 /-- The semi-ultrafilter bound applies after minimizing over all auxiliary counts and verifiers. -/
-private theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ}
+theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ}
     (f : BooleanFunction n) :
     pairCoverComplexity {x | f x = true} (fun i => {x | AltFormula.literals x i = true})
       Semifilter.IsUltra ≤ econondeterministicAndComplexity f := by
@@ -116,7 +116,7 @@ private theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ
   exact pairCoverComplexity_forallGuess_le_cost g c hc
 
 /-- A semi-ultrafilter cover gives a universal verifier at most five times as costly. -/
-private theorem econondeterministicAndComplexity_le_pairCoverComplexity {n : ℕ}
+theorem econondeterministicAndComplexity_le_pairCoverComplexity {n : ℕ}
     (f : BooleanFunction n) :
     econondeterministicAndComplexity f ≤
       5 * pairCoverComplexity {x | f x = true}
diff --git a/Complexity/Computability/Circuit/Fusion/Cyclic.lean b/Complexity/Computability/Circuit/Fusion/Cyclic.lean
index d8d901340..c5d974198 100644
--- a/Complexity/Computability/Circuit/Fusion/Cyclic.lean
+++ b/Complexity/Computability/Circuit/Fusion/Cyclic.lean
@@ -117,7 +117,7 @@ theorem pairCover_lowerBound_cyclic {target : Set U} {input : Fin n → Set U}
     hbound (PairCover.ofCyclicCircuit c input o hc admissible)
 
 /-- The minimum pair-cover length bounds the AND cost of any cyclic construction. -/
-private theorem pairCoverComplexity_le_cyclic_cost {target : Set U}
+theorem pairCoverComplexity_le_cyclic_cost {target : Set U}
     (c : CyclicCircuit Monotone.signature n m) (input : Fin n → Set U) (o : Fin m)
     (hc : c.eval (Monotone.setInterpretation U) Monotone.setInterpretation_mono input o = target)
     (admissible : Semifilter ↥(targetᶜ) → Prop := fun _ => True) :
diff --git a/Complexity/Computability/Circuit/Fusion/DeMorgan.lean b/Complexity/Computability/Circuit/Fusion/DeMorgan.lean
index 37cabf596..9152aa5d1 100644
--- a/Complexity/Computability/Circuit/Fusion/DeMorgan.lean
+++ b/Complexity/Computability/Circuit/Fusion/DeMorgan.lean
@@ -137,7 +137,7 @@ variable {n : ℕ}
 
 open Boolean in
 /-- An unrestricted cover compiles to a monotone circuit computing `f` from its literals. -/
-private theorem PairCover.computesFrom_toCircuit {f : BooleanFunction n}
+theorem PairCover.computesFrom_toCircuit {f : BooleanFunction n}
     (c : PairCover {x | f x = true} (fun i => {x | AltFormula.literals x i = true})) :
     c.toCircuit.ComputesFrom Monotone.interpretation (fun x (_ : Fin 1) => f x)
       AltFormula.literals :=
diff --git a/Complexity/Computability/Circuit/Fusion/Graph/Inequality.lean b/Complexity/Computability/Circuit/Fusion/Graph/Inequality.lean
index d4493182b..24f8d82ab 100644
--- a/Complexity/Computability/Circuit/Fusion/Graph/Inequality.lean
+++ b/Complexity/Computability/Circuit/Fusion/Graph/Inequality.lean
@@ -120,7 +120,7 @@ theorem inequality_signature_injective
   tauto
 
 /-- A canonical cover needs enough bit signatures to label all vertices. -/
-private theorem card_le_two_pow_length_inequality
+theorem card_le_two_pow_length_inequality
     (c : PairCover (inequality V) sources (canonicalClass (inequality V))) :
     Fintype.card V ≤ 2 ^ c.pairs.length := by
   simpa using Fintype.card_le_of_injective _ (inequality_signature_injective c)
diff --git a/Complexity/Computability/Circuit/Fusion/Quadratic.lean b/Complexity/Computability/Circuit/Fusion/Quadratic.lean
index 975914787..c2a56640c 100644
--- a/Complexity/Computability/Circuit/Fusion/Quadratic.lean
+++ b/Complexity/Computability/Circuit/Fusion/Quadratic.lean
@@ -335,7 +335,7 @@ theorem PairCover.size_toCircuit_le (c : PairCover target input) :
   nlinarith
 
 /-- Every unrestricted pair cover yields a quadratic upper bound for native AND complexity. -/
-private theorem PairCover.ecomplexityFrom_le_sq (c : PairCover target input) :
+theorem PairCover.ecomplexityFrom_le_sq (c : PairCover target input) :
     ecomplexityFrom (Monotone.setInterpretation U) Monotone.andCost
       (fun _ : Unit => fun _ : Fin 1 => target) (fun _ => input) ≤
         (c.pairs.length : ℕ∞) ^ 2 := by
diff --git a/Complexity/Computability/Circuit/Iteration.lean b/Complexity/Computability/Circuit/Iteration.lean
index c32088a54..ffb915542 100644
--- a/Complexity/Computability/Circuit/Iteration.lean
+++ b/Complexity/Computability/Circuit/Iteration.lean
@@ -113,7 +113,7 @@ def stages (q : ℕ → Set ((Fin n → U) → U)) (t : ℕ) : Set ((Fin n → U
 @[simp] theorem stages_zero (q : ℕ → Set ((Fin n → U) → U)) : stages q 0 = q 0 := by
   simp [stages]
 
-private theorem stages_succ (q : ℕ → Set ((Fin n → U) → U)) (t : ℕ) :
+theorem stages_succ (q : ℕ → Set ((Fin n → U) → U)) (t : ℕ) :
     stages q (t + 1) = stages q t ∪ q (t + 1) := by
   simp [stages, Finset.range_add_one, Set.union_comm]
 
diff --git a/Complexity/Computability/Circuit/Linearize.lean b/Complexity/Computability/Circuit/Linearize.lean
index d03e327a4..a17d58bd8 100644
--- a/Complexity/Computability/Circuit/Linearize.lean
+++ b/Complexity/Computability/Circuit/Linearize.lean
@@ -109,7 +109,7 @@ theorem polynomialInterpretation_apply (R : Type*) [CommRing R] [Algebra F R] (o
 
 /-- Evaluation of a program with polynomial operations commutes with algebra
 homomorphisms. -/
-private theorem Program.map_trace_polynomialInterpretation {R S : Type*} [CommRing R] [Algebra F R]
+theorem Program.map_trace_polynomialInterpretation {R S : Type*} [CommRing R] [Algebra F R]
     [CommRing S] [Algebra F S] (φ : R →ₐ[F] S) (p : Program σ n s) (x : Fin n → R)
     (w : Wire n s) :
     φ (p.trace (polynomialInterpretation P R) x w) =
@@ -131,7 +131,7 @@ noncomputable def taylorOp (P : MvPolynomial (Fin k) F) (z : Fin k → F) :
   ⟨k, fun a => eval z (pderiv a P), eval z P - ∑ a, eval z (pderiv a P) * z a⟩
 
 /-- The value of the first-order Taylor expansion of `P` at `z`. -/
-private theorem affineInterpretation_taylorOp (P : MvPolynomial (Fin k) F) (z y : Fin k → F) :
+theorem affineInterpretation_taylorOp (P : MvPolynomial (Fin k) F) (z y : Fin k → F) :
     affineInterpretation F (taylorOp P z) y =
       eval z P + ∑ a, eval z (pderiv a P) * (y a - z a) := by
   simp only [taylorOp, affineInterpretation_apply, mul_sub, Finset.sum_sub_distrib]
@@ -149,7 +149,7 @@ noncomputable def Program.linearize : ∀ {s : ℕ}, Program σ n s → Program
         line.wires⟩
 
 /-- Linearization preserves the arity of every gate. -/
-private theorem Program.arity_lines_linearize (p : Program σ n s) (g : Fin s) :
+theorem Program.arity_lines_linearize (p : Program σ n s) (g : Fin s) :
     (affineSignature F).Arity ((p.linearize P).lines g).op = σ.Arity (p.lines g).op := by
   induction p with
   | empty => exact g.elim0
@@ -161,12 +161,12 @@ private theorem Program.arity_lines_linearize (p : Program σ n s) (g : Fin s) :
       exact ih g
 
 /-- Linearization preserves the inner gates. -/
-private theorem Program.innerGates_linearize (p : Program σ n s) :
+theorem Program.innerGates_linearize (p : Program σ n s) :
     (p.linearize P).innerGates = p.innerGates :=
   Finset.filter_congr fun g _ => by rw [arity_lines_linearize]
 
 /-- Linearization preserves fan-in. -/
-private theorem Program.fanInAtMost_linearize (p : Program σ n s) (r : ℕ) :
+theorem Program.fanInAtMost_linearize (p : Program σ n s) (r : ℕ) :
     (p.linearize P).FanInAtMost r ↔ p.FanInAtMost r := by
   simp only [Program.fanInAtMost_iff]
   exact forall_congr' fun g => iff_of_eq (congrArg (· ≤ r) (p.arity_lines_linearize P g))
diff --git a/Complexity/Computability/Circuit/Monotone/Clique/Essential.lean b/Complexity/Computability/Circuit/Monotone/Clique/Essential.lean
index 09fcfa496..0b8deac00 100644
--- a/Complexity/Computability/Circuit/Monotone/Clique/Essential.lean
+++ b/Complexity/Computability/Circuit/Monotone/Clique/Essential.lean
@@ -43,7 +43,7 @@ open Cslib.Circuits.Clique Finset
 variable {n k : ℕ}
 
 /-- Monotone programs have fan-in at most two. -/
-private theorem program_fanInAtMost_two {g : ℕ} (p : Program signature n g) : p.FanInAtMost 2 := by
+theorem program_fanInAtMost_two {g : ℕ} (p : Program signature n g) : p.FanInAtMost 2 := by
   induction p with
   | empty => trivial
   | gate p line ih => exact ⟨ih, by cases line.op <;> simp⟩
diff --git a/Complexity/Computability/Circuit/Monotone/DualRail.lean b/Complexity/Computability/Circuit/Monotone/DualRail.lean
index 6014027a7..08557750a 100644
--- a/Complexity/Computability/Circuit/Monotone/DualRail.lean
+++ b/Complexity/Computability/Circuit/Monotone/DualRail.lean
@@ -73,7 +73,7 @@ def railBits (x : List Bool) : List Bool := true :: x.flatMap fun b => [b, !b]
     simp only [List.length_append, List.length_cons, List.length_nil]
     omega
 
-private theorem railBits_append (x : List Bool) (v : Bool) :
+theorem railBits_append (x : List Bool) (v : Bool) :
     railBits (x ++ [v]) = railBits x ++ [v, !v] := by
   simp [railBits]
 
@@ -140,7 +140,7 @@ def dualCode (gates : List (Boolean.Op × List ℕ)) : List (Op × List ℕ) :=
   | cons g gates ih => simp only [dualCode, List.flatMap_cons, List.length_append,
       length_dualGates, List.length_cons] at ih ⊢; omega
 
-private theorem dualCode_append (gates gates' : List (Boolean.Op × List ℕ)) :
+theorem dualCode_append (gates gates' : List (Boolean.Op × List ℕ)) :
     dualCode (gates ++ gates') = dualCode gates ++ dualCode gates' :=
   List.flatMap_append
 
diff --git a/Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean b/Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean
index 63eec8549..1c5aa55fb 100644
--- a/Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean
+++ b/Complexity/Computability/Circuit/Monotone/KarchmerWigderson.lean
@@ -85,7 +85,7 @@ def monotoneKWProtocol : Formula Monotone.signature n → KWProtocol (Fin n)
 
 /-- The protocol of a monotone formula finds a bit that is one in Alice's input and zero in Bob's,
 when the formula is true on Alice's input and false on Bob's. -/
-private theorem exceedsAt_run_monotoneKWProtocol (F : Formula Monotone.signature n)
+theorem exceedsAt_run_monotoneKWProtocol (F : Formula Monotone.signature n)
     {x y : BitString n}
     (hx : F.eval interpretation x = true) (hy : F.eval interpretation y = false) :
     ExceedsAt x y (F.monotoneKWProtocol.run x y) := by
diff --git a/Complexity/Computability/Circuit/SimulationContext.lean b/Complexity/Computability/Circuit/SimulationContext.lean
index 72f70d56b..19cb556a3 100644
--- a/Complexity/Computability/Circuit/SimulationContext.lean
+++ b/Complexity/Computability/Circuit/SimulationContext.lean
@@ -63,7 +63,7 @@ def Circuit.withContext (c : Circuit σ n m) (q : ℕ) : Circuit (σ.withContext
   (c.comp (wiring σ (Fin.natAdd q))).mapLines (Line.withContext q)
 
 /-- Adding context does not add gates or change their costs. -/
-private theorem Circuit.cost_program_withContext (c : Circuit σ n m) (q : ℕ) (cost : σ.Op → ℕ) :
+theorem Circuit.cost_program_withContext (c : Circuit σ n m) (q : ℕ) (cost : σ.Op → ℕ) :
     (c.withContext q).program.cost cost = c.program.cost cost := by
   change ((c.comp (wiring σ (Fin.natAdd q))).program.mapLines
     (Line.withContext q)).cost cost = _