refactor(foundations): move general arithmetic and counting lemmas out of Classes (#610)

Complexity.lean

@@ -1700,6 +1700,7 @@ public import Complexity.Foundations.Data.Nat.Log
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Log
+public import Complexity.Foundations.Data.Nat.Primrec
 public import Complexity.Foundations.Data.Nat.Radix
 public import Complexity.Foundations.Data.OrderedSet
 public import Complexity.Foundations.Data.Polynomial.CoeffList

Complexity/Computability/Complexity/Classes/Toda/Counting.lean

@@ -17,9 +17,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bi
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
-import Mathlib.Data.Finset.Sort
 import Mathlib.Data.List.GetD
-import Mathlib.Data.Nat.Choose.Sum
 
 /-!
 # Counting the parities of a random string with one bit of a `#P` value
@@ -34,16 +32,16 @@ Toda's amplifier uses residues `0` modulo `2 ^ K` for even counts and `-1` for o
 This module uses the opposite sign: `0` for even counts and `+1` for odd counts. Negating our
 amplifier modulo `2 ^ K` recovers the `0`/`-1` convention. All subsequent counts and bit
 extraction here use the `+1` convention, from the binomial expansion of `(1 - 2) ^ c`
-(`Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose`):
+(`Cslib.BitString.sum_range_neg_two_pow_mul_choose`):
 
 `[c odd] = ∑ i < c, (-2) ^ i * choose c (i + 1)`,
 
 whose terms with `i ≥ K` vanish modulo `2 ^ K`
-(`Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose_zmod`). The coefficients `(-2) ^ i` are
+(`Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod`). The coefficients `(-2) ^ i` are
 replaced by naturals equal to them modulo `2 ^ K` (`Cslib.Complexity.Toda.parityCoeff`), and
 `choose (f r) k` counts the `k`-element sets of accepted witnesses, written as strictly
 increasing lists of `k` words for the lexicographic order
-(`Cslib.Complexity.Toda.card_filter_strictMono`, `Cslib.BitString.wordLt_ofFn_iff`). So
+(`Cslib.BitString.card_filter_strictMono`, `Cslib.BitString.wordLt_ofFn_iff`). So
 the words accepted by `Cslib.Complexity.Toda.countingTest` — a size `k ≤ K` in unary, one of
 `parityCoeff K (k - 1)` coefficient words, a random string `r` and a strictly increasing list of
 `k` accepted witnesses, padded with zero words — number
@@ -66,9 +64,6 @@ odd number of accepted witnesses (`Cslib.Complexity.Toda.testBit_card_filter_sha
 
 ## Main results
 
-* `Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose_zmod`: the parity of `c` from binomial
-  coefficients, modulo `2 ^ K`.
-* `Cslib.Complexity.Toda.card_filter_strictMono`: strictly increasing tuples count subsets.
 * `Cslib.Complexity.Toda.cast_card_filter_countingTest`: the count is `G` modulo `2 ^ (R + 1)`.
 * `Cslib.Complexity.Toda.testBit_card_filter_sharpTest`: one bit says whether `2 G > 2 ^ R`.
 
@@ -82,55 +77,10 @@ odd number of accepted witnesses (`Cslib.Complexity.Toda.testBit_card_filter_sha
 
 namespace Cslib.Complexity.Toda
 
-open Finset Turing.MultiTapeTM
+open Finset BitString Turing.MultiTapeTM
 
 /-! ### Modulus amplification -/
 
-/-- **The parity of `c` from the binomial expansion of `(1 - 2) ^ c`**:
-`∑ i < c, (-2) ^ i * choose c (i + 1)` is `1` for odd `c` and `0` for even `c`. -/
-theorem sum_range_neg_two_pow_mul_choose (c : ℕ) :
-    ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = if Odd c then 1 else 0 := by
-  have hbin : ∑ i ∈ range (c + 1), (-2 : ℤ) ^ i * (c.choose i : ℤ) = (-1) ^ c := by
-    have := add_pow (-2 : ℤ) 1 c
-    simp only [one_pow, mul_one] at this
-    rw [show (-2 : ℤ) + 1 = -1 by norm_num] at this
-    rw [this]
-  rw [sum_range_succ'] at hbin
-  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at hbin
-  have h : -2 * ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = (-1) ^ c - 1 := by
-    rw [mul_sum]
-    rw [← hbin]
-    simp only [pow_succ]
-    ring_nf
-  split
-  · rename_i hc
-    rw [hc.neg_one_pow] at h
-    linarith
-  · rename_i hc
-    rw [(Nat.not_odd_iff_even.1 hc).neg_one_pow, sub_self] at h
-    linarith
-
-/-- **The parity of `c` modulo `2 ^ K`**: only the first `K` binomial terms matter. -/
-theorem sum_range_neg_two_pow_mul_choose_zmod (c K : ℕ) :
-    ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      if Odd c then 1 else 0 := by
-  have hexact := congrArg (Int.cast : ℤ → ZMod (2 ^ K)) (sum_range_neg_two_pow_mul_choose c)
-  push_cast at hexact
-  rw [← hexact]
-  have hK : (-2 : ZMod (2 ^ K)) ^ K = 0 := by
-    have h2 : (2 : ZMod (2 ^ K)) ^ K = 0 := by
-      exact_mod_cast ZMod.natCast_self (2 ^ K)
-    rw [neg_pow, h2, mul_zero]
-  have h₁ : ∑ i ∈ range (K + c), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
-    rw [sum_range_add]
-    simp [pow_add, hK]
-  have h₂ : ∑ i ∈ range (c + K), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      ∑ i ∈ range c, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
-    rw [sum_range_add]
-    simp [Nat.choose_eq_zero_of_lt (by omega : c < c + _ + 1)]
-  rw [← h₁, ← h₂, Nat.add_comm]
-
 /-- Natural coefficients equal to `(-2) ^ i` modulo `2 ^ K`, for `i ≤ K`: `2 ^ i` for even `i`
 and `2 ^ K - 2 ^ i` for odd `i`. -/
 def parityCoeff (K i : ℕ) : ℕ := if Even i then 2 ^ i else 2 ^ K - 2 ^ i
@@ -184,43 +134,6 @@ private theorem testBit_two_mul_add_two_pow_sub_one {R G H : ℕ} (hG : G ≤ 2
 
 /-! ### Subsets as strictly increasing tuples -/
 
-/-- **Strictly increasing tuples count subsets**: the strictly increasing `k`-tuples of elements
-of `A` are as many as the `k`-element subsets of `A`. -/
-theorem card_filter_strictMono {β : Type*} [LinearOrder β] [Fintype β] (A : Finset β) (k : ℕ)
-    [DecidablePred fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A] :
-    (univ.filter fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A).card = (#A).choose k := by
-  classical
-  rw [← card_powersetCard]
-  refine card_bij (fun g _ => univ.image g) ?_ ?_ ?_
-  · intro g hg
-    simp only [mem_filter, mem_univ, true_and] at hg
-    rw [mem_powersetCard]
-    refine ⟨fun x hx => ?_, ?_⟩
-    · obtain ⟨i, -, rfl⟩ := mem_image.1 hx
-      exact hg.2 i
-    · rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
-  · intro g hg g' hg' h
-    simp only [mem_filter, mem_univ, true_and] at hg hg'
-    have hc : (univ.image g).card = k := by
-      rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
-    have h1 : g = (univ.image g).orderEmbOfFin hc :=
-      orderEmbOfFin_unique hc (fun i => mem_image_of_mem g (mem_univ i)) hg.1
-    have h2 : g' = (univ.image g).orderEmbOfFin hc :=
-      orderEmbOfFin_unique hc (fun i => h ▸ mem_image_of_mem g' (mem_univ i)) hg'.1
-    rw [h1, ← h2]
-  · intro s hs
-    rw [mem_powersetCard] at hs
-    refine ⟨s.orderEmbOfFin hs.2, ?_, image_orderEmbOfFin_univ s hs.2⟩
-    simp only [mem_filter, mem_univ, true_and]
-    exact ⟨(s.orderEmbOfFin hs.2).strictMono, fun i => hs.1 (orderEmbOfFin_mem s hs.2 i)⟩
-
-/-- A tuple increasing at every step is strictly increasing. -/
-private theorem strictMono_of_lt_succ {β : Type*} [Preorder β] {k : ℕ} {g : Fin k → β}
-    (h : ∀ (i : ℕ) (hi : i + 1 < k), g ⟨i, by omega⟩ < g ⟨i + 1, hi⟩) : StrictMono g := by
-  cases k with
-  | zero => exact fun i => i.elim0
-  | succ k => exact Fin.strictMono_iff_lt_succ.2 fun i => h i (by omega)
-
 /-- The `k`-subset test on `K` rows of `Z` bits: the first `k` rows are accepted by `acc` and
 strictly increasing, and the other rows are zero. -/
 def subsetTest (acc : List Bool → Bool) (K Z k : ℕ) (zs : List Bool) : Bool :=

Complexity/Computability/Complexity/Classes/Toda/Isolation.lean

@@ -39,7 +39,7 @@ A *trial* sums the numbers `c x` over the strings `x` passing the test of some l
 seed; its parity is the parity of the number of `x` with `c x` odd that pass the test
 (`Finset.odd_sum_iff_odd_card_odd`). The trials are combined by the parity form of a
 disjunction: `1 + ∏ⱼ (1 + cⱼ)` is odd exactly when some `cⱼ` is
-(`Cslib.Complexity.Toda.odd_one_add_prod_one_add`). Running `4 (E + 1)` rounds, each with one
+(`Cslib.BitString.odd_one_add_prod_one_add`). Running `4 (E + 1)` rounds, each with one
 trial at every level `k ≤ M + 2`, the combined number is odd exactly when `S` is nonempty, unless
 some `c x` has the wrong parity or every round fails to isolate an element of `S`
 (`Cslib.Complexity.Toda.two_pow_mul_card_filter_not_odd_iff_le`). With `c x` depending on
@@ -54,7 +54,6 @@ first failure has probability at most `2 ^ M * 2 ^ (-(E + M + 1))`, the second a
 
 ## Main results
 
-* `Cslib.Complexity.Toda.odd_one_add_prod_one_add`: the parity form of a disjunction.
 * `Cslib.Complexity.Toda.hashesToZero_ofFn_iff`: the test is the affine hash hitting `0`.
 * `Cslib.Complexity.Toda.three_mul_two_pow_le_card_filter_card_eq_one`: isolation with
   probability at least `3 / 16`.
@@ -73,58 +72,7 @@ first failure has probability at most `2 ^ M * 2 ^ (-(E + M + 1))`, the second a
 
 namespace Cslib.Complexity.Toda
 
-open Finset Turing.MultiTapeTM
-
-/-! ### Counting words -/
-
-/-- A product of naturals is odd exactly when every factor is. -/
-theorem odd_prod_iff {ι : Type*} {s : Finset ι} (f : ι → ℕ) :
-    Odd (∏ j ∈ s, f j) ↔ ∀ j ∈ s, Odd (f j) := by
-  classical
-  induction s using Finset.induction_on with
-  | empty => simp
-  | insert a s ha ih => rw [Finset.prod_insert ha, Nat.odd_mul, ih, Finset.forall_mem_insert]
-
-/-- **The parity form of a disjunction**: `1 + ∏ⱼ (1 + cⱼ)` is odd exactly when some `cⱼ` is
-odd. -/
-theorem odd_one_add_prod_one_add {ι : Type*} [Fintype ι] (c : ι → ℕ) :
-    Odd (1 + ∏ j, (1 + c j)) ↔ ∃ j, Odd (c j) := by
-  rw [Nat.add_comm, Nat.odd_add_one, odd_prod_iff]
-  simp only [mem_univ, true_imp_iff, not_forall]
-  refine exists_congr fun j => ?_
-  rw [Nat.add_comm, Nat.odd_add_one, not_not]
-
-/-- The functions `s : ι → X` whose values at the `t` distinct points `f i` lie in `F`: `F` is
-chosen at those points and anything elsewhere. -/
-private theorem card_filter_forall_apply_mem {ι X : Type*} [Fintype ι] [DecidableEq ι] [Fintype X]
-    [DecidableEq X] {t : ℕ} (f : Fin t → ι) (hf : Function.Injective f) (F : Finset X) :
-    (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F).card =
-      #F ^ t * Fintype.card X ^ (Fintype.card ι - t) := by
-  classical
-  have h : (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F) =
-      Fintype.piFinset fun j => if j ∈ Finset.image f univ then F else univ := by
-    ext s
-    simp only [mem_filter, mem_univ, true_and, Fintype.mem_piFinset]
-    constructor
-    · intro hs j
-      split
-      · rename_i hj
-        obtain ⟨i, -, rfl⟩ := Finset.mem_image.1 hj
-        exact hs i
-      · exact mem_univ _
-    · intro hs i
-      have := hs (f i)
-      rwa [ite_eq_left_iff.2 (fun h => absurd (Finset.mem_image_of_mem f (mem_univ i)) h)]
-        at this
-  rw [h, Fintype.card_piFinset]
-  simp only [apply_ite Finset.card, card_univ]
-  rw [Finset.prod_ite, Finset.prod_const, Finset.prod_const]
-  have himg : (univ.filter fun j => j ∈ Finset.image f univ) = Finset.image f univ := by
-    ext j; simp
-  have hcard : #(Finset.image f univ) = t := by
-    rw [Finset.card_image_of_injective _ hf, card_univ, Fintype.card_fin]
-  rw [himg, hcard, Finset.filter_not, himg, Finset.card_sdiff_of_subset (subset_univ _), hcard,
-    card_univ]
+open Finset BitString Turing.MultiTapeTM
 
 /-! ### The Valiant–Vazirani test -/
 
@@ -247,27 +195,6 @@ private theorem two_pow_mul_thirteen_pow_le (E : ℕ) :
   rw [pow_mul, pow_mul, ← mul_pow]
   exact Nat.pow_le_pow_left (by norm_num) _
 
-/-- **The union bound for random strings**: if each `x` is bad for at most a `2 ^ (-e')` fraction
-of the random strings, some `x` of length `M` is bad for at most a `2 ^ (M - e')` fraction. -/
-private theorem two_pow_mul_card_filter_exists_le {R M e' : ℕ}
-    {Bad : (Fin R → Bool) → (Fin M → Bool) → Prop}
-    [∀ r x, Decidable (Bad r x)]
-    (h : ∀ x, 2 ^ e' * (univ.filter fun r => Bad r x).card ≤ 2 ^ R) :
-    2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card ≤ 2 ^ M * 2 ^ R := by
-  classical
-  have hsub : (univ.filter fun r => ∃ x, Bad r x) ⊆
-      univ.biUnion fun x => univ.filter fun r => Bad r x := by
-    intro r hr
-    simp only [mem_filter, mem_univ, true_and] at hr
-    obtain ⟨x, hx⟩ := hr
-    exact mem_biUnion.2 ⟨x, mem_univ _, by simpa using hx⟩
-  calc 2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card
-      ≤ 2 ^ e' * ∑ x, (univ.filter fun r => Bad r x).card :=
-        Nat.mul_le_mul_left _ ((card_le_card hsub).trans card_biUnion_le)
-    _ = ∑ x : Fin M → Bool, 2 ^ e' * (univ.filter fun r => Bad r x).card := mul_sum ..
-    _ ≤ ∑ _x : Fin M → Bool, 2 ^ R := sum_le_sum fun x _ => h x
-    _ = 2 ^ M * 2 ^ R := by simp
-
 /-- **The isolation step errs with probability at most `2 ^ (-E)`.** Let `c r x` be numbers
 whose parity says whether `x ∈ S`, except for at most a `2 ^ (-e')` fraction of the random
 strings `r` of length `R`, for each string `x` of length `M`, where `e' ≥ E + M + 1`. Draw seeds

Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean

@@ -11,6 +11,7 @@ public import Complexity.Init
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Data.Nat.Digits.Defs
 import Mathlib.Tactic.Ring
 
 /-!
@@ -40,49 +41,36 @@ open Finset
 
 namespace Nat
 
+private theorem sum_range_mul_pow_eq_ofDigits (b N : ℕ) (a : ℕ → ℕ) :
+    ∑ p ∈ range N, a p * b ^ p = ofDigits b ((List.range N).map a) := by
+  induction N with
+  | zero => rfl
+  | succ N ih =>
+    rw [sum_range_succ, ih, List.range_succ, List.map_append, List.map_singleton, ofDigits_append]
+    simp [mul_comm]
+
 /-- Base-`b` digits that are less than `b` are determined by the number they represent. -/
 theorem sum_range_mul_pow_inj {b N : ℕ} {a c : ℕ → ℕ} (ha : ∀ p < N, a p < b)
     (hc : ∀ p < N, c p < b) :
     ∑ p ∈ range N, a p * b ^ p = ∑ p ∈ range N, c p * b ^ p ↔ ∀ p < N, a p = c p := by
-  refine ⟨fun h => ?_, fun h => sum_congr rfl fun p hp => by rw [h p (mem_range.1 hp)]⟩
-  induction N generalizing a c with
-  | zero => simp
-  | succ N ih =>
-    have hb : 0 < b := (Nat.zero_le _).trans_lt (ha 0 (by lia))
-    have hshift (d : ℕ → ℕ) : ∑ p ∈ range (N + 1), d p * b ^ p =
-        d 0 + b * ∑ p ∈ range N, d (p + 1) * b ^ p := by
-      rw [sum_range_succ', mul_sum]
-      simp only [pow_succ, pow_zero, mul_one]
-      rw [add_comm]
-      congr 1
-      exact sum_congr rfl fun p _ => by ring
-    rw [hshift, hshift] at h
-    have h0 : a 0 = c 0 := by
-      have := congrArg (· % b) h
-      simpa [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt (ha 0 (by lia)),
-        Nat.mod_eq_of_lt (hc 0 (by lia))] using this
-    rw [h0, Nat.add_left_cancel_iff, Nat.mul_left_cancel_iff hb] at h
-    have ih' := ih (a := fun p => a (p + 1)) (c := fun p => c (p + 1))
-      (fun p hp => ha _ (by lia)) (fun p hp => hc _ (by lia)) h
-    intro p hp
-    rcases p with _ | p
-    · exact h0
-    · exact ih' p (by lia)
+  refine ⟨fun h p hp => ?_, fun h => sum_congr rfl fun p hp => by rw [h p (mem_range.1 hp)]⟩
+  rcases le_or_gt b 1 with hb | hb
+  · have := ha p hp; have := hc p hp; omega
+  · rw [sum_range_mul_pow_eq_ofDigits, sum_range_mul_pow_eq_ofDigits] at h
+    have hL := ofDigits_inj_of_len_eq hb (by simp) (by simpa using ha) (by simpa using hc) h
+    have := congrArg (·[p]?) hL
+    simpa [hp] using this
 
 /-- A number with base-`b` digits below `b` at the positions below `N` is less than `b ^ N`. -/
 theorem sum_range_mul_pow_lt {b N : ℕ} {a : ℕ → ℕ} (ha : ∀ p < N, a p < b) :
     ∑ p ∈ range N, a p * b ^ p < b ^ N := by
-  induction N with
-  | zero => simp
-  | succ N ih =>
-    rw [sum_range_succ, pow_succ]
-    have h₁ := ih fun p hp => ha p (by lia)
-    have h₂ : a N * b ^ N ≤ (b - 1) * b ^ N := Nat.mul_le_mul_right _ (by have := ha N; lia)
-    have h₃ : b ^ N + (b - 1) * b ^ N = b ^ N * b := by
-      obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le ((Nat.zero_le _).trans_lt (ha N (by lia)))
-      simp only [Nat.add_sub_cancel_left]
-      ring
-    lia
+  rcases N.eq_zero_or_pos with rfl | hN
+  · simp
+  rcases le_or_gt b 1 with hb | hb
+  · obtain rfl : b = 1 := by have := ha 0 hN; omega
+    simpa using fun i hi => by have := ha i hi; omega
+  · rw [sum_range_mul_pow_eq_ofDigits]
+    simpa using ofDigits_lt_base_pow_length (l := (List.range N).map a) hb (by simpa using ha)
 
 end Nat
 

Complexity/Computability/Kolmogorov/Incompressibility.lean

@@ -22,8 +22,6 @@ of length `n` have complexity below `n - c` [Li and Vitányi, Chapter 2][LiVitan
 
 ## Main results
 
-* `Cslib.Kolmogorov.encard_setOf_length_lt_add_one`: there are `2 ^ n - 1` binary strings of
-  length below `n`, using `Cslib.BitString.encard_setOf_length_eq` for each exact length.
 * `Cslib.Kolmogorov.DescriptionMethod.encard_setOf_ecomplexity_lt`,
   `Cslib.Kolmogorov.DescriptionMethod.encard_setOf_etimeBoundedComplexity_lt`: fewer than `2 ^ r`
   objects have (time-bounded) complexity below `r`.
@@ -48,24 +46,6 @@ of length `n` have complexity below `n - c` [Li and Vitányi, Chapter 2][LiVitan
 
 namespace Cslib.Kolmogorov
 
-/-! ### Counting binary strings -/
-
-/-- There are `2 ^ n - 1` binary strings of length below `n`. -/
-theorem encard_setOf_length_lt_add_one (n : ℕ) :
-    {p : List Bool | p.length < n}.encard + 1 = 2 ^ n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    have hunion : {p : List Bool | p.length < n + 1} =
-        {p | p.length < n} ∪ {p | p.length = n} := by
-      ext p
-      simp only [Set.mem_ofPred_eq, Set.mem_union]
-      omega
-    have hdisj : Disjoint {p : List Bool | p.length < n} {p | p.length = n} :=
-      Set.disjoint_left.mpr fun _ hlt heq => Nat.ne_of_lt hlt heq
-    rw [hunion, Set.encard_union_eq hdisj, add_right_comm, ih, BitString.encard_setOf_length_eq,
-      pow_succ, mul_two]
-
 namespace DescriptionMethod
 
 variable {α : Type*} (M : DescriptionMethod α)
@@ -85,8 +65,10 @@ theorem encard_setOf_ecomplexity_lt (r : ℕ) : {x | M.ecomplexity x < r}.encard
     Set.encard_le_encard_of_injOn (fun _ hx => (hf hx).1)
       fun _ hx _ hy hxy => (hf hx).2.unique (hxy ▸ (hf hy).2)
   have htop : {p : List Bool | p.length < r}.encard ≠ ⊤ :=
-    ne_top_of_le_ne_top (by simp) (le_self_add.trans_eq (encard_setOf_length_lt_add_one r))
-  rw [← ENat.add_one_le_iff (ne_top_of_le_ne_top htop hle), ← encard_setOf_length_lt_add_one r]
+    ne_top_of_le_ne_top (by simp)
+      (le_self_add.trans_eq (BitString.encard_setOf_length_lt_add_one r))
+  rw [← ENat.add_one_le_iff (ne_top_of_le_ne_top htop hle),
+    ← BitString.encard_setOf_length_lt_add_one r]
   exact add_le_add_left hle 1
 
 /-- Fewer than `2 ^ r` objects have time-bounded complexity below `r`, for every time bound. -/