refactor(Foundations,Probability,Languages): make 41 API and general declarations public again (#926)

Complexity/Foundations/BooleanAnalysis/Bernoulli.lean

@@ -149,7 +149,7 @@ theorem bernoulliAverage_sumElim {ι κ : Type*} [Fintype ι] [Fintype κ]
     rw [← Sum.elim_comp_inl_inr P]
     rfl
 
-private theorem bernoulliWeight_split {ι : Type*} [Fintype ι] (p : ℝ) (s x : ι → Bool) :
+theorem bernoulliWeight_split {ι : Type*} [Fintype ι] (p : ℝ) (s x : ι → Bool) :
     bernoulliWeight p x = bernoulliWeight p (fun i : {i // s i = true} => x i) *
       bernoulliWeight p (fun i : {i // s i ≠ true} => x i) :=
   (Fintype.prod_subtype_mul_prod_subtype (fun i => s i = true)

Complexity/Foundations/BooleanAnalysis/Fibers.lean

@@ -493,7 +493,7 @@ end Projection
 /-! ### Korten's entropy lemma -/
 
 /-- The log-sum inequality, from Jensen's inequality for `x log x`. -/
-private theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β → ℝ}
+theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β → ℝ}
     (hm : ∀ b, 0 ≤ m b) :
     (∑ b, m b) * Real.log ((∑ b, m b) / Fintype.card β) ≤ ∑ b, m b * Real.log (m b) := by
   have hc : (0 : ℝ) < Fintype.card β := by exact_mod_cast Fintype.card_pos
@@ -506,7 +506,7 @@ private theorem sum_mul_log_ge {β : Type*} [Fintype β] [Nonempty β] {m : β 
 
 /-- The logarithm of the size of the fiber of a uniform point of `X` under a map to `β` is on
 average at least `log |X| - log |β|`. -/
-private theorem expect_log_card_fiber {α β : Type*} [Fintype β] [Nonempty β] [DecidableEq β]
+theorem expect_log_card_fiber {α β : Type*} [Fintype β] [Nonempty β] [DecidableEq β]
     (X : Finset α) (hX : X.Nonempty) (g : α → β) :
     Real.log X.card - Real.log (Fintype.card β) ≤
       𝔼 x ∈ X, Real.log (X.filter (fun y => g y = g x)).card := by

Complexity/Foundations/BooleanAnalysis/HarmonicTransform.lean

@@ -183,7 +183,7 @@ private theorem resample_cons {n : ℕ} (s y x : Fin n → Bool) (a b c : Bool)
   funext i
   refine Fin.cases ?_ (fun j => ?_) i <;> simp [resample, Set.piecewise]
 
-private theorem projectionAverage_cons_false {n : ℕ}
+theorem projectionAverage_cons_false {n : ℕ}
     (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) :
     projectionAverage f (Fin.cons false selected) (Fin.cons b x) =
       projectionAverage (fun x => (f (Fin.cons false x) + f (Fin.cons true x)) / 2)
@@ -193,7 +193,7 @@ private theorem projectionAverage_cons_false {n : ℕ}
   simp only [resample_cons, Bool.false_eq_true, ite_false]
   rw [← expect_div, expect_add_distrib]
 
-private theorem projectionAverage_cons_true {n : ℕ}
+theorem projectionAverage_cons_true {n : ℕ}
     (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) :
     projectionAverage f (Fin.cons true selected) (Fin.cons b x) =
       projectionAverage (fun x => f (Fin.cons b x)) selected x := by
@@ -202,7 +202,7 @@ private theorem projectionAverage_cons_true {n : ℕ}
   simp only [resample_cons, ite_true]
   ring
 
-private theorem harmonicTransform_cons_false {n : ℕ}
+theorem harmonicTransform_cons_false {n : ℕ}
     (f : (Fin (n + 1) → Bool) → ℝ) (selected : Fin n → Bool) :
     harmonicTransform f (Fin.cons false selected) =
       harmonicTransform
@@ -214,7 +214,7 @@ private theorem harmonicTransform_cons_false {n : ℕ}
   simp_rw [projectionAverage_cons_false]
   simp [harmonicMean, Fintype.expect_prod_type]
 
-private theorem harmonicTransform_cons_true {n : ℕ}
+theorem harmonicTransform_cons_true {n : ℕ}
     {f : (Fin (n + 1) → Bool) → ℝ} (hf : ∀ x, 0 ≤ f x) (selected : Fin n → Bool) :
     harmonicTransform f (Fin.cons true selected) =
       2 * harmonicTransform (fun x => f (Fin.cons false x)) selected *

Complexity/Foundations/BooleanAnalysis/Hypercontractivity.lean

@@ -82,7 +82,7 @@ theorem expect_mul_noiseOp_mul (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) :
   rw [← noiseOp_noiseOp, expect_mul_noiseOp_comm]
 
 /-- The expectation of `f` against `T_{ρ σ} g` is at most `‖T_ρ f‖_2 ‖T_σ g‖_2`. -/
-private theorem expect_mul_noiseOp_mul_le (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) :
+theorem expect_mul_noiseOp_mul_le (ρ σ : ℝ) (f g : (ι → Bool) → ℝ) :
     𝔼 x, f x * noiseOp (ρ * σ) g x ≤ lpNorm 2 (noiseOp ρ f) * lpNorm 2 (noiseOp σ g) := by
   rw [expect_mul_noiseOp_mul, lpNorm_two, lpNorm_two]
   exact Real.expect_mul_le_sqrt_mul_sqrt _ _ _

Complexity/Foundations/BooleanAnalysis/Hypercontractivity/Derivative.lean

@@ -39,7 +39,7 @@ variable {ι : Type*} [Fintype ι] [DecidableEq ι]
 omit [Fintype ι] in
 /-- A power of the absolute value of the derivative of a Boolean function, read as signs, is the
 absolute value: the derivative takes the values `0` and `±1`. -/
-private theorem abs_derivative_signVal_rpow (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) {p : ℝ}
+theorem abs_derivative_signVal_rpow (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) {p : ℝ}
     (hp : p ≠ 0) :
     |derivative i (fun x => signVal (f x)) x| ^ p = |derivative i (fun x => signVal (f x)) x| := by
   simp only [derivative]

Complexity/Foundations/BooleanAnalysis/Hypercube.lean

@@ -63,7 +63,7 @@ open Finset Function Module
 variable {ι : Type*}
 
 /-- Flipping a bit of `T` negates the character of `T`. -/
-private theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι}
+theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι}
     {i : ι}
     (hi : i ∈ T) (x : ι → Bool) : chi R T (update x i (!x i)) = -chi R T x := by
   have h := chi_update_of_mem (R := R) hi x (x i)

Complexity/Foundations/BooleanAnalysis/KahnKalaiLinial.lean

@@ -112,7 +112,7 @@ private theorem sum_sum_filter_mem_fourierCoeff_sq_div_card (f : (ι → Bool) 
   · simp [not_not.1 hS]
 
 /-- The weight `∑_{S ∋ i} f̂(S) ^ 2 / |S|` is at most the influence of `i`. -/
-private theorem sum_filter_mem_fourierCoeff_sq_div_card_le_influence (f : (ι → Bool) → ℝ) (i : ι) :
+theorem sum_filter_mem_fourierCoeff_sq_div_card_le_influence (f : (ι → Bool) → ℝ) (i : ι) :
     ∑ S with i ∈ S, fourierCoeff f S ^ 2 / #S ≤ influence i f := by
   rw [influence_eq_sum_fourierCoeff_sq]
   refine sum_le_sum fun S hS => div_le_self (sq_nonneg _) ?_

Complexity/Foundations/Combinatorics/AffineDisperser.lean

@@ -143,7 +143,7 @@ theorem eq_of_covering {r : ℕ} (k : Fin r → ℕ) (hk : StrictAnti k) (hk0 :
 
 /-- **Averaging**: some `t`-element subset `I` of `S` carries at least a `t / |S|` share of
 `∑_{i ∈ S} d i`. -/
-private theorem exists_subset_card_eq_mul_sum_le {ι : Type*} (S : Finset ι) (d : ι → ℕ)
+theorem exists_subset_card_eq_mul_sum_le {ι : Type*} (S : Finset ι) (d : ι → ℕ)
     {t : ℕ} (ht : t ≤ S.card) :
     ∃ I ⊆ S, I.card = t ∧ t * ∑ i ∈ S, d i ≤ S.card * ∑ i ∈ I, d i := by
   classical

Complexity/Foundations/Combinatorics/AffineDisperser/Threshold.lean

@@ -54,7 +54,7 @@ namespace Cslib.AffineDisperser
 open Filter Explicit
 
 /-- Exponentials beat polynomials: `c * (n + 1) ^ k ≤ 2 ^ n` for all large `n`. -/
-private theorem eventually_mul_pow_le_two_pow (c k : ℕ) :
+theorem eventually_mul_pow_le_two_pow (c k : ℕ) :
     ∀ᶠ n : ℕ in atTop, c * (n + 1) ^ k ≤ 2 ^ n := by
   filter_upwards [Nat.eventually_mul_pow_le_pow (c * 2 ^ k) k one_lt_two,
     eventually_ge_atTop 1] with n hn hn1
@@ -92,7 +92,7 @@ private theorem eventually_chebyshevFactor_le :
     _ = 2 ^ (s + q * (8 * s + 10)) := by rw [← pow_mul, ← pow_add]
     _ ≤ 2 ^ L := Nat.pow_le_pow_right two_pos h3
 
-private theorem tendsto_log_two_atTop : Tendsto (Nat.log 2) atTop atTop :=
+theorem tendsto_log_two_atTop : Tendsto (Nat.log 2) atTop atTop :=
   tendsto_atTop_atTop.2 fun b => ⟨2 ^ b, fun _ hN => Nat.le_log_of_pow_le one_lt_two hN⟩
 
 /-- Decomposing `explicitThreshold N` into the budget `N / (⌊log₂ N⌋ + 1) ^ 2`, the block-count

Complexity/Foundations/Combinatorics/CentralBinomial.lean

@@ -128,7 +128,7 @@ theorem two_mul_card_small_le (n : ℕ) :
 
 /-- Subsets of size between `n / 2` and `n / 2 + t` number at most
 `(t + 1) · C(n, ⌊n/2⌋)`. -/
-private theorem card_middle_le (n t : ℕ) :
+theorem card_middle_le (n t : ℕ) :
     (univ.filter fun S : Finset (Fin n) =>
       n ≤ 2 * S.card ∧ S.card ≤ n / 2 + t).card ≤ (t + 1) * n.choose (n / 2) := by
   classical

Complexity/Foundations/Combinatorics/Expander/Walk.lean

@@ -485,7 +485,7 @@ variable [Fintype D]
 /-- From a fixed start `v`, the `i`-th dart of a uniformly random walk leaves the vertex reached by
 the random walk after `i` steps along a uniformly random label: the average of `f` over it is
 `(G.walk ^ i) (fun w ↦ 𝔼 a, f (w, a)) v`. -/
-private theorem expect_walkDart_mk (v : V) (i : Fin t) (f : V × D → ℝ) :
+theorem expect_walkDart_mk (v : V) (i : Fin t) (f : V × D → ℝ) :
     𝔼 k : Fin t → D, f (G.walkDart (v, k) i) = (G.walk ^ (i : ℕ)) (fun w ↦ 𝔼 a, f (w, a)) v := by
   rcases isEmpty_or_nonempty D with hD | hD
   · have : IsEmpty (Fin t → D) := ⟨fun k ↦ hD.false (k i)⟩

Complexity/Foundations/Combinatorics/FunctionalGraph/Cycle.lean

@@ -61,7 +61,7 @@ variable {α : Type u} [Finite α] (f : α → α)
 
 omit [Finite α] in
 /-- Periodic points reached at different times along one orbit have the same minimal period. -/
-private theorem minimalPeriod_eq_of_periodic_iterates (x : α) {a b : ℕ}
+theorem minimalPeriod_eq_of_periodic_iterates (x : α) {a b : ℕ}
     (ha : f^[a] x ∈ periodicPts f) (hb : f^[b] x ∈ periodicPts f) :
     minimalPeriod f (f^[a] x) = minimalPeriod f (f^[b] x) := by
   rcases le_total a b with h | h

Complexity/Foundations/Combinatorics/FunctionalGraph/ForestIntervals.lean

@@ -106,7 +106,7 @@ theorem forestPath_injective : Function.Injective (forestPath f) := by
 theorem self_mem_forestPath (x : α) : x ∈ forestPath f x :=
   (mem_forestPath f x x).mpr ⟨0, Nat.zero_le _, rfl⟩
 
-private theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) :
+theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) :
     forestPath f x = forestPath f (f x) ++ [x] := by
   have hd : transientDepth f (f x) + 1 = transientDepth f x := by
     have hh := transientDepth_iterate f x 1
@@ -117,7 +117,7 @@ private theorem forestPath_step (x : α) (hx : 0 < transientDepth f x) :
     (forestTrace f (f x) (transientDepth f (f x) + 1)).reverse ++ [x]
   rw [hd]
 
-private theorem forestPath_iterate_prefix (x : α) {t : ℕ} (ht : t ≤ transientDepth f x) :
+theorem forestPath_iterate_prefix (x : α) {t : ℕ} (ht : t ≤ transientDepth f x) :
     forestPath f (f^[t] x) <+: forestPath f x := by
   induction t generalizing x with
   | zero => exact ⟨[], List.append_nil _⟩

Complexity/Foundations/Combinatorics/MajorityTree.lean

@@ -62,7 +62,7 @@ variable {α : Type*} [DecidableEq α]
 def maj3 (a b c : α) : α := if a = b then a else c
 
 /-- If `maj3 a b c` misses `y`, then two of `a`, `b`, `c` miss `y`. -/
-private theorem two_ne_of_maj3_ne {a b c y : α} (h : maj3 a b c ≠ y) :
+theorem two_ne_of_maj3_ne {a b c y : α} (h : maj3 a b c ≠ y) :
     (a ≠ y ∧ b ≠ y) ∨ (a ≠ y ∧ c ≠ y) ∨ (b ≠ y ∧ c ≠ y) := by
   unfold maj3 at h
   split_ifs at h with hab

Complexity/Foundations/Data/BitString/PartialAssignment/Counting.lean

@@ -83,7 +83,7 @@ free. -/
 
 /-- For a fixed subset `S ∈ powersetCard ℓ ρ₀.free`, there are `2 ^ (#ρ₀.free - ℓ)` extensions in
 `ρ₀.extensions ℓ` whose free set is `S`. -/
-private theorem card_filter_extensions_free_eq (ρ₀ : PartialAssignment ι) (ℓ : ℕ)
+theorem card_filter_extensions_free_eq (ρ₀ : PartialAssignment ι) (ℓ : ℕ)
     {S : Finset ι} (hS : S ∈ powersetCard ℓ ρ₀.free) :
     #{ρ ∈ ρ₀.extensions ℓ | ρ.free = S} = 2 ^ (#ρ₀.free - ℓ) := by
   obtain ⟨hSsub, hScard⟩ := mem_powersetCard.1 hS
@@ -158,7 +158,7 @@ theorem card_filter_extensions_free_subset (ρ₀ : PartialAssignment ι) (ℓ :
 
 /-- The number of extensions in `ρ₀.extensions ℓ` that fix every coordinate of `B ⊆ ρ₀.free` is
 `C(#ρ₀.free - |B|, ℓ) * 2 ^ (#ρ₀.free - ℓ)`. -/
-private theorem card_filter_extensions_not_nonempty_inter (ρ₀ : PartialAssignment ι) (ℓ : ℕ)
+theorem card_filter_extensions_not_nonempty_inter (ρ₀ : PartialAssignment ι) (ℓ : ℕ)
     {B : Finset ι} (hB : B ⊆ ρ₀.free) :
     #{ρ ∈ ρ₀.extensions ℓ | ¬(ρ.free ∩ B).Nonempty} =
       (#ρ₀.free - #B).choose ℓ * 2 ^ (#ρ₀.free - ℓ) := by
@@ -199,7 +199,7 @@ theorem card_withFree (ℓ : ℕ) :
 
 /-- A partial assignment with `ℓ'` free coordinates extends `C(|ι| - ℓ', ℓ - ℓ')` of the ones
 with `ℓ ≥ ℓ'` free coordinates: those that free `ℓ - ℓ'` of its fixed coordinates. -/
-private theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ : ℕ}
+theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ : ℕ}
     (hℓ : #ρ'.free ≤ ℓ) :
     #((withFree ι ℓ).filter fun ρ => ρ'.Extends ρ) =
       (Fintype.card ι - #ρ'.free).choose (ℓ - #ρ'.free) := by
@@ -241,7 +241,7 @@ private theorem card_filter_extends_withFree {ρ' : PartialAssignment ι} {ℓ :
 
 /-- The words agreeing with a partial assignment outside its free coordinates: `2 ^ ℓ` of them for
 `ℓ` free coordinates. -/
-private theorem card_filter_outside_eq (ρ : PartialAssignment ι) :
+theorem card_filter_outside_eq (ρ : PartialAssignment ι) :
     #{z : ι → Bool | outside ρ.free z = ρ} = 2 ^ #ρ.free := by
   rw [← card_filter_forall_notMem_eq ρ.free (ρ.fill fun _ => false)]
   congr 1

Complexity/Foundations/Data/BitString/ShortWords.lean

@@ -95,7 +95,7 @@ theorem nil_mem_shortWords (L : ℕ) : [] ∈ shortWords L := by simp
 
 /-- The binary words of length at most `L` are the words `List.ofFn r` for `r : Fin m → Bool` and
 `m ≤ L`. -/
-private theorem shortWords_eq_biUnion (L : ℕ) :
+theorem shortWords_eq_biUnion (L : ℕ) :
     shortWords L =
       (range (L + 1)).biUnion fun m => univ.image (List.ofFn : (Fin m → Bool) → _) := by
   ext w

Complexity/Foundations/Data/Code/HammingBound.lean

@@ -66,7 +66,7 @@ variable {ι : Type*} [Fintype ι] [DecidableEq ι] {β : ι → Type*} [∀ i,
 
 /-- The words differing from `x` exactly at the positions `S`: a different letter at each position
 of `S`. -/
-private theorem card_filter_filter_ne_eq (x : ∀ i, β i) (S : Finset ι) :
+theorem card_filter_filter_ne_eq (x : ∀ i, β i) (S : Finset ι) :
     #{y : ∀ i, β i | ({i | x i ≠ y i} : Finset ι) = S} = ∏ i ∈ S, (Fintype.card (β i) - 1) := by
   have h : #{y : ∀ i, β i | ({i | x i ≠ y i} : Finset ι) = S} =
       Fintype.card (∀ i, {b : β i // (i ∈ S ↔ x i ≠ b)}) := by

Complexity/Foundations/Data/Nat/Bitwise/Multiplication.lean

@@ -105,7 +105,7 @@ private theorem sum_pairs (x y : ℕ) :
 /-- The weighted contribution of all columns strictly below `k`. -/
 def mulPrefix (x y k : ℕ) : ℕ := ∑ j ∈ range k, mulColumn x y j * 2 ^ j
 
-private theorem mulPrefix_succ (x y k : ℕ) :
+theorem mulPrefix_succ (x y k : ℕ) :
     mulPrefix x y (k + 1) = mulPrefix x y k + mulColumn x y k * 2 ^ k := sum_range_succ _ _
 
 private theorem mulPrefix_eq_filter (x y k : ℕ) :
@@ -162,7 +162,7 @@ def mulCarry (x y k : ℕ) : ℕ := mulPrefix x y k / 2 ^ k
 /-- No carry enters column `0`. -/
 @[simp] theorem mulCarry_zero (x y : ℕ) : mulCarry x y 0 = 0 := by simp [mulCarry, mulPrefix]
 
-private theorem mulCarry_succ (x y k : ℕ) :
+theorem mulCarry_succ (x y k : ℕ) :
     mulCarry x y (k + 1) = (mulCarry x y k + mulColumn x y k) / 2 := by
   simp only [mulCarry, mulPrefix_succ, pow_succ, ← Nat.div_div_eq_div_mul,
     Nat.add_mul_div_right _ _ (Nat.two_pow_pos k)]

Complexity/Foundations/Data/StackTape.lean

@@ -148,7 +148,7 @@ lemma ofList_append_replicate_none (l : List (Option Symbol)) (n : ℕ) :
     ofList (l.map some) = mapSome l := by
   exact ofList_toList (mapSome l)
 
-private lemma listBlank_mk_cons_toList (a : Option Symbol) (tape : StackTape Symbol) :
+lemma listBlank_mk_cons_toList (a : Option Symbol) (tape : StackTape Symbol) :
     _root_.Turing.ListBlank.mk (cons a tape).toList =
       _root_.Turing.ListBlank.cons a (_root_.Turing.ListBlank.mk tape.toList) := by
   cases a with

Complexity/Foundations/FieldTheory/Finite/BinaryField.lean

@@ -155,7 +155,7 @@ noncomputable def leastIrreducible (p : ℕ) : (ZMod 2)[X] :=
     polyOfCode (Nat.find h)
   else X
 
-private theorem exists_code_irreducible {p : ℕ} (hp : p ≠ 0) :
+theorem exists_code_irreducible {p : ℕ} (hp : p ≠ 0) :
     ∃ m, Irreducible (polyOfCode m) ∧ (polyOfCode m).natDegree = p := by
   obtain ⟨g, hg, hgp⟩ := exists_irreducible_natDegree_eq hp
   obtain ⟨m, rfl⟩ := polyOfCode_surjective g

Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean

@@ -352,7 +352,7 @@ theorem linearizedEval_pow_two_pow [Finite F] {n : ℕ} [NeZero n] (hn : finrank
     pow_two_pow_mod hn x (j.val + k), ZMod.val_add, ZMod.val_natCast, Nat.add_mod_mod]
 
 omit [Algebra (ZMod 2) F] in
-private theorem linearizedEval_sub_mul {n : ℕ} [NeZero n] (a b : ZMod n → F) (c x : F) :
+theorem linearizedEval_sub_mul {n : ℕ} [NeZero n] (a b : ZMod n → F) (c x : F) :
     linearizedEval (fun j => b j - c * a j) x = linearizedEval b x - c * linearizedEval a x := by
   simp only [linearizedEval, sub_mul, Finset.sum_sub_distrib, Finset.mul_sum, mul_assoc]
 

Complexity/Foundations/LinearAlgebra/Matrix/CutRank.lean

@@ -88,7 +88,7 @@ theorem blockRank_eq_rank [Finite m] (S : Set m) (T : Set n) [Fintype T] :
 
 /-- Restricting the columns of a block maps its row space onto the row space of the smaller
 block. -/
-private theorem span_range_row_submatrix_eq_map (S : Set m) {T T' : Set n} (h : T' ⊆ T) :
+theorem span_range_row_submatrix_eq_map (S : Set m) {T T' : Set n} (h : T' ⊆ T) :
     span K (range (M.submatrix ((↑) : S → m) ((↑) : T' → n)).row) =
       (span K (range (M.submatrix ((↑) : S → m) ((↑) : T → n)).row)).map
         (LinearMap.funLeft K K (inclusion h)) := by

Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean

@@ -356,7 +356,7 @@ theorem add_blockRank_le_cutRank_add_transpose [Finite ι]
   omega
 
 /-- Two injective maps with disjoint ranges pull back at most `|V|` elements of `V`. -/
-private theorem ncard_preimage_add_ncard_preimage_le [Finite ι] {f : κ → ι} {g : κ' → ι}
+theorem ncard_preimage_add_ncard_preimage_le [Finite ι] {f : κ → ι} {g : κ' → ι}
     (hf : Function.Injective f) (hg : Function.Injective g) (hfg : Disjoint (range f) (range g))
     (V : Set ι) : (f ⁻¹' V).ncard + (g ⁻¹' V).ncard ≤ V.ncard := by
   rw [← ncard_image_of_injective _ hf, ← ncard_image_of_injective _ hg,

Complexity/Languages/Probabilistic/LinearHash.lean

@@ -77,7 +77,7 @@ theorem eval_extract_bind {n m : ℕ} (source : PMF (BitString n)) :
     wordHash_eq_ofFn, ofList_ofFn, blocksEquiv_apply]
 
 /-- The word extractor's exact finite law on one fixed-width input. -/
-private theorem eval_extract_ofFn {n m : ℕ} (input : BitString n) :
+theorem eval_extract_ofFn {n m : ℕ} (input : BitString n) :
     ProbComp.eval (extract m (List.ofFn input)) =
       (PMF.uniformOfFintype (BitString (m * n))).map
         (fun seed => List.ofFn seed ++

Complexity/Probability/BitString/LinearHash.lean

@@ -99,7 +99,7 @@ theorem isTwoUniversal (n m : ℕ) :
   (isDeltaUniversalHash n m).isTwoUniversal
 
 /-- Any initial block of a uniform matrix is itself uniform. Unused rows may remain public. -/
-private theorem uniform_prefix {n m count : ℕ} (h : m ≤ count) :
+theorem uniform_prefix {n m count : ℕ} (h : m ≤ count) :
     (PMF.uniformOfFintype (Fin count → BitString n)).map
         (fun rows => rows ∘ Fin.castLE h) =
       PMF.uniformOfFintype (Fin m → BitString n) := by

Complexity/Probability/Conditioning.lean

@@ -55,7 +55,7 @@ theorem map_fst_apply (joint : PMF (α × β)) (a : α) :
     simp [Ne.symm hx]
 
 /-- Each joint mass is at most the corresponding marginal mass. -/
-private theorem apply_le_map_fst (joint : PMF (α × β)) (a : α) (b : β) :
+theorem apply_le_map_fst (joint : PMF (α × β)) (a : α) (b : β) :
     joint (a, b) ≤ (joint.map Prod.fst) a :=
   le_map_apply joint Prod.fst (a, b)
 

Complexity/Probability/HashIsolation.lean

@@ -158,7 +158,7 @@ theorem IsTwoUniversal.conditionalEntropy_hash_le [Finite Seed] {seed : PMF Seed
 omit [Fintype Seed] [Fintype Output] in
 /-- Averaging over hash lengths `1, …, count` leaves at most the average logarithmic fiber size
 plus two bits, divided by `count`. This is the entropy bound in Holenstein's Lemma 3. -/
-private theorem mean_conditionalEntropy_hash_le [Finite Seed] (count : ℕ) (seed : PMF Seed)
+theorem mean_conditionalEntropy_hash_le [Finite Seed] (count : ℕ) (seed : PMF Seed)
     (source : PMF Input)
     (f : Input → Image) (hash : (i : Fin count) → Seed → Input → (Fin (i.val + 1) → Bool))
     (hhash : ∀ i, IsTwoUniversal seed (hash i)) (predicate : Fin count → Seed → Input → Bool) :