@ProvenHashes.uniformProb_mono : ∀ {K : Type u_1} [inst : Fintype K] {E D : K → Prop},
  (∀ (k : K), E k → D k) → ProvenHashes.uniformProb E ≤ ProvenHashes.uniformProb D
'ProvenHashes.uniformProb_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_or_le : ∀ {K : Type u_1} [inst : Fintype K] (E D : K → Prop),
  (ProvenHashes.uniformProb fun k => E k ∨ D k) ≤ ProvenHashes.uniformProb E + ProvenHashes.uniformProb D
'ProvenHashes.uniformProb_or_le' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_const : ∀ {K : Type u_1} [inst : Fintype K] [Nonempty K] (p : Prop) [inst_2 : Decidable p],
  (ProvenHashes.uniformProb fun x => p) = if p then 1 else 0
'ProvenHashes.uniformProb_const' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_prod : ∀ {K : Type u_1} {J : Type u_2} [inst : Fintype K] [inst_1 : Fintype J]
  (E : K × J → Prop), ProvenHashes.uniformProb E = (∑ k, ProvenHashes.uniformProb fun j => E (k, j)) / ↑(Fintype.card K)
'ProvenHashes.uniformProb_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_prod_fst : ∀ {K : Type u_1} {J : Type u_2} [inst : Fintype K] [inst_1 : Fintype J]
  [Nonempty J] (E : K → Prop), (ProvenHashes.uniformProb fun p => E p.1) = ProvenHashes.uniformProb E
'ProvenHashes.uniformProb_prod_fst' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_prod_le : ∀ {K : Type u_1} {J : Type u_2} [inst : Fintype K] [inst_1 : Fintype J] [Nonempty K]
  (E : K × J → Prop) (b : ℚ≥0),
  (∀ (k : K), (ProvenHashes.uniformProb fun j => E (k, j)) ≤ b) → ProvenHashes.uniformProb E ≤ b
'ProvenHashes.uniformProb_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.compose_collision_bound : ∀ {K : Type u_1} {J : Type u_2} {M : Type u_3} {R : Type u_4} [inst : Fintype K]
  [inst_1 : Fintype J] [Nonempty K] [Nonempty J] (s s' : K → M) (g : J → M → R) (a b : ℚ≥0),
  (ProvenHashes.uniformProb fun k => s k = s' k) ≤ a →
    (∀ (k : K), s k ≠ s' k → (ProvenHashes.uniformProb fun j => g j (s k) = g j (s' k)) ≤ b) →
      (ProvenHashes.uniformProb fun k => g k.2 (s k.1) = g k.2 (s' k.1)) ≤ a + b
'ProvenHashes.compose_collision_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.chainhash_equal_length_from_stages : ∀ {F : Type u_1} {K : Type u_2} {J : Type u_3} [inst : Field F]
  [inst_1 : Fintype F] [inst_2 : Fintype K] [inst_3 : Fintype J] [Nonempty K] [Nonempty J] (p : ℕ)
  (s s' : K → List (F × F)) (g : J → F → F),
  (∀ (k : K), (s k).length = (s' k).length) →
    (∀ (k : K), (s k).length ≤ p) →
      (ProvenHashes.uniformProb fun k => s k = s' k) ≤ 1 / ↑(Fintype.card F) →
        (∀ (v v' : F), v ≠ v' → (ProvenHashes.uniformProb fun j => g j v = g j v') ≤ 1 / ↑(Fintype.card F)) →
          (ProvenHashes.uniformProb fun k =>
              g k.2 (ProvenHashes.Recurrence.hash (s k.1.1) k.1.2) =
                g k.2 (ProvenHashes.Recurrence.hash (s' k.1.1) k.1.2)) ≤
            ↑(p + 2) / ↑(Fintype.card F)
'ProvenHashes.chainhash_equal_length_from_stages' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.chainhash_different_lengths_from_stages : ∀ {F : Type u_1} {K : Type u_2} {J : Type u_3} [inst : Field F]
  [inst_1 : Fintype F] [inst_2 : Fintype K] [inst_3 : Fintype J] [Nonempty K] [Nonempty J] (p : ℕ)
  (s s' : K → List (F × F)) (g : J → F → F),
  (∀ (k : K), (s k).length ≠ (s' k).length) →
    (∀ (k : K), max (s k).length (s' k).length ≤ p) →
      (∀ (v v' : F), v ≠ v' → (ProvenHashes.uniformProb fun j => g j v = g j v') ≤ 1 / ↑(Fintype.card F)) →
        (ProvenHashes.uniformProb fun k =>
            g k.2 (ProvenHashes.Recurrence.hash (s k.1.1) k.1.2) =
              g k.2 (ProvenHashes.Recurrence.hash (s' k.1.1) k.1.2)) ≤
          ↑(p + 2) / ↑(Fintype.card F)
'ProvenHashes.chainhash_different_lengths_from_stages' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.seed_monic : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  (ProvenHashes.Recurrence.encode m).seed.Monic
'ProvenHashes.Recurrence.seed_monic' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.seed_degree : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  (ProvenHashes.Recurrence.encode m).seed.natDegree = m.length
'ProvenHashes.Recurrence.seed_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.seed_top : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  (ProvenHashes.Recurrence.encode m).seed.coeff m.length = 1
'ProvenHashes.Recurrence.seed_top' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.data_coeff_zero : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)) (k : ℕ),
  m.length ≤ k → (ProvenHashes.Recurrence.encode m).data.coeff k = 0
'ProvenHashes.Recurrence.data_coeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.shift_coeff_zero : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)) (k : ℕ),
  m.length < k → (ProvenHashes.Recurrence.encode m).shift.coeff k = 0
'ProvenHashes.Recurrence.shift_coeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.shift_top : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  (ProvenHashes.Recurrence.encode m).shift.coeff m.length = if m.length = 0 then 0 else 1
'ProvenHashes.Recurrence.shift_top' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.head_a : ∀ {F : Type u_1} [inst : Field F] (a b : F) (m : List (F × F)),
  (ProvenHashes.Recurrence.encode ((a, b) :: m)).data.coeff m.length = a
'ProvenHashes.Recurrence.head_a' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.head_b : ∀ {F : Type u_1} [inst : Field F] (a b : F) (m : List (F × F)),
  ProvenHashes.Recurrence.headB m.length (ProvenHashes.Recurrence.encode ((a, b) :: m)) = b
'ProvenHashes.Recurrence.head_b' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.peel_encode : ∀ {F : Type u_1} [inst : Field F] (a b : F) (m : List (F × F)),
  ProvenHashes.Recurrence.peel m.length (ProvenHashes.Recurrence.encode ((a, b) :: m)) =
    ProvenHashes.Recurrence.encode m
'ProvenHashes.Recurrence.peel_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.decode_encode : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  ProvenHashes.Recurrence.decode m.length (ProvenHashes.Recurrence.encode m) = m
'ProvenHashes.Recurrence.decode_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.encode_injective : ∀ {F : Type u_1} [inst : Field F],
  Function.Injective ProvenHashes.Recurrence.encode
'ProvenHashes.Recurrence.encode_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.same_bucket_close : ∀ {r s B : ℕ}, 0 < B → r / B = s / B → r < s + B ∧ s < r + B
'ProvenHashes.same_bucket_close' depends on axioms: [propext, Classical.choice, Quot.sound]
ProvenHashes.multiplyShift_collision_close : ∀ (w ℓ : ℕ) (a : ProvenHashes.OddMultiplier w) (x y : Fin (2 ^ w)),
  ProvenHashes.multiplyShift w ℓ a x = ProvenHashes.multiplyShift w ℓ a y →
    ↑↑a * ↑x % 2 ^ (2 * w) < ↑↑a * ↑y % 2 ^ (2 * w) + 2 ^ (2 * w - ℓ) ∧
      ↑↑a * ↑y % 2 ^ (2 * w) < ↑↑a * ↑x % 2 ^ (2 * w) + 2 ^ (2 * w - ℓ)
'ProvenHashes.multiplyShift_collision_close' depends on axioms: [propext, Classical.choice, Quot.sound]
ProvenHashes.odd_mul_mod_injective : ∀ (N a : ℕ), Odd a → Function.Injective fun x => a * ↑x % 2 ^ N
'ProvenHashes.odd_mul_mod_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.affine_bijective : ∀ {F : Type u_1} [inst : Field F] (a b : F),
  a ≠ 0 → Function.Bijective fun v => a * v + b
'ProvenHashes.affine_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.sum_mul_update : ∀ {I : Type u_1} {F : Type u_2} [inst : Fintype I] [inst_1 : DecidableEq I]
  [inst_2 : Field F] (c k : I → F) (i : I) (v : F),
  ∑ j, c j * Function.update k i v j = c i * v + ∑ j ∈ Finset.univ.erase i, c j * k j
'ProvenHashes.sum_mul_update' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.affine_sum_uniform : ∀ {I : Type u_1} {F : Type u_2} [inst : Fintype I] [inst_1 : DecidableEq I]
  [inst_2 : Field F] [inst_3 : Fintype F] (c : I → F) (d : F),
  (∃ i, c i ≠ 0) → ∀ (t : F), (ProvenHashes.uniformProb fun k => d + ∑ i, c i * k i = t) = 1 / ↑(Fintype.card F)
'ProvenHashes.affine_sum_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.nh_difference : ∀ {F : Type u_1} [inst : Field F] {n : ℕ} (m m' k : Fin n × Bool → F),
  ProvenHashes.nhHash m k - ProvenHashes.nhHash m' k =
    ProvenHashes.nhConstant m m' + ∑ j, ProvenHashes.nhCoefficient m m' j * k j
'ProvenHashes.nh_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.nh_difference_uniform : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {n : ℕ}
  (m m' : Fin n × Bool → F),
  m ≠ m' →
    ∀ (t : F),
      (ProvenHashes.uniformProb fun k => ProvenHashes.nhHash m k - ProvenHashes.nhHash m' k = t) = 1 / ↑(Fintype.card F)
'ProvenHashes.nh_difference_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.nh_collision_bound : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {n : ℕ}
  (m m' : Fin n × Bool → F),
  m ≠ m' →
    (ProvenHashes.uniformProb fun k => ProvenHashes.nhHash m k = ProvenHashes.nhHash m' k) ≤ 1 / ↑(Fintype.card F)
'ProvenHashes.nh_collision_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.polynomialHash_eq_eval : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {n : ℕ}
  (m : Fin n → F) (x : F), ProvenHashes.polynomialHash m x = Polynomial.eval x ((Polynomial.ofFn n) m)
'ProvenHashes.polynomialHash_eq_eval' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.polynomial_zero_count : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F]
  (p : Polynomial F), p ≠ 0 → {x | Polynomial.eval x p = 0}.card ≤ p.natDegree
'ProvenHashes.polynomial_zero_count' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.polynomial_collision_bound : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {n L : ℕ},
  n ≤ L →
    ∀ (m m' : Fin n → F),
      m ≠ m' →
        (ProvenHashes.uniformProb fun x => ProvenHashes.polynomialHash m x = ProvenHashes.polynomialHash m' x) ≤
          ↑(L - 1) / ↑(Fintype.card F)
'ProvenHashes.polynomial_collision_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ProvenHashes.polynomial_collision_zmod : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {n L : ℕ},
  n ≤ L →
    ∀ (m m' : Fin n → ZMod p),
      m ≠ m' →
        (ProvenHashes.uniformProb fun x => ProvenHashes.polynomialHash m x = ProvenHashes.polynomialHash m' x) ≤
          ↑(L - 1) / ↑p
'ProvenHashes.polynomial_collision_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
ProvenHashes.gf64_card : Fintype.card (GaloisField 2 64) = 2 ^ 64
'ProvenHashes.gf64_card' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.polynomial_collision_gf64 : ∀ {n L : ℕ},
  n ≤ L →
    ∀ (m m' : Fin n → GaloisField 2 64),
      m ≠ m' →
        (ProvenHashes.uniformProb fun x => ProvenHashes.polynomialHash m x = ProvenHashes.polynomialHash m' x) ≤
          ↑(L - 1) / 2 ^ 64
'ProvenHashes.polynomial_collision_gf64' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_equiv : ∀ {K : Type u_1} {J : Type u_2} [inst : Fintype K] [inst_1 : Fintype J] (e : K ≃ J)
  (event : J → Prop), (ProvenHashes.uniformProb fun k => event (e k)) = ProvenHashes.uniformProb event
'ProvenHashes.uniformProb_equiv' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_fst : ∀ {A : Type u_1} {B : Type u_2} [inst : Fintype A] [inst_1 : Fintype B] [Nonempty A]
  [Nonempty B] (t : A), (ProvenHashes.uniformProb fun p => p.1 = t) = 1 / ↑(Fintype.card A)
'ProvenHashes.uniformProb_fst' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_of_bijective_slices : ∀ {A : Type u_1} {R : Type u_2} [inst : Fintype A] [inst_1 : Fintype R]
  [Nonempty A] [Nonempty R] (f : A × R → A),
  (∀ (r : R), Function.Bijective fun a => f (a, r)) →
    ∀ (t : A), (ProvenHashes.uniformProb fun k => f k = t) = 1 / ↑(Fintype.card A)
'ProvenHashes.uniformProb_of_bijective_slices' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.uniformProb_of_bijective_update : ∀ {I : Type u_1} {V : Type u_2} [inst : Fintype I] [inst_1 : Fintype V]
  [Nonempty V] [inst_3 : DecidableEq I] (f : (I → V) → V) (i : I),
  (∀ (k : I → V), Function.Bijective fun v => f (Function.update k i v)) →
    ∀ (t : V), (ProvenHashes.uniformProb fun k => f k = t) = 1 / ↑(Fintype.card V)
'ProvenHashes.uniformProb_of_bijective_update' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.slice_lift : ∀ {F : Type u_1} [inst : Field F] (u z : F) (p : Polynomial F),
  (ProvenHashes.Recurrence.slice u z) (ProvenHashes.Recurrence.liftY p) = p
'ProvenHashes.Recurrence.slice_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.slice_X : ∀ {F : Type u_1} [inst : Field F] (u z : F) (i : Fin 3),
  (ProvenHashes.Recurrence.slice u z) (MvPolynomial.X i) = ![Polynomial.C u, Polynomial.X, Polynomial.C z] i
'ProvenHashes.Recurrence.slice_X' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.extract_keyPolynomial : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  ProvenHashes.Recurrence.extract (ProvenHashes.Recurrence.keyPolynomial m) = ProvenHashes.Recurrence.encode m
'ProvenHashes.Recurrence.extract_keyPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.decode_keyPolynomial : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  ProvenHashes.Recurrence.decodePolynomial (ProvenHashes.Recurrence.keyPolynomial m) = m
'ProvenHashes.Recurrence.decode_keyPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.keyPolynomial_injective : ∀ {F : Type u_1} [inst : Field F],
  Function.Injective ProvenHashes.Recurrence.keyPolynomial
'ProvenHashes.Recurrence.keyPolynomial_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.keyCoefficients_injective : ∀ {F : Type u_1} [inst : Field F],
  Function.Injective fun m d => MvPolynomial.coeff d (ProvenHashes.Recurrence.keyPolynomial m)
'ProvenHashes.Recurrence.keyCoefficients_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.fold_expansion : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)) (u y z : F),
  List.foldl (fun p ab => ab.1 + (ab.2 + y) * (p + u)) z m =
    Polynomial.eval y (ProvenHashes.Recurrence.encode m).data +
        z * Polynomial.eval y (ProvenHashes.Recurrence.encode m).seed +
      u * Polynomial.eval y (ProvenHashes.Recurrence.encode m).shift
'ProvenHashes.Recurrence.fold_expansion' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.eval_lift : ∀ {F : Type u_1} [inst : Field F] (k : Fin 3 → F) (p : Polynomial F),
  (MvPolynomial.eval k) (ProvenHashes.Recurrence.liftY p) = Polynomial.eval (k 1) p
'ProvenHashes.Recurrence.eval_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.eval_keyPolynomial : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)) (k : Fin 3 → F),
  (MvPolynomial.eval k) (ProvenHashes.Recurrence.keyPolynomial m) = ProvenHashes.Recurrence.hash m k
'ProvenHashes.Recurrence.eval_keyPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.lift_degree : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F),
  (ProvenHashes.Recurrence.liftY p).totalDegree ≤ p.natDegree
'ProvenHashes.Recurrence.lift_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.component_difference_degrees : ∀ {F : Type u_1} [inst : Field F] (m m' : List (F × F)),
  m.length = m'.length →
    ((ProvenHashes.Recurrence.encode m).data - (ProvenHashes.Recurrence.encode m').data).natDegree ≤ m.length - 1 ∧
      ((ProvenHashes.Recurrence.encode m).seed - (ProvenHashes.Recurrence.encode m').seed).natDegree ≤ m.length - 1 ∧
        ((ProvenHashes.Recurrence.encode m).shift - (ProvenHashes.Recurrence.encode m').shift).natDegree ≤ m.length - 1
'ProvenHashes.Recurrence.component_difference_degrees' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.keyPolynomial_difference_degree : ∀ {F : Type u_1} [inst : Field F] (m m' : List (F × F)),
  m.length = m'.length →
    0 < m.length →
      (ProvenHashes.Recurrence.keyPolynomial m - ProvenHashes.Recurrence.keyPolynomial m').totalDegree ≤ m.length
'ProvenHashes.Recurrence.keyPolynomial_difference_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.collision_bound : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] (m m' : List (F × F)),
  m.length = m'.length →
    m ≠ m' →
      (ProvenHashes.uniformProb fun k => ProvenHashes.Recurrence.hash m k = ProvenHashes.Recurrence.hash m' k) ≤
        ↑m.length / ↑(Fintype.card F)
'ProvenHashes.Recurrence.collision_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ProvenHashes.Recurrence.collision_bound_gf64 : ∀ (m m' : List (GaloisField 2 64 × GaloisField 2 64)),
  m.length = m'.length →
    m ≠ m' →
      (ProvenHashes.uniformProb fun k => ProvenHashes.Recurrence.hash m k = ProvenHashes.Recurrence.hash m' k) ≤
        ↑m.length / 2 ^ 64
'ProvenHashes.Recurrence.collision_bound_gf64' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.keyPolynomial_degree : ∀ {F : Type u_1} [inst : Field F] (m : List (F × F)),
  (ProvenHashes.Recurrence.keyPolynomial m).totalDegree ≤ m.length + 1
'ProvenHashes.Recurrence.keyPolynomial_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.Recurrence.collision_bound_any_length : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F]
  (m m' : List (F × F)),
  m ≠ m' →
    (ProvenHashes.uniformProb fun k => ProvenHashes.Recurrence.hash m k = ProvenHashes.Recurrence.hash m' k) ≤
      ↑(max m.length m'.length + 1) / ↑(Fintype.card F)
'ProvenHashes.Recurrence.collision_bound_any_length' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.tabulation_difference_uniform : ∀ {I : Type u_1} {A : Type u_2} {G : Type u_3} [inst : Fintype I]
  [inst_1 : Fintype A] [inst_2 : DecidableEq I] [inst_3 : DecidableEq A] [inst_4 : AddCommGroup G] [inst_5 : Fintype G]
  (x x' : I → A),
  x ≠ x' →
    ∀ (t : G),
      (ProvenHashes.uniformProb fun T => ProvenHashes.tabulationHash x T - ProvenHashes.tabulationHash x' T = t) =
        1 / ↑(Fintype.card G)
'ProvenHashes.tabulation_difference_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
@ProvenHashes.tabulation_collision_exact : ∀ {I : Type u_1} {A : Type u_2} [inst : Fintype I] [inst_1 : Fintype A]
  [inst_2 : DecidableEq I] [inst_3 : DecidableEq A] (w : ℕ) (x x' : I → A),
  x ≠ x' →
    (ProvenHashes.uniformProb fun T => ProvenHashes.tabulationHash x T = ProvenHashes.tabulationHash x' T) = 1 / 2 ^ w
'ProvenHashes.tabulation_collision_exact' depends on axioms: [propext, Classical.choice, Quot.sound]