refactor(Logics,Algorithms,WordRAM): make 42 API and general declarations public again (#926)

Complexity/Algorithms/Lean/FusionTree/Tree.lean

@@ -359,15 +359,15 @@ theorem listPredecessor_eq_none_iff (q : ℕ) (xs : List ℕ) :
         contradiction
       simp [listPredecessor, hs, Option.or, ht]
 
-private theorem listPredecessor_append (q : ℕ) (xs ys : List ℕ) :
+theorem listPredecessor_append (q : ℕ) (xs ys : List ℕ) :
     listPredecessor q (xs ++ ys) = (listPredecessor q ys).or (listPredecessor q xs) := by
   induction xs with
   | nil => simp [listPredecessor]
   | cons x xs ih =>
     simp only [List.cons_append, listPredecessor, ih]
     cases listPredecessor q ys <;> cases listPredecessor q xs <;> rfl
 
-private theorem listPredecessor_ne_none_iff {q : ℕ} {xs : List ℕ}
+theorem listPredecessor_ne_none_iff {q : ℕ} {xs : List ℕ}
     (hn : xs ≠ []) (hs : xs.Pairwise (· ≤ ·)) :
     listPredecessor q xs ≠ none ↔ xs.headD 0 ≤ q := by
   obtain ⟨x, xs, rfl⟩ := List.exists_cons_of_ne_nil hn
@@ -456,7 +456,7 @@ decreasing_by
   simp_wf
   omega
 
-private theorem listPredecessor_some_spec {q p : ℕ} {xs : List ℕ}
+theorem listPredecessor_some_spec {q p : ℕ} {xs : List ℕ}
     (hs : xs.Pairwise (· ≤ ·)) (hp : listPredecessor q xs = some p) :
     p ∈ xs ∧ p ≤ q ∧ ∀ x ∈ xs, x ≤ q → x ≤ p := by
   revert hs hp

Complexity/Algorithms/Lean/Sort/Bitonic/Correctness.lean

@@ -34,7 +34,7 @@ namespace Cslib.BitonicSort
 variable {α κ : Type*}
 
 /-- Every minimum half-entry lies below every maximum half-entry of a bitonic tuple. -/
-private theorem IsBitonic.min_le_max_halves [LinearOrder κ] {n : ℕ} (first second : Fin n → κ)
+theorem IsBitonic.min_le_max_halves [LinearOrder κ] {n : ℕ} (first second : Fin n → κ)
     (h : IsBitonic (Fin.append first second)) (i j : Fin n) :
     min (first i) (second i) ≤ max (first j) (second j) := by
   rcases lt_trichotomy i j with hij | hij | hij
@@ -58,7 +58,7 @@ private theorem append_right_value {n m : ℕ} (first : Fin n → κ) (second :
   exact (congrArg (Fin.append first second) heq).trans (Fin.append_right _ _ _)
 
 /-- An increasing tuple followed by a decreasing tuple is bitonic. -/
-private theorem isBitonic_append [LinearOrder κ] {n m : ℕ} {first : Fin n → κ}
+theorem isBitonic_append [LinearOrder κ] {n m : ℕ} {first : Fin n → κ}
     {second : Fin m → κ} (hfirst : Monotone first) (hsecond : Antitone second) :
     IsBitonic (Fin.append first second) := by
   have hpeak (i j k : Fin (n + m)) (hij : i < j) (hjk : j < k) :
@@ -187,7 +187,7 @@ theorem merge_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending
       exact hpairs.min_le_max_halves left right i j
 
 /-- Batcher sorting orders the keys in either direction on every input. -/
-private theorem sort_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool)
+theorem sort_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool)
     (input : Fin (arity depth) → α) :
     if ascending then Monotone (key ∘ sort key depth ascending input)
     else Antitone (key ∘ sort key depth ascending input) := by

Complexity/Algorithms/Reachability/BreadthFirst.lean

@@ -161,7 +161,7 @@ theorem prefix_search {i j : ℕ} (hij : i ≤ j) (start : α) :
     rw [← Nat.add_assoc, search_succ]
     exact prefix_expand _
 
-private theorem start_mem_search (rounds : ℕ) (start : α) : start ∈ search succ rounds start :=
+theorem start_mem_search (rounds : ℕ) (start : α) : start ∈ search succ rounds start :=
   (prefix_search (Nat.zero_le rounds) start).subset (by simp)
 
 /-- **The found elements are distinct.** -/

Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean

@@ -53,7 +53,7 @@ open scoped Classical in
 noncomputable def roundSet (N : ℕ) (edge : ℕ → ℕ → Bool) (source k : ℕ) : Finset ℕ :=
   (Finset.range N).filter (· ∈ Relation.reachableWithin (Graph N edge) source k)
 
-private theorem reachable_lt (hsource : source < N)
+theorem reachable_lt (hsource : source < N)
     (h : Relation.ReflTransGen (Graph N edge) source u) : u < N := by
   induction h with
   | refl => exact hsource
@@ -72,7 +72,7 @@ theorem mem_roundSet (hsource : source < N) :
   exact (Finset.mem_filter).trans ⟨And.right, fun h => ⟨Finset.mem_range.mpr
     (within_lt hsource h), h⟩⟩
 
-private theorem roundSet_zero (hsource : source < N) : roundSet N edge source 0 = {source} := by
+theorem roundSet_zero (hsource : source < N) : roundSet N edge source 0 = {source} := by
   ext u
   rw [mem_roundSet hsource, ← Relation.mem_reachableWithin, Relation.reachableWithin_zero]
   simp
@@ -82,7 +82,7 @@ theorem roundSet_card_le : (roundSet N edge source k).card ≤ N := by
   classical
   exact (Finset.card_le_card (Finset.filter_subset _ _)).trans_eq (Finset.card_range N)
 
-private theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) :
+theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) :
     v ∈ roundSet N edge source (k + 1) ↔
       ∃ u ∈ roundSet N edge source k, u = v ∨ edge u v = true := by
   rw [mem_roundSet hsource, ← Relation.mem_reachableWithin, Relation.mem_reachableWithin_succ]
@@ -100,7 +100,7 @@ private theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) :
     · exact .single ⟨within_lt hsource hu', hv, huv⟩
 
 /-- Round `N - 1` is already the entire reachable set. -/
-private theorem mem_roundSet_final (hsource : source < N) (hk : k + 1 = N) :
+theorem mem_roundSet_final (hsource : source < N) (hk : k + 1 = N) :
     u ∈ roundSet N edge source k ↔ Relation.ReflTransGen (Graph N edge) source u := by
   have hs : {u | Relation.ReflTransGen (Graph N edge) source u} ⊆
       (Finset.range N : Set ℕ) := fun u hu => Finset.mem_range.mpr (reachable_lt hsource hu)

Complexity/Algorithms/WordRAM/FusionTree/Preprocessing.lean

@@ -48,7 +48,7 @@ open Cslib.WordRAM
 open Cslib.Algorithms.Lean.FusionTree
 
 /-- A nonempty valid tree's cached minimum is one of its actual leaf keys. -/
-private theorem minimum_mem {B : ℕ} {t : Tree} (ht : Tree.Valid B t)
+theorem minimum_mem {B : ℕ} {t : Tree} (ht : Tree.Valid B t)
     (hne : t.keys ≠ []) : t.minimum ∈ t.keys := by
   rw [Tree.minimum_eq_headD ht]
   obtain ⟨x, xs, hx⟩ := List.exists_cons_of_ne_nil hne

Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean

@@ -352,7 +352,7 @@ theorem successor_executes_log {d w base stackBase₀ query : ℕ} {tree : Tree
 
 /-- `Tree.successor` on a valid tree computes the mathematical `OrderedSet.least` of the stored
 elements strictly greater than the query. -/
-private theorem successor_eq_least {d : ℕ} {t : Tree d} (ht : t.Valid) (q : ℕ) :
+theorem successor_eq_least {d : ℕ} {t : Tree d} (ht : t.Valid) (q : ℕ) :
     t.successor q = OrderedSet.least (t.elements.filter (q < ·)) := by
   apply OrderedSet.LeastResult.eq_least
   cases hs : t.successor q with

Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean

@@ -174,7 +174,7 @@ private theorem memberNext_constants {base query : ℕ} {s : Data 32}
   split_ifs <;> simp +decide [hz, ho, ht, hthree, hfour, hfive]
 
 /-- A query above the cached maximum is absent; this fact uses validity, not outside memory. -/
-private theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d}
+theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d}
     (ht : tree.Valid) (hb : tree.bounds = some (m, M)) (hx : M < query) :
     tree.member query = false := by
   have hnot : ¬tree.Contains query := by
@@ -188,7 +188,7 @@ private theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d}
   · exact False.elim (hnot ((Tree.member_iff_contains ht query).mp he))
 
 /-- The cached maximum is a valid early successful membership result. -/
-private theorem member_maximum {d m M : ℕ} {tree : Tree d}
+theorem member_maximum {d m M : ℕ} {tree : Tree d}
     (ht : tree.Valid) (hb : tree.bounds = some (m, M)) : tree.member M = true :=
   (Tree.member_iff_contains ht M).mpr (ht.contains_maximum hb)
 

Complexity/Computability/WordRAM/Allocation.lean

@@ -127,7 +127,7 @@ theorem clear_zero (m : ℕ → ℕ) (base : ℕ) : clear m base 0 = m := by
   funext a
   simp [clear]
 
-private theorem clear_succ (m : ℕ → ℕ) (base k : ℕ) :
+theorem clear_succ (m : ℕ → ℕ) (base k : ℕ) :
     clear m base (k + 1) = Function.update (clear m base k) (base + k) 0 := by
   funext a
   simp only [clear, Function.update_apply]

Complexity/Computability/WordRAM/Copy.lean

@@ -59,7 +59,7 @@ theorem copyPrefix_outside {mem : ℕ → ℕ} {src dst k a : ℕ}
     (ha : ¬(dst ≤ a ∧ a < dst + k)) : copyPrefix mem src dst k a = mem a := by
   simp [copyPrefix, ha]
 
-private theorem copyPrefix_succ (mem : ℕ → ℕ) (src dst k : ℕ) :
+theorem copyPrefix_succ (mem : ℕ → ℕ) (src dst k : ℕ) :
     copyPrefix mem src dst (k + 1) =
       Function.update (copyPrefix mem src dst k) (dst + k) (mem (src + k)) := by
   funext a

Complexity/Computability/WordRAM/Defs.lean

@@ -768,7 +768,7 @@ theorem Next.mono_width {w w' : ℕ} {p : Program B r} {s t : State r} (hp : ¬p
     | branch c t => rw [step_branch hpc] at h ⊢; exact h
     | halt i => simp [step_halt hpc] at h
 
-private theorem step_halt_mono_width {w w' : ℕ} {p : Program B r} {s : State r} {v : ℕ}
+theorem step_halt_mono_width {w w' : ℕ} {p : Program B r} {s : State r} {v : ℕ}
     (h : step w p s = .halt v) : step w' p s = .halt v := by
   cases hpc : p[s.pc]? with
   | none => simp [WordRAM.step, hpc] at h

Complexity/Computability/WordRAM/MapOp.lean

@@ -144,11 +144,11 @@ theorem step_mapOp (w : ℕ) (p : Program B r) (s : State r) :
     | op o => simp only [Option.map_some, Instr.mapOp, Op.eval_mapOp]
     | _ => rfl
 
-private theorem next_mapOp (w : ℕ) (p : Program B r) : Next w (p.mapOp φ) = Next w p := by
+theorem next_mapOp (w : ℕ) (p : Program B r) : Next w (p.mapOp φ) = Next w p := by
   funext s t
   simp only [Next, step_mapOp]
 
-private theorem runs_mapOp (w : ℕ) (p : Program B r) : Runs w (p.mapOp φ) = Runs w p := by
+theorem runs_mapOp (w : ℕ) (p : Program B r) : Runs w (p.mapOp φ) = Runs w p := by
   rw [Runs, Runs, next_mapOp]
 
 /-- **Translation preserves halting runs.** The translated program halts with the same output

Complexity/Computability/WordRAM/Multiword/CircuitRun.lean

@@ -58,7 +58,7 @@ private theorem update_prefix (v : Fin n → ℕ) (d : Fin n) :
 namespace Operation
 
 /-- Evaluation depends only on the earlier source values of a node. -/
-private theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ}
+theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ}
     (he : op.Earlier d) (h : ∀ j, j.val < d.val → v j = u j) :
     op.eval v = op.eval u := by
   cases op with
@@ -68,7 +68,7 @@ private theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ}
     simp only [eval, h a he.1, h b he.2]
 
 /-- The admissibility bounds depend only on the earlier source values of a node. -/
-private theorem admissible_congr {w : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ}
+theorem admissible_congr {w : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ}
     (he : op.Earlier d) (h : ∀ j, j.val < d.val → v j = u j) :
     op.Admissible w v ↔ op.Admissible w u := by
   cases op with

Complexity/Computability/WordRAM/Structured.lean

@@ -614,13 +614,13 @@ theorem Data.comap_regs (x : Data r') (i : Fin r) : (x.comap f).regs i = x.regs
 @[simp]
 theorem Data.comap_mem (x : Data r') : (x.comap f).mem = x.mem := rfl
 
-private theorem Data.comap_extend (hf : f.Injective) (y : Data r) (x : Data r') :
+theorem Data.comap_extend (hf : f.Injective) (y : Data r) (x : Data r') :
     (y.extend f x).comap f = y := by
   ext i
   · exact hf.extend_apply _ _ i
   · rfl
 
-private theorem Data.extend_extend (hf : f.Injective) (y z : Data r) (x : Data r') :
+theorem Data.extend_extend (hf : f.Injective) (y z : Data r) (x : Data r') :
     z.extend f (y.extend f x) = z.extend f x := by
   ext j
   · simp only [Data.extend]

Complexity/Computability/WordRAM/Trace.lean

@@ -162,7 +162,7 @@ theorem writes_append (ts us : List Probe) : writes (ts ++ us) = writes ts ∪ w
 end Probe
 
 /-- A successful primitive instruction preserves every cell absent from its write transcript. -/
-private theorem Op.eval_modifies {w : ℕ} {o : Op B r} {x y : Data r} (h : o.eval w x = some y) :
+theorem Op.eval_modifies {w : ℕ} {o : Op B r} {x y : Data r} (h : o.eval w x = some y) :
     Modifies (Probe.writes (o.probes x)) x.mem y.mem := by
   cases o with
   | const =>

Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean

@@ -115,7 +115,7 @@ theorem IsCarrySuccessor.lexRank_succ {n k : ℕ} {x y : Fin k → Fin n}
   lia
 
 /-- Consecutive ranks have precisely one increment coordinate and a carried suffix. -/
-private theorem isCarrySuccessor_of_lexRank_succ {n k : ℕ} {x y : Fin k → Fin n}
+theorem isCarrySuccessor_of_lexRank_succ {n k : ℕ} {x y : Fin k → Fin n}
     (h : lexRank y = lexRank x + 1) : IsCarrySuccessor x y := by
   obtain ⟨hxy, hgap⟩ := (lexRank_succ_iff x y).mp h
   obtain ⟨i, hi, hpre⟩ := (lexRank_lt_iff x y).mp hxy

Complexity/Logics/FirstOrder/Problems/CNF.lean

@@ -270,7 +270,7 @@ private theorem literals_copies (j : J) (c : M) :
 
 /-- A positive number of disjoint copies of a CNF structure is satisfiable exactly when the
 structure is. -/
-private theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) ↔ Satisfiable M := by
+theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) ↔ Satisfiable M := by
   constructor
   · rintro ⟨A, hA⟩
     obtain ⟨j₀⟩ := ‹Nonempty J›
@@ -288,7 +288,7 @@ private theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) 
 
 /-- A positive number of disjoint copies of a CNF structure is a 3-CNF structure exactly when the
 structure is. -/
-private theorem isThreeCNF_copies_iff [Nonempty J] : IsThreeCNF (Copies J M) ↔ IsThreeCNF M := by
+theorem isThreeCNF_copies_iff [Nonempty J] : IsThreeCNF (Copies J M) ↔ IsThreeCNF M := by
   have hinj (j : J) : Function.Injective fun l : Bool × M => (l.1, (⟨j, l.2⟩ : Copies J M)) := by
     intro l l' h
     simp only [Prod.mk.injEq, Copies.mk.injEq, true_and] at h

Complexity/Logics/FirstOrder/Problems/Coloring.lean

@@ -94,7 +94,7 @@ theorem colorable_copies_iff [Nonempty J] : Colorable n (Copies J M) ↔ Colorab
     exact ⟨fun x => f x.val, fun x y h => hf _ _ ((Copies.relMap_copies_two adj _ _).1 h).2⟩
 
 /-- A positive number of disjoint copies of a graph is a simple graph exactly when the graph is. -/
-private theorem simpleGraph_copies_iff [Nonempty J] :
+theorem simpleGraph_copies_iff [Nonempty J] :
     Copies J M ⊨ Theory.simpleGraph ↔ M ⊨ Theory.simpleGraph := by
   simp only [Theory.simpleGraph_model_iff, Copies.relMap_copies_two]
   constructor

Complexity/Logics/FirstOrder/Problems/IndependentSetReduction.lean

@@ -90,7 +90,7 @@ theorem mem_IndependentSet_of_subsingleton [Subsingleton M] :
 
 /-- **Independent set is invariant under copies**: the largest independent sets of `J` disjoint
 copies of a graph are unions of largest independent sets of the copies. -/
-private theorem independentSet_copies_iff [Finite J] [Finite M] [Nonempty J] :
+theorem independentSet_copies_iff [Finite J] [Finite M] [Nonempty J] :
     (Bundled.of (Copies J M) : Bundled.{w} sizedGraph.Structure) ∈ IndependentSet ↔
       (Bundled.of M : Bundled.{w} sizedGraph.Structure) ∈ IndependentSet := by
   have hsize : {x : Copies J M | RelMap sizedGraph.size ![x]}.ncard =

Complexity/Logics/Propositional/CNF/ThreeCNF.lean

@@ -211,7 +211,7 @@ private theorem Clause.length_splitAux (fresh : ℕ → W) (j : ℕ) (carry : Li
     · exact hrest
 
 /-- Splitting a clause of width `w` gives `w - 2` clauses, and at least one. -/
-private theorem Clause.length_split3 (fresh : ℕ → W) (j : ℕ) (c : Clause W) :
+theorem Clause.length_split3 (fresh : ℕ → W) (j : ℕ) (c : Clause W) :
     (Clause.split3 fresh j c).length = max 1 (c.length - 2) := by
   cases c with
   | nil => rfl

Complexity/Logics/Propositional/CNF/UnsatVal.lean

@@ -290,7 +290,7 @@ theorem Clause.IsExactThreeDistinct.card_eval_eq_true {c : Clause (Fin 3)}
 
 /-- The expected number of falsified clauses in an exact 3-CNF formula with distinct variables per
 clause under a uniform random assignment is `φ.length / 8`. -/
-private theorem CNF.IsExactThreeDistinct.expect_countUnsat {φ : CNF ι}
+theorem CNF.IsExactThreeDistinct.expect_countUnsat {φ : CNF ι}
     (hφ : φ.IsExactThreeDistinct) :
     (𝔼 σ : ι → Bool, (φ.countUnsat σ : ℝ)) = (φ.length : ℝ) / 8 := by
   induction φ with
@@ -311,7 +311,7 @@ end FintypeCube
 
 /-- Relabelling a clause along a map that is injective on its variables preserves
 `Clause.IsExactThreeDistinct`. -/
-private theorem Clause.IsExactThreeDistinct.relabel_of_injOn {f : V → ι} {c : Clause V}
+theorem Clause.IsExactThreeDistinct.relabel_of_injOn {f : V → ι} {c : Clause V}
     (hf : ∀ x ∈ c.map Prod.fst, ∀ y ∈ c.map Prod.fst, f x = f y → x = y)
     (hc : c.IsExactThreeDistinct) : (c.relabel f).IsExactThreeDistinct := by
   refine ⟨by rw [Clause.length_relabel, hc.1], ?_⟩

Complexity/Logics/Propositional/ClauseSet/Sparsification.lean

@@ -56,7 +56,7 @@ namespace Cslib.Logic.PL
 open Finset Filter
 
 /-- A polynomial is eventually below an exponential with base `r > 1`. -/
-private theorem exists_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) :
+theorem exists_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) :
     ∃ α : ℕ, 1 ≤ α ∧ C * (α : ℝ) ^ d ≤ r ^ α := by
   have hlim := tendsto_pow_const_div_const_pow_of_one_lt d hr
   have hC : 0 < |C| + 1 := by positivity

Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean

@@ -151,16 +151,16 @@ theorem mem_toClauseSet {ψ : CNF V} {C : Finset (Literal V)} :
     C ∈ ψ.toClauseSet ↔ ∃ D ∈ ψ, D.toFinset = C := by
   simp [CNF.toClauseSet]
 
-private theorem toClauseSet_append (ψ χ : CNF V) :
+theorem toClauseSet_append (ψ χ : CNF V) :
     (ψ ++ χ).toClauseSet = ψ.toClauseSet ∪ χ.toClauseSet := by
   simp [CNF.toClauseSet, List.toFinset_append]
 
-private theorem toClauseSet_mono {ψ χ : CNF V} (h : ψ ⊆ χ) : ψ.toClauseSet ⊆ χ.toClauseSet := by
+theorem toClauseSet_mono {ψ χ : CNF V} (h : ψ ⊆ χ) : ψ.toClauseSet ⊆ χ.toClauseSet := by
   intro C hC
   obtain ⟨D, hD, rfl⟩ := mem_toClauseSet.mp hC
   exact mem_toClauseSet.mpr ⟨D, h hD, rfl⟩
 
-private theorem subclause_eq_true_iff {D C : Clause V} :
+theorem subclause_eq_true_iff {D C : Clause V} :
     subclause D C = true ↔ D.toFinset ⊆ C.toFinset := by
   simp only [subclause, List.all_eq_true, List.any_eq_true, beq_iff_eq, exists_eq_right]
   constructor
@@ -213,7 +213,7 @@ private theorem toClauseSet_flower {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c
     simp only [Bool.and_eq_true, beq_iff_eq, subclause_eq_true_iff]
     exact ⟨by rw [← List.toFinset_card_of_nodup (hnd C hC), hcard], hH⟩
 
-private theorem toFinset_filter_not_mem (C H : Clause V) :
+theorem toFinset_filter_not_mem (C H : Clause V) :
     (C.filter fun l => !H.any (· == l)).toFinset = C.toFinset \ H.toFinset := by
   ext l
   rw [List.mem_toFinset, List.mem_filter, Finset.mem_sdiff, List.mem_toFinset, List.mem_toFinset]

Complexity/Logics/Propositional/Resolution/Proof.lean

@@ -174,7 +174,7 @@ theorem fst_mem_vars (h : φ.IsProof ls) (hc : c ∈ ls) {l : Literal V} (hl : l
 end IsProof
 
 /-- A derivable clause is a line of some proof. -/
-private theorem Derives.exists_isProof (h : φ.Derives c) : ∃ ls, φ.IsProof ls ∧ c ∈ ls := by
+theorem Derives.exists_isProof (h : φ.Derives c) : ∃ ls, φ.IsProof ls ∧ c ∈ ls := by
   induction h with
   | mem hc => exact ⟨[_], IsProof.nil.mem hc, List.mem_singleton_self _⟩
   | resolvent v _ _ hv₁ hv₂ ih₁ ih₂ =>