Trace — 2607.19337v1

$ /bin/bash -lc "ls -la /work && find /work -maxdepth 2 -type f -printf '%p %s bytes
' | sort | head -80"
total 312
drwxr-xr-x  6 root root   4096 Jul 23 12:18 .
drwxr-xr-x 20 root root   4096 Jul 23 12:16 ..
dr-xr-xr-x  2 root root     40 Jul 23 12:18 .agents
dr-xr-xr-x  2 root root     40 Jul 23 12:18 .codex
drwxr-xr-x  7 root root   4096 Jul 23 12:17 .git
-rw-r--r--  1 root root   3210 Jul 23 12:16 PROMPT.txt
-rw-r--r--  1 root root   1211 Jul 23 12:18 codex-events.jsonl
-rw-r--r--  1 root root   5083 Jul 23 12:18 codex.err
-rw-r--r--  1 root root    621 Jul 23 12:16 paper.json
-rw-r--r--  1 root root 270092 Jul 23 12:16 paper.pdf
-rw-r--r--  1 root root   9297 Jul 23 12:16 paper.txt
drwxr-xr-x 17 root root   4096 Jul 23 12:16 repro
/work/.git/HEAD 23 bytes
/work/.git/config 147 bytes
/work/.git/description 73 bytes
/work/PROMPT.txt 3210 bytes
/work/codex-events.jsonl 1211 bytes
/work/codex.err 5083 bytes
/work/paper.json 621 bytes
/work/paper.pdf 270092 bytes
/work/paper.txt 9297 bytes
/work/repro/.git-blame-ignore-revs 401 bytes
/work/repro/.gitignore 440 bytes
/work/repro/.gitpod.yml 155 bytes
/work/repro/.pre-commit-config.yaml 419 bytes
/work/repro/Archive.lean 2901 bytes
/work/repro/CITATION.md 677 bytes
/work/repro/CODE_OF_CONDUCT.md 5319 bytes
/work/repro/Counterexamples.lean 1261 bytes
/work/repro/LICENSE 11357 bytes
/work/repro/Mathlib.lean 452322 bytes
/work/repro/README.md 8936 bytes
/work/repro/bors.toml 1857 bytes
/work/repro/docs.lean 53 bytes
/work/repro/lake-manifest.json 2815 bytes
/work/repro/lakefile.lean 6816 bytes
/work/repro/lean-toolchain 29 bytes

$ /bin/bash -lc "sed -n '1,260p' paper.txt"
On the A-transcendence of a Champernowne-type constant
Shin-ichiro Seki

arXiv:2607.19337v1 [math.NT] 21 Jul 2026

Abstract. Let pn denote the n-th prime. We prove that for every nonzero polynomial f (x) ∈ Z[x],
there exist infinitely many positive integers n such that pn ∤ f (n).

1. Introduction
Let pn denote the n-th prime. In this note, we prove the following.
Theorem 1.1. For every nonzero polynomial f (x) ∈ Z[x], we have
#{n ∈ Z>0 : pn ∤ f (n)} = ∞.
This theorem can be reformulated as a statement concerning the transcendence of a certain
element of the ring
!,
!
Y
M
A :=
Z/pZ
Z/pZ .
p: prime

p: prime

0 denote the set of all finite algebraic numbers introduced by Rosen in [4]. Let C be
Let PA
A
0 ⊊ C ⊊ A hold. In the ring
the integral closure of Q in A. Then the strict inclusions Q ⊊ PA
A

A, two notions of transcendence have been studied: transcendence in the sense of not belonging
0 , and transcendence in the sense of not belonging to C . Let α = (a mod p) ∈ A. It is
to PA
p
p
A
easy to see that if ap → ∞ as p → ∞ and ap grows more slowly than every positive power of p,
then α is transcendental in the stronger sense ([2, Lemma 2.3]); that is, α ∈
/ CA . For example,
(⌊log p⌋ mod p)p ∈
/ CA ([2, Example 2.4]). Here, ⌊X⌋ denotes the greatest integer less than or equal
to X. In contrast, the following criterion, established by Luca and Zudilin using a prime-counting
argument, makes it possible to prove transcendence even when ap grows substantially faster.
Lemma 1.2 (Luca–Zudilin’s second criterion [1], [2, Lemma 2.5]). Let α = (ap mod p)p ∈ A.
Let g(X) and h(X) be positive-valued, monotonically increasing functions satisfying g(X) log X =
o(h(X)) as X → ∞. Let S be an infinite set of primes, and let (bp )p∈S be a sequence of integers
satisfying bp → ∞ and bp = O(g(p)) as p → ∞. Suppose that ap ≡ bp (mod p) for all p ∈ S.
Assume further that #{p ≤ X : p ∈ S} ≫ h(X) for all sufficiently large X. Then α ∈
/ CA .
Although this formulation allows more general grow

$ /bin/bash -lc "sed -n '261,520p' paper.txt"
d X
d−1
k
X
(−1)v bu (n) X
u=0 v=0

pv+1
n

cj j u hvj = 0.

j=0

Therefore, we obtain
k

(−hj )d
Φ(n, pn ) X
=
= O(nd /pd+1
cj f (n + j) d
n ) = o(1)
ρ(pn )
pn (pn + hj )

as n → ∞.

j=0

Here, the implied constant depends only on f , (hj )j , and (cj )j , and is independent of n. Combining
this with (2.4), we conclude that
Φ(n, pn ) = 0
for all sufficiently large n ∈ M . This contradicts (2.3).
References
[1] F. Luca, W. Zudilin, Poor man’s transcendence for Frobenius traces of elliptic curves, to appear in Advanced
Studies in Pure Math.
[2] T. Matsusaka, S. Seki, Some results on naive transcendence in the ring of integers modulo infinitely large primes,
to appear in J. Aust. Math. Soc.
[3] J. Maynard, Small gaps between primes, Ann. of Math. 181 (2015), 383–413.
[4] J. Rosen, A finite analogue of the ring of algebraic numbers, J. Number Theory 208 (2020), 59–71.
Nagahama Institute of Bio-Science and Technology, 1266, Tamura, Nagahama, Shiga, 526-0829,
Japan
Email address: s seki@nagahama-i-bio.ac.jp

4

$ /bin/bash -lc 'rg -n "nth[Pp]rime|nth.*prime|prime.*asympt|Prime.*asympt|primeCounting|prime_counting|PrimeCounting|pi.*asympt" Mathlib | head -240'
Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean:135:lemma nthRootsFinset_pairwise_associated_sub_one_sub_of_prime (hζ : IsPrimitiveRoot ζ p)
Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean:151:  nthRootsFinset_pairwise_associated_sub_one_sub_of_prime
Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean:161:  · exact (hζ.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:36:* `nthRootsFinset_eq_of_prime`: for `p` prime, the `p`-th roots of unity are the primitive `p`-th
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:843:theorem nthRootsFinset_eq_of_prime [DecidableEq R] (hp : p.Prime) :
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:849:theorem mem_nthRootsFinset_iff_of_prime (hp : p.Prime) {η : R} :
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:852:  simp [nthRootsFinset_eq_of_prime hp, mem_primitiveRoots hp.pos, or_comm]
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:857:  ((mem_nthRootsFinset_iff_of_prime hp).1 hη).resolve_right hne1
Mathlib/Data/Nat/Prime/Nth.lean:20:theorem nth_prime_zero_eq_two : nth Prime 0 = 2 := nth_count prime_two
Mathlib/Data/Nat/Prime/Nth.lean:23:theorem nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three
Mathlib/Data/Nat/Prime/Nth.lean:26:theorem nth_prime_two_eq_five : nth Nat.Prime 2 = 5 := nth_count prime_five
Mathlib/Data/Nat/Prime/Nth.lean:29:theorem nth_prime_three_eq_seven : nth Nat.Prime 3 = 7 := nth_count prime_seven
Mathlib/Data/Nat/Prime/Nth.lean:32:theorem nth_prime_four_eq_eleven : nth Nat.Prime 4 = 11 := nth_count prime_eleven
Mathlib/Data/Nat/Choose/Factorization.lean:174:  nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]
Mathlib/Data/Nat/Factorization/Basic.lean:504:  nth_rw 1 [← Finset.prod_pow, prod_primeFactors_pow_factorization hn]
Mathlib/Data/Nat/Factors.lean:243:  nth_rw 1 [← Nat.prod_primeFactorsList ha]
Mathlib/NumberTheory/Primorial.lean:12:public import Mathlib

$ /bin/bash -lc "sed -n '1,130p' Mathlib/Data/Nat/Prime/Nth.lean && sed -n '780,865p' Mathlib/NumberTheory/Chebyshev.lean && rg -n \"nth.*StrictMono|strictMono.*nth|nth_strictMono\" Mathlib/Data/Nat Mathlib | head -80"
/-
Copyright (c) 2024 Ralf Stephan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ralf Stephan
-/
module

public import Mathlib.Data.Nat.Prime.Defs
public import Mathlib.Data.Nat.Nth

/-!
# The Nth primes
-/

public section

namespace Nat

@[simp]
theorem nth_prime_zero_eq_two : nth Prime 0 = 2 := nth_count prime_two

@[simp]
theorem nth_prime_one_eq_three : nth Nat.Prime 1 = 3 := nth_count prime_three

@[simp]
theorem nth_prime_two_eq_five : nth Nat.Prime 2 = 5 := nth_count prime_five

@[simp]
theorem nth_prime_three_eq_seven : nth Nat.Prime 3 = 7 := nth_count prime_seven

@[simp]
theorem nth_prime_four_eq_eleven : nth Nat.Prime 4 = 11 := nth_count prime_eleven

end Nat
  case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

theorem integral_theta_div_log_sq_isLittleO :
    (fun x ↦ ∫ t in 2..x, θ t / (t * log t ^ 2)) =o[atTop] (fun x ↦ x / log x) := by
  refine integral_theta_div_log_sq_isBigO.trans_isLittleO ?_
  refine isLittleO_iff_tendsto' (by simp) |>.mpr ?_
  refine Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop
  filter_upwards [eventually_gt_atTop 0] with x _
  field

theorem primeCounting_sub_theta_div_log_isBigO :
    (fun x ↦ π ⌊x⌋₊ - θ x / log x) =O[atTop] (fun x ↦ x / log x ^ 2) := by
  apply integral_theta_div_log_sq_isBigO.congr' _ (by rfl)
  filter_upwards [eventually_ge_atTop 2] with x hx
  rw [primeCounting_eq_theta_div_log_add_integral hx]
  simp

/-- Chebyshev's upper bound on the prime counting function -/
theorem eventually_primeCounting_le {ε : ℝ} (εpos : 0 < ε) :
    ∀ᶠ x in atTop, π ⌊x⌋₊ ≤ (log 4 + ε) * x / log x := by
  have := integral_theta_div_log_sq_isLittleO.bound εpos
  filter_upwards [eventually_ge_atTop 2, this] with x hx hx2
  rw [primeCounting_eq_theta

$ /bin/bash -lc 'rg -n -i "prime number theorem|prime_number_theorem|primeNumberTheorem|tendsto.*primeCounting|primeCounting.*isEquivalent|asymptotic.*prime" Mathlib | head -200 && rg -n "Fintype.*LinearMap.*ker|finrank_ker|exists_ne_zero.*map|nontrivial.*kernel|finrank.*lt.*ker" Mathlib/LinearAlgebra | head -160'
Mathlib/NumberTheory/LSeries/Nonvanishing.lean:25:These results are prerequisites for the **Prime Number Theorem** and
Mathlib/NumberTheory/PrimeCounting.lean:97:theorem tendsto_primeCounting' : Tendsto π' atTop atTop := by
Mathlib/NumberTheory/PrimeCounting.lean:98:  apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
Mathlib/NumberTheory/PrimeCounting.lean:101:theorem tendsto_primeCounting : Tendsto π atTop atTop :=
Mathlib/NumberTheory/PrimeCounting.lean:102:  (tendsto_add_atTop_iff_nat 1).mpr tendsto_primeCounting'
Mathlib/NumberTheory/Chebyshev.lean:60:Parts of this file were upstreamed from the PrimeNumberTheoremAnd project by Kontorovich et al, https://github.com/alexKontorovich/PrimeNumberTheoremAnd.
Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean:107:      apply LinearMap.finrank_range_add_finrank_ker
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean:278:      LinearMap.finrank_range_add_finrank_ker]
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:173:theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:181:  have h₁ := f.finrank_range_add_finrank_ker
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:200:  have := finrank_range_add_finrank_ker f
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:415:        apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker
Mathlib/LinearAlgebra/Span/Basic.lean:454:  have ⟨_, ⟨m, hm, rfl⟩, ne⟩ := LinearMap.exists_ne_zero_of_sSup_eq_top h (comap N.subtype '' s) <|
Mathlib/LinearAlgebra/Matrix/Rank.lean:441:  · simp only [LinearMap.finrank_range_add_finrank_ker]
Mathlib/LinearAlgebra/Matrix/Rank.lean:481:  · simp only [LinearMap.finrank_range_add_finrank_ker]
Mathlib/LinearAlgebra/Matrix/Rank.lean:518:      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean:249:  simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]
Mathlib/LinearAlgeb

$ /bin/bash -lc 'git clone --depth 1 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /tmp/pnt-project && rg -n "theorem.*primeCounting|primeCounting.*~|IsEquivalent.*prime|PNT|prime_number_theorem|PrimeNumberTheorem" /tmp/pnt-project/PrimeNumberTheoremAnd | head -240'
/tmp/pnt-project/PrimeNumberTheoremAnd/MellinCalculus.lean:8:import PrimeNumberTheoremAnd.Auxiliary
/tmp/pnt-project/PrimeNumberTheoremAnd/BorelCaratheodory.lean:10:import PrimeNumberTheoremAnd.StrongPNT
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:3:import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:4:import PrimeNumberTheoremAnd.Defs
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:5:import PrimeNumberTheoremAnd.Wiener
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:85:theorem WeakPNT' : Tendsto (fun N ↦ (∑ n ∈ Iic N, Λ n) / N) atTop (nhds 1) := by
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:94:  apply Tendsto.add WeakPNT
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:104:/-- An alternate form of the Weak PNT. -/
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:105:theorem WeakPNT'' : ψ ~[atTop] (fun x ↦ x) := by
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:110:      · convert! Tendsto.comp WeakPNT' tendsto_nat_floor_atTop
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:178:  refine WeakPNT''.add_isLittleO'' (IsBigO.trans_isLittleO (g := fun x ↦ 2 * x.sqrt * x.log) ?_ ?_)
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:901:    (fun (x : ℝ) ↦ (primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / log x) := by
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:937:    apply IsEquivalent.congr_right (v := (fun n ↦ log (nth_prime n) - log (log (nth_prime n))))
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:1726:      simpa [Psi] using! WeakPNT''
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:1951:  (proofUses := ["WeakPNT", "mun"])
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:2433:\section{Consequences of the PNT in arithmetic progressions}
/tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean:2455:    have hW := WeakPNT_AP hq ha ha'
/tmp/pnt-project/PrimeNumberTheorem

$ /bin/bash -lc "sed -n '880,960p' /tmp/pnt-project/PrimeNumberTheoremAnd/Consequences.lean && sed -n '1,80p' /tmp/pnt-project/lakefile.toml && cat /tmp/pnt-project/lean-toolchain && cat lean-toolchain"
· apply IsLittleO.congr' (f₁ := (fun x ↦ f x + f x * f' x + f' x)) _ _ (by rfl)
    · apply IsLittleO.add _ hf'
      apply IsLittleO.add hf
      convert! hf.mul hf'
      ring
    · filter_upwards [eventually_ge_atTop 2, h, h'] with x hx h h'
      rw [h, intervalIntegral.integral_of_le hx, ← integral_Icc_eq_integral_Ioc, h']
      have : log x ≠ 0 := by simp; grind
      field
  · intro x
    obtain rfl|hx := eq_or_ne x 0
    · simp
    obtain rfl|hx := eq_or_ne x 1
    · simp
    obtain rfl|hx := eq_or_ne x (-1 : ℝ)
    · simp
      norm_num
    have : log x ≠ 0 := by simp_all
    field

theorem pi_alt' :
    (fun (x : ℝ) ↦ (primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / log x) := by
  obtain ⟨f, ⟨hf1, hf2⟩⟩ := pi_alt
  simp_rw [hf2, IsEquivalent]
  have : ((fun x ↦ (1 + f x) * x / log x) - fun x ↦ x / log x) =
      (fun x ↦ f x * x / log x) := by
    ext
    simp
    ring
  rw [this]
  convert hf1.mul_isBigO (f₂ := (fun x ↦ x / log x)) (g₂ := (fun x ↦ x /log x))
      (isBigO_refl ..) using 2
  all_goals first | ring | rfl


lemma pi_nth_prime (n : ℕ) :
    primeCounting (nth_prime n) = n + 1 := by
  rw [primeCounting, primeCounting', count_nth_succ_of_infinite infinite_setOf_prime]

lemma tendsto_nth_prime_atTop : Tendsto nth_prime atTop atTop :=
  nth_strictMono infinite_setOf_prime |>.tendsto_atTop

lemma pi_nth_prime_asymp :
    (fun n ↦ (nth_prime n) / (log (nth_prime n))) ~[atTop] (fun (n : ℕ) ↦ (n : ℝ)) := by
  trans (fun (n : ℕ) ↦ ( n + 1 : ℝ))
  · have : Tendsto (fun n ↦ ((nth_prime n) : ℝ)) atTop atTop := by
      apply tendsto_natCast_atTop_iff.mpr tendsto_nth_prime_atTop
    convert! pi_alt'.comp_tendsto this |>.symm
    simp only [Function.comp_apply, floor_natCast]
    rw [pi_nth_prime]
    norm_cast
  · apply IsEquivalent.add_isLittleO (by rfl)
    exact isLittleO_const_id_atTop (1 : ℝ) |>.natCast_atTop

lemma log_nth_prime_asymp : (fun n ↦ log (nth_prime n)) ~[atTop] (fun n ↦ log n) := by
  have := pi_nth_prime_asymp.log tendsto_natCast_atTop_a

$ /bin/bash -lc 'rg -n "exists.*mulVec.*zero|mulVec.*eq_zero.*exists|rank.*lt.*exists|nontrivial.*ker|finrank.*domain|finrank.*codomain" Mathlib/LinearAlgebra/Matrix Mathlib/LinearAlgebra | head -240 && rg -n "Fintype.card.*finrank|finrank_fun|finrank_pi|finrank_fin" Mathlib/LinearAlgebra | head -120'
Mathlib/LinearAlgebra/Determinant.lean:353:  obtain ⟨v, hv_ne_zero, hv_zero⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr (det_toMatrix b f ▸ hf)
Mathlib/LinearAlgebra/Determinant.lean:365:    rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:27:* `Matrix.exists_mulVec_eq_zero_iff`: `M` maps some `v ≠ 0` to zero iff `det M = 0`
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:109:/-- This holds for all integral domains (see `Matrix.exists_mulVec_eq_zero_iff`),
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:111:private theorem exists_mulVec_eq_zero_iff_aux {K : Type*} [DecidableEq n] [Field K]
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:127:private theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [CommRing A]
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:131:    exists_mulVec_eq_zero_iff_aux
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:163:theorem exists_mulVec_eq_zero_iff [DecidableEq n] : (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 :=
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:164:  exists_mulVec_eq_zero_iff' (FractionRing A)
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:167:  simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:170:  grind [nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero, exists_mulVec_eq_zero_iff,
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:177:  grind [separatingRight_iff_forall_mulVec_eq_zero, exists_mulVec_eq_zero_iff]
Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean:676:  Iff.trans separatingLeft_iff_linear_nontrivial LinearMap.ker_eq_bot'.symm
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:27:* `Matrix.exists_mulVec_eq_zero_iff`: `M` maps some `v ≠ 0` to zero iff `det M = 0`
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:109:/-- This holds for all integral domains (see `Matrix.exists_mulVec_eq_zero_iff`),
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean:111:private theorem e

$ /bin/bash -lc 'rg -n "card.*finrank.*LinearIndependent|LinearIndependent.*card.*finrank|not_linearIndependent.*finrank|finrank.*linearIndependent" Mathlib/LinearAlgebra Mathlib | head -200'
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:260:theorem LinearIndependent.span_eq_top_of_card_eq_finrank' [FiniteDimensional K V] {b : ι → V}
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:261:    (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:267:theorem LinearIndependent.span_eq_top_of_card_eq_finrank [Nonempty ι]
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:287:    {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:293:    {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:319:    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) : Basis s K V :=
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:325:    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:333:    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:339:    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
Mathlib/LinearAlgebra/Matrix/Rank.lean:506:  rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]
Mathlib/LinearAlgebra/Dimension/Finite.lean:302:    (mt LinearIndependent.finset_card_le_finrank h.not_ge)
Mathlib/LinearAlgebra/Dimension/OrzechProperty.lean:43:    LinearIndependent R b ↔ Fintype.card ι = (Set.range b).finrank R where
Mathlib/LinearAlgebra/Dimension/OrzechProperty.lean:52:    LinearIndependent R b ↔ Fintype.card ι ≤ (Set.range b).finrank R := by
Mathlib/FieldTheory/Galois/NormalBasis.lean:47:    (AdjoinRoot.powerBasis (X_pow_sub_C_ne_zero Module.finrank_pos 1)).basis.linearIndependent
Mathlib/LinearAlgebra/FiniteDimensional/Lemm

$ /bin/bash -lc 'rg -n "ker_ne_bot.*finrank|finrank_lt.*ker|finrank.*lt.*finrank.*ker|not_injective.*finrank|finrank_lt.*not.*Injective|injective.*finrank" Mathlib/LinearAlgebra | head -220'
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:178:lemma ker_ne_bot_of_finrank_lt [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:197:theorem injective_iff_surjective_of_finrank_eq_finrank [FiniteDimensional K V]
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:210:  rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:218:    ⟨hf, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp hf⟩
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean:415:        apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean:82:        rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean:276:  toSubmodule_injective <| Submodule.eq_of_le_of_finrank_le h_le h_finrank
Mathlib/LinearAlgebra/Matrix/Rank.lean:436:  refine add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) ?_
Mathlib/LinearAlgebra/Matrix/Rank.lean:476:  refine add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_
Mathlib/LinearAlgebra/Dual/Lemmas.lean:1034:  rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]

$ /bin/bash -lc "sed -n '165,187p' Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean && rg -n \"mem_ker|ker_ne_bot\" Mathlib/LinearAlgebra/Basic.lean Mathlib/LinearAlgebra | head -100"
section DivisionRing

variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂]
  [Module K V₂]

/-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
the dimension of the source space. -/
theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V₂) :
    finrank K (LinearMap.range f) + finrank K (LinearMap.ker f) = finrank K V := by
  rw [← f.quotKerEquivRange.finrank_eq]
  exact Submodule.finrank_quotient_add_finrank _

lemma ker_ne_bot_of_finrank_lt [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
    (h : finrank K V₂ < finrank K V) :
    LinearMap.ker f ≠ ⊥ := by
  have h₁ := f.finrank_range_add_finrank_ker
  have h₂ : finrank K (LinearMap.range f) ≤ finrank K V₂ := (LinearMap.range f).finrank_le
  suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this
  lia

end DivisionRing

rg: Mathlib/LinearAlgebra/Basic.lean: No such file or directory (os error 2)
Mathlib/LinearAlgebra/Pi.lean:129:      simp only [mem_iInf, mem_ker, proj_apply] at h
Mathlib/LinearAlgebra/Pi.lean:197:  simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
Mathlib/LinearAlgebra/Pi.lean:208:      simp only [mem_iInf, mem_ker, proj_apply] at hb
Mathlib/LinearAlgebra/Pi.lean:239:  simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
Mathlib/LinearAlgebra/Pi.lean:317:    simp only [mem_iInf, mem_ker, proj_apply, pi_apply]
Mathlib/LinearAlgebra/Pi.lean:330:      simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean:223:  · simp_rw [Submodule.mem_map, LinearMap.mem_ker]
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean:246:  simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean:257:  simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coe_subtype,

$ /bin/bash -lc 'rg -n "clearDenom|commonDenom|den.*prod|num_den|den_dvd|den.*smul|Int.*den" Mathlib/Data/Rat Mathlib | head -220'
Mathlib/Data/Rat/Lemmas.lean:34:theorem den_dvd (a b : ℤ) : ((a /. b).den : ℤ) ∣ b := by
Mathlib/Data/Rat/Lemmas.lean:42:theorem num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) :
Mathlib/Data/Rat/Lemmas.lean:48:    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
Mathlib/Data/Rat/Lemmas.lean:49:    · rwa [num_divInt_den]
Mathlib/Data/Rat/Lemmas.lean:59:theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den := by
Mathlib/Data/Rat/Lemmas.lean:69:theorem sub_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ - q₂).den ∣ q₁.den.lcm q₂.den := by
Mathlib/Data/Rat/Lemmas.lean:70:  simpa only [sub_eq_add_neg, neg_den] using add_den_dvd_lcm q₁ (-q₂)
Mathlib/Data/Rat/Lemmas.lean:72:theorem add_den_dvd (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den * q₂.den :=
Mathlib/Data/Rat/Lemmas.lean:73:  (add_den_dvd_lcm _ _).trans (Nat.lcm_dvd_mul _ _)
Mathlib/Data/Rat/Lemmas.lean:75:theorem sub_den_dvd (q₁ q₂ : ℚ) : (q₁ - q₂).den ∣ q₁.den * q₂.den :=
Mathlib/Data/Rat/Lemmas.lean:76:  (sub_den_dvd_lcm _ _).trans (Nat.lcm_dvd_mul _ _)
Mathlib/Data/Rat/Lemmas.lean:78:theorem mul_den_dvd (q₁ q₂ : ℚ) : (q₁ * q₂).den ∣ q₁.den * q₂.den := by
Mathlib/Data/Rat/Lemmas.lean:95:  · simpa using add_den_dvd q n
Mathlib/Data/Rat/Lemmas.lean:96:  · simpa using add_den_dvd (q + n) (-n)
Mathlib/Data/Rat/Lemmas.lean:104:  rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]
Mathlib/Data/Rat/Lemmas.lean:149:theorem add_num_den (q r : ℚ) :
Mathlib/Data/Rat/Lemmas.lean:151:  have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
Mathlib/Data/Rat/Lemmas.lean:152:  have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
Mathlib/Data/Rat/Lemmas.lean:153:  conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
Mathlib/Data/Rat/Lemmas.lean:164:    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
Mathlib/Data/Rat/Lemmas.lean:188:  Rat.num_den_mk d_ne_zero this
Mathlib/Data/Rat/Lemmas.lean:190:theorem mul_num_den' (q r : ℚ) :

$ /bin/bash -lc 'rg -n "Polynomial.*IsEquivalent|isEquivalent.*Polynomial|isEquivalent_atTop|eval.*atTop.*leading|tendsto.*Polynomial.*atTop|IsLittleO.*Polynomial" Mathlib/Analysis Mathlib/Algebra/Polynomial | head -240'
Mathlib/Analysis/Polynomial/Basic.lean:16:The main result is `Polynomial.isEquivalent_atTop_lead`, which states that for
Mathlib/Analysis/Polynomial/Basic.lean:48:theorem isEquivalent_atTop_lead :
Mathlib/Analysis/Polynomial/Basic.lean:49:    (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree := by
Mathlib/Analysis/Polynomial/Basic.lean:64:  P.isEquivalent_atTop_lead.symm.tendsto_atTop <|
Mathlib/Analysis/Polynomial/Basic.lean:69:    Tendsto (fun x => eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff := by
Mathlib/Analysis/Polynomial/Basic.lean:72:    (isEquivalent_atTop_lead P).tendsto_atTop h
Mathlib/Analysis/Polynomial/Basic.lean:77:    Tendsto (fun x => eval x P) atTop atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0 := by
Mathlib/Analysis/Polynomial/Basic.lean:78:  simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg,
Mathlib/Analysis/Polynomial/Basic.lean:106:    Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0 := by
Mathlib/Analysis/Polynomial/Basic.lean:108:  · have := P.isEquivalent_atTop_lead.tendsto_nhds h
Mathlib/Analysis/Polynomial/Basic.lean:114:  · refine P.isEquivalent_atTop_lead.symm.tendsto_nhds ?_
Mathlib/Analysis/Polynomial/Basic.lean:124:  convert! (P.comp (-X)).isEquivalent_atTop_lead.comp_tendsto tendsto_neg_atBot_atTop using 2
Mathlib/Analysis/Polynomial/Basic.lean:149:theorem isEquivalent_atTop_div :
Mathlib/Analysis/Polynomial/Basic.lean:157:    (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
Mathlib/Analysis/Polynomial/Basic.lean:166:  refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
Mathlib/Analysis/Polynomial/Basic.lean:183:  · have := (isEquivalent_atTop_div P Q).tendsto_nhds h
Mathlib/Analysis/Polynomial/Basic.lean:194:    Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 <| P.leadingCoeff / Q.leadingCoeff) := by
Mathlib/Analysis/Polynomial/Basic.lean:195:  refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
Mathli

$ /bin/bash -lc "sed -n '1,80p' Mathlib/Analysis/Polynomial/Basic.lean && rg -n \"isEquivalent.*log|isLittleO.*log|log.*isLittleO|pow.*log.*Is\" Mathlib/Analysis/SpecialFunctions/Log Mathlib/Analysis/Asymptotics | head -220"
/-
Copyright (c) 2020 Anatole Dedecker. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anatole Dedecker, Devon Tuma
-/
module

public import Mathlib.Algebra.Polynomial.Roots
public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
public import Mathlib.Analysis.Asymptotics.SpecificAsymptotics

/-!
# Limits related to polynomial and rational functions

This file proves basic facts about limits of polynomial and rational functions.
The main result is `Polynomial.isEquivalent_atTop_lead`, which states that for
any polynomial `P` of degree `n` with leading coefficient `a`, the corresponding
polynomial function is equivalent to `a * x^n` as `x` goes to +∞.

We can then use this result to prove various limits for polynomial and rational
functions, depending on the degrees and leading coefficients of the considered
polynomials.
-/

public section


open Filter Finset Asymptotics

open Asymptotics Polynomial Topology

namespace Polynomial

variable {𝕜 : Type*} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : 𝕜[X])

theorem eventually_atTop_not_isRoot (hP : P ≠ 0) : ∀ᶠ x in atTop, ¬P.IsRoot x :=
  atTop_le_cofinite <| (finite_setOfPred_isRoot hP).compl_mem_cofinite

@[deprecated (since := "2026-02-05")] alias eventually_no_roots := eventually_atTop_not_isRoot

theorem eventually_atBot_not_isRoot (hP : P ≠ 0) : ∀ᶠ x in atBot, ¬P.IsRoot x :=
  atBot_le_cofinite <| (finite_setOfPred_isRoot hP).compl_mem_cofinite

variable [OrderTopology 𝕜]

section PolynomialAtTop

theorem isEquivalent_atTop_lead :
    (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree := by
  by_cases h : P = 0
  · simp [h, IsEquivalent.refl]
  · simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
    exact
      IsLittleO.add_isEquivalent
        (IsLittleO.sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittle

$ /bin/bash -lc 'rg -n "def swap|theorem swap|swap.*Polynomial|Polynomial.*swap" Mathlib/Algebra/Polynomial | head -160 && rg -n "bivariate|eval₂.*eval₂|eval.*eval.*Polynomial" Mathlib/Algebra/Polynomial/Eval Mathlib/Algebra/Polynomial | head -200'
Mathlib/Algebra/Polynomial/Div.lean:617:    {x : S} (hx : q.eval₂ f x = 0) : (p %ₘ q).eval₂ f x = p.eval₂ f x := by
Mathlib/Algebra/Polynomial/Div.lean:618:  rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]
Mathlib/Algebra/Polynomial/Eval/SMul.lean:45:    eval₂ g x (s • p) = g s * eval₂ g x p := by
Mathlib/Algebra/Polynomial/Eval/SMul.lean:48:  rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B] <;>
Mathlib/Algebra/Polynomial/Eval/SMul.lean:60:  rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
Mathlib/Algebra/Polynomial/FieldDivision.lean:466:    (hg : g.eval₂ ϕ α = 0) : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 := by
Mathlib/Algebra/Polynomial/FieldDivision.lean:467:  rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
Mathlib/Algebra/Polynomial/FieldDivision.lean:475:    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : f.eval₂ ϕ α = 0 := by
Mathlib/Algebra/Polynomial/FieldDivision.lean:480:    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : g.eval₂ ϕ α = 0 := by
Mathlib/Algebra/Polynomial/FieldDivision.lean:486:    (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 ↔ f.eval₂ ϕ α = 0 ∧ g.eval₂ ϕ α = 0 :=
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:41:theorem eval₂_at_zero : p.eval₂ f 0 = f (coeff p 0) := by
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:47:theorem eval₂_C_X : eval₂ C X p = p :=
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:139:    (p.map f).eval₂ g x = p.eval₂ (g.comp f) x := by
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:140:  rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:172:theorem hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) := by
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:173:  rw [← eval₂_map, eval₂_at_apply, eval_map]
Mathlib/Algebra/Polynomial/Eval/Coeff.lean:187:theorem eval₂_hom (x : R) : p.eval₂ f (f x) = f (p.eval x) :=
Mathlib/Algebra/Polynomial/Reverse.lean:192:    

$ /bin/bash -lc "sed -n '1,230p' Mathlib/Algebra/Polynomial/Bivariate.lean"
/-
Copyright (c) 2024 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/
module

public import Mathlib.RingTheory.AdjoinRoot
public import Mathlib.Algebra.MvPolynomial.PDeriv
public import Mathlib.RingTheory.Derivation.MapCoeffs

/-!
# Bivariate polynomials

This file introduces the notation `R[X][Y]` for the polynomial ring `R[X][X]` in two variables,
and the notation `Y` for the second variable, in the `Polynomial.Bivariate` scope.

It also defines `Polynomial.evalEval` for the evaluation of a bivariate polynomial at a point
on the affine plane, which is a ring homomorphism (`Polynomial.evalEvalRingHom`), as well as
the abbreviation `CC` to view a constant in the base ring `R` as a bivariate polynomial.
-/

@[expose] public section

/-- The notation `Y` for `X` in the `Polynomial` scope. -/
scoped[Polynomial.Bivariate] notation3:max "Y" => Polynomial.X (R := Polynomial _)

/-- The notation `R[X][Y]` for `R[X][X]` in the `Polynomial` scope. -/
scoped[Polynomial.Bivariate] notation3:max R "[X][Y]" => Polynomial (Polynomial R)

open scoped Polynomial.Bivariate

namespace Polynomial

noncomputable section

variable {R S : Type*}

section Semiring

variable [Semiring R]

/-- `evalEval x y p` is the evaluation `p(x,y)` of a two-variable polynomial `p : R[X][Y]`. -/
abbrev evalEval (x y : R) (p : R[X][Y]) : R := eval x (eval (C y) p)

/-- A constant viewed as a polynomial in two variables. -/
abbrev CC (r : R) : R[X][Y] := C (C r)

lemma evalEval_C (x y : R) (p : R[X]) : (C p).evalEval x y = p.eval x := by
  rw [evalEval, eval_C]

lemma evalEval_map_C (x y : R) (p : R[X]) : (p.map C).evalEval x y = p.eval y := by
  rw [evalEval, eval_map_apply, eval_C]

@[simp]
lemma evalEval_CC (x y : R) (p : R) : (CC p).evalEval x y = p := by
  rw [evalEval_C, eval_C]

@[simp]
lemma evalEval_zero (x y : R) : (0 : R[X][Y]).evalEval x y = 0 := by
  simp only [evalEval, eval_zero]

@[simp]
lemma evalEval_one (x y : R) 

$ /bin/bash -lc 'rg -n "pow.*log.*pow|pow_log|log.*pow.*isLittleO|isLittleO.*pow.*pow.*atTop|pow_pow_atTop" Mathlib/Analysis/Asymptotics Mathlib/Analysis/SpecialFunctions | head -240'
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean:117:  rw [← log_rpow, ← log_rpow, ← log_mul]
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean:71:    log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean:90:theorem Asymptotics.isLittleO_pow_pow_atTop_of_lt
Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean:93:  refine (isLittleO_iff_tendsto' ?_).mpr (tendsto_pow_div_pow_atTop_zero hpq)
Mathlib/Analysis/SpecialFunctions/Stirling.lean:71:  · rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:137:theorem rpow_logb_eq_abs (hx : x ≠ 0) : b ^ logb b x = |x| := by
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:146:theorem rpow_logb (hx : 0 < x) : b ^ logb b x = x := by
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:147:  rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:150:theorem rpow_logb_of_neg (hx : x < 0) : b ^ logb b x = -x := by
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:151:  rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:156:  · exact rpow_logb b_pos b_ne_one hy
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:160:  ⟨b ^ x, rpow_pos_of_pos b_pos x, logb_rpow b_pos b_ne_one⟩
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:207:  rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:210:  rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:213:  rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:216:  rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]
Mathlib/Analysis/SpecialFunctions/Log/Base.lean:297:  rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_l

$ /bin/bash -lc 'rg -n "Infinite.*fiber|infinite_fiber|Infinite.*finite.*range|Finite.*Infinite.*preimage|exists.*Infinite.*preimage" Mathlib/Data/Set Mathlib | head -200'
Mathlib/Data/Set/Finite/Basic.lean:605:protected lemma Infinite.preimage (hs : s.Infinite) (hf : s ⊆ range f) : (f ⁻¹' s).Infinite :=
Mathlib/Order/KonigLemma.lean:140:    obtain ⟨a₀, ha₀⟩ := Finite.exists_infinite_fiber (fun (a : αs) ↦ π zero_le a.2)
Mathlib/Combinatorics/Pigeonhole.lean:33:* `Data.Fintype.Basic` has `Finite.exists_infinite_fiber`
Mathlib/Data/Fintype/Pigeonhole.lean:21:* `Finite.exists_infinite_fiber`: Infinitely many pigeons in finitely many pigeonholes. Strong
Mathlib/Data/Fintype/Pigeonhole.lean:72:See also: `Fintype.exists_ne_map_eq_of_card_lt`, `Finite.exists_infinite_fiber`.
Mathlib/Data/Fintype/Pigeonhole.lean:86:theorem Finite.exists_infinite_fiber [Infinite α] [Finite β] (f : α → β) :
Mathlib/SetTheory/Cardinal/Pigeonhole.lean:81:theorem exists_infinite_fiber {β α : Type u} (f : β → α) (h : #α < #β) [Infinite β] :
Mathlib/SetTheory/Cardinal/Pigeonhole.lean:90:/-- A weaker version of `exists_infinite_fiber` that requires codomain to be infinite. -/
Mathlib/SetTheory/Cardinal/Pigeonhole.lean:91:theorem exists_infinite_fiber' {β α : Type u} (f : β → α) (h : #α < #β) [Infinite α] :
Mathlib/SetTheory/Cardinal/Pigeonhole.lean:93:  suffices Infinite β from exists_infinite_fiber f h
Mathlib/SetTheory/Cardinal/Pigeonhole.lean:122:  obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h
Mathlib/Data/Set/Finite/Basic.lean:605:protected lemma Infinite.preimage (hs : s.Infinite) (hf : s ⊆ range f) : (f ⁻¹' s).Infinite :=
Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean:249:  obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber' Φ h

$ /bin/bash -lc 'rg -n "comp.*ne_zero|natDegree_comp|degree_comp|comp_eq_zero|comp.*X.*C" Mathlib/Algebra/Polynomial | head -220'
Mathlib/Algebra/Polynomial/Div.lean:706:    (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t = (p.comp (X + C t)).trailingCoeff := by
Mathlib/Algebra/Polynomial/Div.lean:712:  have : (g.comp (X + C t)).coeff 0 = g.eval t := by
Mathlib/Algebra/Polynomial/Div.lean:713:    rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
Mathlib/Algebra/Polynomial/Div.lean:714:  rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp,
Mathlib/Algebra/Polynomial/RingDivision.lean:109:    p.rootMultiplicity t = (p.comp (X + C t)).rootMultiplicity 0 := by
Mathlib/Algebra/Polynomial/RingDivision.lean:111:  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
Mathlib/Algebra/Polynomial/RingDivision.lean:119:    p.rootMultiplicity t = (p.comp (X + C t)).natTrailingDegree :=
Mathlib/Algebra/Polynomial/RingDivision.lean:178:private theorem rootMultiplicity_comp_C_mul_X_add_C_le (p : R[X]) (a b c : R) (ha : IsUnit a) :
Mathlib/Algebra/Polynomial/RingDivision.lean:179:    (p.comp (C a * X + C b)).rootMultiplicity c ≤ p.rootMultiplicity (a * c + b) := by
Mathlib/Algebra/Polynomial/RingDivision.lean:183:  have h := pow_rootMultiplicity_dvd (p.comp (C a * X + C b)) c
Mathlib/Algebra/Polynomial/RingDivision.lean:184:  rw [dvd_comp_C_mul_X_add_C_iff, pow_comp] at h
Mathlib/Algebra/Polynomial/RingDivision.lean:188:theorem rootMultiplicity_comp_C_mul_X_add_C (p : R[X]) (a b c : R) (ha : IsUnit a) :
Mathlib/Algebra/Polynomial/RingDivision.lean:189:    (p.comp (C a * X + C b)).rootMultiplicity c = p.rootMultiplicity (a * c + b) := by
Mathlib/Algebra/Polynomial/RingDivision.lean:191:  apply le_antisymm (rootMultiplicity_comp_C_mul_X_add_C_le p a b c ha)
Mathlib/Algebra/Polynomial/RingDivision.lean:192:  have := rootMultiplicity_comp_C_mul_X_add_C_le
Mathlib/Algebra/Polynomial/RingDivision.lean:193:    (p.comp (C a * X + C b)) ⅟a (- ⅟a * b) (a * c + b) (isUnit_of_invertible ⅟a)
Mathlib/Algebra/Polynomial/RingDivision.lean:207:    ((-

$ /bin/bash -lc 'rg -n "evalEval.*nth|bivariate.*asympt|Polynomial.*nth_prime|eval.*nth_prime|evalEval.*log" /tmp/pnt-project/PrimeNumberTheoremAnd | head -100'

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:18:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.nth', which is 'noncomputable'
ChampernowneA.lean:70:35: error: Application type mismatch: The argument
  hxy
has type
  (fun n => ⟨↑↑n, ⋯⟩) x = (fun n => ⟨↑↑n, ⋯⟩) y
but is expected to have type
  x = y
in the application
  congrArg Subtype.val hxy
ChampernowneA.lean:71:10: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Infinite ↑{n | offset n = a}

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
ChampernowneA.lean:87:6: error: Application type mismatch: The argument
  nthPrime_strictMono (Nat.add_lt_add_left hij n)
has type
  nthPrime (n + ↑i) < nthPrime (n + ↑j)
but is expected to have type
  nthPrime n ≤ nthPrime (n + ↑i)
in the application
  Nat.sub_lt_sub_right (nthPrime_strictMono (Nat.add_lt_add_left hij n))

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
#check Finite.exists_infinite_fiber
#check Set.infinite_coe_iff
#check Infinite.of_injective_forall_mem
#check Infinite.of_injective_forall_mem
#check Infinite.of_injective
#check Set.Infinite.of_fintype
#check Set.Infinite.mono
#check Set.infinite_range_of_injective
#check Nat.sub_lt_sub_left
#check Nat.sub_lt_sub_right
EOF
lake env lean /tmp/Check.lean"
Finite.exists_infinite_fiber.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] (f : α → β) :
  ∃ y, Infinite ↑(f ⁻¹' {y})
Set.infinite_coe_iff.{u} {α : Type u} {s : Set α} : Infinite ↑s ↔ s.Infinite
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Infinite.of_injective_forall_mem`
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Infinite.of_injective_forall_mem`
Infinite.of_injective.{u_4, u_5} {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : β → α) (hf : Function.Injective f) :
  Infinite α
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Set.Infinite.of_fintype`
Set.Infinite.mono.{u} {α : Type u} {s t : Set α} (h : s ⊆ t) : s.Infinite → t.Infinite
Set.infinite_range_of_injective.{u, v} {α : Type u} {β : Type v} [Infinite α] {f : α → β} (hi : Function.Injective f) :
  (Set.range f).Infinite
Nat.sub_lt_sub_left {k m n : ℕ} : k < m → k < n → m - n < m - k
Nat.sub_lt_sub_right {a b c : ℕ} : c ≤ a → a < b → a - c < b - c

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:71:8: error: Type mismatch
  congrArg (fun z => ↑z) hxy
has type
  ↑((fun n => ⟨↑↑n, ⋯⟩) x) = ↑((fun n => ⟨↑↑n, ⋯⟩) y)
but is expected to have type
  ↑x = ↑y

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:110:2: error: Type mismatch
  IsLittleO.congr' hdiv ?m.40
has type
  ((fun n => ↑n * Real.log ↑n) / fun n => ↑n) =ᶠ[atTop] ?m.39 → ?m.37 =o[atTop] ?m.39
but is expected to have type
  primeRatio ~[atTop] fun n => Real.log ↑n
ChampernowneA.lean:116:2: error: Tactic `apply` failed: could not unify the conclusion of `IsEquivalent.tendsto_atTop (pnt_primeRatio hPNT)`
  Tendsto (fun n => Real.log ↑n) atTop atTop
with the goal
  Tendsto primeRatio atTop atTop

Note: The full type of `IsEquivalent.tendsto_atTop (pnt_primeRatio hPNT)` is
  Tendsto primeRatio atTop atTop → Tendsto (fun n => Real.log ↑n) atTop atTop

hPNT : PrimeNumberTheorem
⊢ Tendsto primeRatio atTop atTop

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Filter Asymptotics
#check IsEquivalent.congr
#check IsEquivalent.congr'
#check IsEquivalent.tendsto_atTop
#check IsEquivalent.symm
#check IsEquivalent.trans_isLittleO
#check IsLittleO.congr'
EOF
lake env lean /tmp/Check.lean"
/tmp/Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.congr`
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.congr'`
Asymptotics.IsEquivalent.tendsto_atTop.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β]
  [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atTop) :
  Tendsto v l atTop
Asymptotics.IsEquivalent.symm.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β}
  {l : Filter α} (h : u ~[l] v) : v ~[l] u
Asymptotics.IsEquivalent.trans_isLittleO.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {β₂ : Type u_3}
  [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =o[l] g₂) :
  f =o[l] g₂
Asymptotics.IsLittleO.congr'.{u_1, u_3, u_4} {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F]
  {l : Filter α} {f₁ f₂ : α → E} {g₁ g₂ : α → F} (h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[l] g₂

$ /bin/bash -lc 'rg -n "namespace IsEquivalent|theorem.*congr.*IsEquivalent|lemma.*congr.*IsEquivalent|IsEquivalent.*congr" Mathlib/Analysis/Asymptotics | head -200'
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean:102:theorem IsEquivalent.congr_left {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) :
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean:106:theorem IsEquivalent.congr_right {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) :
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean:388:  IsEquivalent.congr_right (isLittleO_refl_left _ _) h

$ /bin/bash -lc "sed -n '90,112p' Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean && rg -n \"tendsto_atTop.*iff.*IsEquivalent|tendsto_atTop.*symm\" Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean | head -60"
rw [IsEquivalent, sub_self]
  exact isLittleO_zero _ _

@[symm]
theorem IsEquivalent.symm (h : u ~[l] v) : v ~[l] u :=
  (h.isLittleO.trans_isBigO h.isBigO_symm).symm

@[trans]
theorem IsEquivalent.trans {l : Filter α} {u v w : α → β} (huv : u ~[l] v) (hvw : v ~[l] w) :
    u ~[l] w :=
  (huv.isLittleO.trans_isBigO hvw.isBigO).triangle hvw.isLittleO

theorem IsEquivalent.congr_left {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) :
    w ~[l] v :=
  huv.congr' (huw.sub (EventuallyEq.refl _ _)) (EventuallyEq.refl _ _)

theorem IsEquivalent.congr_right {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) :
    u ~[l] w :=
  (huv.symm.congr_left hvw).symm

theorem isEquivalent_zero_iff_eventually_zero : u ~[l] 0 ↔ u =ᶠ[l] 0 := by
  rw [IsEquivalent, sub_zero]
  exact isLittleO_zero_right_iff
321:  ⟨huv.tendsto_atTop, huv.symm.tendsto_atTop⟩

$ /bin/bash -lc "sed -n '310,326p' Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean"
variable {α β : Type*} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β]
  {u v : α → β} {l : Filter α}

theorem IsEquivalent.tendsto_atTop [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atTop) :
    Tendsto v l atTop :=
  let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul
  Tendsto.congr' h.symm (mul_comm u φ ▸ hu.atTop_mul_pos zero_lt_one hφ)

theorem IsEquivalent.tendsto_atTop_iff [OrderTopology β] (huv : u ~[l] v) :
    Tendsto u l atTop ↔ Tendsto v l atTop :=
  ⟨huv.tendsto_atTop, huv.symm.tendsto_atTop⟩

theorem IsEquivalent.tendsto_atBot [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atBot) :
    Tendsto v l atBot := by
  convert! tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
  ext

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Filter Asymptotics
#check IsLittleO.mul
#check IsLittleO.mul_isBigO
#check IsLittleO.isBigO_mul
#check IsLittleO.mul_isBigO'
#check IsLittleO.trans_isBigO
#check IsBigO.trans_isLittleO
#check isBigO_pow_pow_atTop_of_le
#check Asymptotics.isLittleO_pow_pow_atTop_of_lt
#check IsEquivalent.mul
#check IsEquivalent.const_mul
#check IsEquivalent.mul_const
#check IsEquivalent.sum
#check IsLittleO.sum
#check IsLittleO.const_mul_left
#check IsLittleO.const_mul_right
EOF
lake env lean /tmp/Check.lean"
Asymptotics.IsLittleO.mul.{u_1, u_13, u_17} {α : Type u_1} {R : Type u_13} [SeminormedRing R] {S : Type u_17}
  [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
  (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
Asymptotics.IsLittleO.mul_isBigO.{u_1, u_13, u_17} {α : Type u_1} {R : Type u_13} [SeminormedRing R] {S : Type u_17}
  [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
  (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.isBigO_mul`
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.mul_isBigO'`
Asymptotics.IsLittleO.trans_isBigO.{u_1, u_3, u_4, u_8} {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8}
  [Norm E] [Norm F] [SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'} (hfg : f =o[l] g)
  (hgk : g =O[l] k) : f =o[l] k
Asymptotics.IsBigO.trans_isLittleO.{u_1, u_3, u_5, u_7} {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7}
  [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g)
  (hgk : g =o[l] k) : f =o[l] k
/tmp/Check.lean:9:7: error(lean.unknownIdentifier): Unknown identifier `isBigO_pow_pow_atTop_of_le`
Asymptotics.isLittleO_pow_pow_atTop_of_lt.{u_1} {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {p q : ℕ} (hpq : p < q) : (fun x => x ^ p) =o[atTop] fun x => x ^ q
Asymptotics.IsEquivalent.mul.{u_1, u_3} {α : Type u_1} {β : Type u_3} [NormedField β] {t u v w : α → β} {l : Filter α}
  (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w
/tmp/Check.lean:12:7: error: Invalid field notation: Function `Function.const_mul` does not have a usable parameter of type `Function` for which to substitute `IsEquivalent`

Note: Such a parameter must 

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Filter Asymptotics
#check IsBigO.mul_isLittleO
#check IsBigO.mul
#check IsBigOWith.of_bound
#check IsBigO.of_bound
#check IsBigO.of_bound'
#check isBigO_iff_eventually
#check isBigOWith_iff
#check IsLittleO.comp_tendsto
#check IsLittleO.congr'
#check IsLittleO.congr_left
#check IsLittleO.congr_right
EOF
lake env lean /tmp/Check.lean"
Asymptotics.IsBigO.mul_isLittleO.{u_1, u_13, u_17} {α : Type u_1} {R : Type u_13} [SeminormedRing R] {S : Type u_17}
  [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
  (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
Asymptotics.IsBigO.mul.{u_1, u_13, u_17} {α : Type u_1} {R : Type u_13} [SeminormedRing R] {S : Type u_17}
  [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
  (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x
Asymptotics.IsBigOWith.of_bound.{u_1, u_3, u_4} {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ}
  {f : α → E} {g : α → F} {l : Filter α} : (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → IsBigOWith c l f g
Asymptotics.IsBigO.of_bound.{u_1, u_3, u_4} {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E}
  {g : α → F} {l : Filter α} (c : ℝ) (h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g
Asymptotics.IsBigO.of_bound'.{u_1, u_3, u_4} {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E}
  {g : α → F} {l : Filter α} (h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g
Asymptotics.isBigO_iff_eventually.{u_1, u_3, u_7} {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E]
  [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} :
  f =O[l] g' ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖
Asymptotics.isBigOWith_iff.{u_1, u_3, u_4} {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ}
  {f : α → E} {g : α → F} {l : Filter α} : IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Asymptotics.IsLittleO.comp_tendsto.{u_1, u_2, u_3, u_4} {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4}
  [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (hfg : f =o[l] g) {k : β → α} {l' : Filter β}
  (hk : Tendsto k l' l) : (f ∘ k) =o[l'] (g ∘ k)
Asymptotics.IsLittleO.congr'.{u_1, u_3, u_4} {α : Type u_1} {E : Type 

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:133:30: error: not a positivity goal
ChampernowneA.lean:144:21: error(lean.unknownIdentifier): Unknown constant `Real.one_le_log.mpr`
ChampernowneA.lean:168:46: error(lean.unknownIdentifier): Unknown identifier `D`

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '125,174p'"
125	    Real.isLittleO_pow_log_id_atTop.comp_tendsto tendsto_natCast_atTop_atTop
   126	  exact (pnt_primeRatio hPNT).pow m |>.trans_isLittleO hlog
   127	
   128	private lemma natPow_isBigO_natPow {a b : ℕ} (hab : a ≤ b) :
   129	    (fun n : ℕ ↦ (n : ℝ) ^ a) =O[atTop] (fun n : ℕ ↦ (n : ℝ) ^ b) := by
   130	  apply IsBigO.of_bound' (eventually_ge_atTop (1 : ℕ) |>.mono fun n hn ↦ ?_)
   131	  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (by positivity),
   132	    abs_of_nonneg (by positivity)]
   133	  exact pow_le_pow_right₀ (by positivity) hab
   134	
   135	private lemma natPow_isBigO_natPow_mul_logPow (D J : ℕ) :
   136	    (fun n : ℕ ↦ (n : ℝ) ^ D) =O[atTop]
   137	      (fun n : ℕ ↦ (n : ℝ) ^ D * Real.log n ^ J) := by
   138	  apply IsBigO.of_bound' (eventually_ge_atTop (3 : ℕ) |>.mono fun n hn ↦ ?_)
   139	  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (by positivity),
   140	    abs_of_nonneg (mul_nonneg (by positivity)
   141	      (pow_nonneg (Real.log_nonneg (by norm_cast; omega)) J))]
   142	  nth_rw 1 [← mul_one ((n : ℝ) ^ D)]
   143	  gcongr
   144	  exact one_le_pow₀ (Real.one_le_log.mpr (by norm_cast; omega))
   145	
   146	/-- Lexicographic dominance of the monomials `n^D (log n)^J`, where total
   147	degree is compared first and log-degree second. -/
   148	lemma logMonomial_isLittleO {t j D J : ℕ}
   149	    (h : t < D ∨ t = D ∧ j < J) :
   150	    (fun n : ℕ ↦ (n : ℝ) ^ t * Real.log n ^ j) =o[atTop]
   151	      (fun n : ℕ ↦ (n : ℝ) ^ D * Real.log n ^ J) := by
   152	  rcases h with ht | ⟨rfl, hj⟩
   153	  · have hlog :
   154	        (fun n : ℕ ↦ Real.log (n : ℝ) ^ j) =o[atTop] (fun n : ℕ ↦ (n : ℝ)) :=
   155	      Real.isLittleO_pow_log_id_atTop.comp_tendsto tendsto_natCast_atTop_atTop
   156	    have h₁ := (isBigO_refl (fun n : ℕ ↦ (n : ℝ) ^ t) atTop).mul_isLittleO hlog
   157	    have h₂ :
   158	        (fun n : ℕ ↦ (n : ℝ) ^ t * (n : ℝ)) =O[atTop]
   159	          (fun n : ℕ ↦ (n : ℝ) ^ D) := by
   160	      have := natP

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
#check pow_le_pow_right₀
#check pow_le_pow_right'
#check pow_le_pow_left'
#check Real.one_le_log
#check Real.le_log_iff_exp_le
#check Real.log_one_lt_iff
#check Real.log_le_sub_one_of_pos
EOF
lake env lean /tmp/Check.lean && rg -n \"one_le_log\" Mathlib/Analysis | head -40"
pow_le_pow_right₀.{u_2} {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀]
  [PosMulMono M₀] (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n
pow_le_pow_right'.{u_3} {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n m : ℕ} (ha : 1 ≤ a)
  (h : n ≤ m) : a ^ n ≤ a ^ m
pow_le_pow_left'.{u_3} {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M} (hab : a ≤ b)
  (i : ℕ) : a ^ i ≤ b ^ i
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Real.one_le_log`
Real.le_log_iff_exp_le {x y : ℝ} (hy : 0 < y) : x ≤ Real.log y ↔ Real.exp x ≤ y
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Real.log_one_lt_iff`
Real.log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) : Real.log x ≤ x - 1

$ /bin/bash -lc 'rg -n "exp_one.*(lt|le)|exp 1 <|exp_one_lt" Mathlib/Analysis | head -80'
Mathlib/Analysis/Complex/Angle.lean:70:lemma angle_exp_one (x : ℝ) : angle (exp (x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x| := by
Mathlib/Analysis/Complex/ExponentialBounds.lean:38:theorem exp_one_lt_d9 : exp 1 < 2.7182818286 :=
Mathlib/Analysis/Complex/ExponentialBounds.lean:44:theorem exp_one_lt_three : exp 1 < 3 :=
Mathlib/Analysis/Complex/ExponentialBounds.lean:45:  lt_trans exp_one_lt_d9 (by norm_num)
Mathlib/Analysis/Complex/ExponentialBounds.lean:48:  Int.floor_eq_iff.mpr ⟨exp_one_gt_two.le, by exact_mod_cast exp_one_lt_three⟩
Mathlib/Analysis/Complex/ExponentialBounds.lean:51:  Int.ceil_eq_iff.mpr ⟨by exact_mod_cast exp_one_gt_two, exp_one_lt_three.le⟩
Mathlib/Analysis/Complex/ExponentialBounds.lean:54:  refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨?_, by grind [exp_one_lt_three]⟩
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean:80:theorem exp_one_mul_le_exp {x : ℝ} : exp 1 * x ≤ exp x := by
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean:90:  · apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter
#check IsEquivalent.isBigO
#check IsEquivalent.isBigO_symm
#check IsEquivalent.const_mul
#check IsEquivalent.const_mul_left
#check IsEquivalent.const_mul_right
EOF
lake env lean /tmp/Check.lean"
Asymptotics.IsEquivalent.isBigO.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β}
  {l : Filter α} (h : u ~[l] v) : u =O[l] v
Asymptotics.IsEquivalent.isBigO_symm.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β}
  {l : Filter α} (h : u ~[l] v) : v =O[l] u
/tmp/Check.lean:5:7: error: Invalid field notation: Function `Function.const_mul` does not have a usable parameter of type `Function` for which to substitute `IsEquivalent`

Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.const_mul_left`
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.const_mul_right`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:183:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (?a * ?b) ^ ?n
in the target expression
  ↑n ^ i * ((fun n => ↑n * Real.log ↑n) ^ j) n = ↑n ^ (i + j) * Real.log ↑n ^ j

hPNT : PrimeNumberTheorem
i j : ℕ
hi : (fun n => ↑n ^ i) ~[atTop] fun n => ↑n ^ i
h : (fun n => ↑n ^ i) * (fun n => ↑(nthPrime n)) ^ j ~[atTop] (fun n => ↑n ^ i) * (fun n => ↑n * Real.log ↑n) ^ j
n : ℕ
⊢ ↑n ^ i * ((fun n => ↑n * Real.log ↑n) ^ j) n = ↑n ^ (i + j) * Real.log ↑n ^ j
ChampernowneA.lean:192:27: error: Application type mismatch: The argument
  IsEquivalent.isBigO_symm (primeMonomial_isEquivalent hPNT I J)
has type
  (fun n => ↑n ^ (I + J) * Real.log ↑n ^ J) =O[atTop] fun n => ↑n ^ I * ↑(nthPrime n) ^ J
but is expected to have type
  (fun n => ↑n ^ i * ↑(nthPrime n) ^ j) =o[atTop] ?m.74
in the application
  IsLittleO.trans_isBigO (IsEquivalent.isBigO_symm (primeMonomial_isEquivalent hPNT I J))
ChampernowneA.lean:188:58: error: unsolved goals
hPNT : PrimeNumberTheorem
i j I J : ℕ
h : i + j < I + J ∨ i + j = I + J ∧ j < J
hsmall : (fun n => ↑n ^ (i + j) * Real.log ↑n ^ j) =o[atTop] fun n => ↑n ^ (I + J) * Real.log ↑n ^ J
⊢ (fun n => ↑n ^ i * ↑(nthPrime n) ^ j) =o[atTop] fun n => ↑n ^ I * ↑(nthPrime n) ^ J

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc 'rg -n "lex_le_iff|Prod.*le_iff|instLinearOrder.*Prod|LinearOrder.*Prod" Mathlib/Order Mathlib/Data/Prod Mathlib | head -140'
Mathlib/Data/Prod/Lex.lean:147:/-- Variant of `Prod.Lex.le_iff` for partial orders. -/
Mathlib/Order/Hom/Lex.lean:161:    simpa [Prod.Lex.toLex_le_toLex] using le_iff_lt_or_eq
Mathlib/Order/Hom/Lex.lean:191:    simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
Mathlib/Order/Hom/Lex.lean:204:  map_rel_iff' := by simp [Prod.Lex.le_iff]
Mathlib/Order/Hom/Lex.lean:211:  map_rel_iff' := by simp [Prod.Lex.le_iff]
Mathlib/Order/Interval/Finset/Gaps.lean:172:    Prod.Lex.le_iff'.mp (G.monotone (by simp [le_iff_val_le_val])) |>.left
Mathlib/Order/Interval/Finset/Gaps.lean:192:  exact Prod.Lex.le_iff'.mp (F.orderEmbOfFin (α := α ×ₗ α) h |>.monotone (by grind)) |>.left
Mathlib/Order/Interval/Lex.lean:78:  { LinearOrder.lift' (fun x : Lex (NonemptyInterval α) => toLex (ofLex x).toDualProd) <|
Mathlib/Order/PiLex.lean:147:theorem lex_le_iff_of_unique [Unique ι] [LinearOrder ι] [∀ i, PartialOrder (β i)]
Mathlib/Order/PiLex.lean:153:theorem colex_le_iff_of_unique [Unique ι] [LinearOrder ι] [∀ i, PartialOrder (β i)]
Mathlib/Order/Interval/Finset/Gaps.lean:172:    Prod.Lex.le_iff'.mp (G.monotone (by simp [le_iff_val_le_val])) |>.left
Mathlib/Order/Interval/Finset/Gaps.lean:192:  exact Prod.Lex.le_iff'.mp (F.orderEmbOfFin (α := α ×ₗ α) h |>.monotone (by grind)) |>.left
Mathlib/Order/Interval/Lex.lean:78:  { LinearOrder.lift' (fun x : Lex (NonemptyInterval α) => toLex (ofLex x).toDualProd) <|
Mathlib/Order/PiLex.lean:147:theorem lex_le_iff_of_unique [Unique ι] [LinearOrder ι] [∀ i, PartialOrder (β i)]
Mathlib/Order/PiLex.lean:153:theorem colex_le_iff_of_unique [Unique ι] [LinearOrder ι] [∀ i, PartialOrder (β i)]
Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean:237:  ((Equiv.sigmaEquivProd β γ).multipliable_iff.mpr h).sigma
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean:217:  Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.summable_iff.symm
Mathlib/Topology/Algebra/InfiniteSum/Real.lean:82:  (Equiv.sigmaEquivProd _ _).summable_iff.symm.tran

$ /bin/bash -lc "rg -n \"IsEquivalent.*eventually.*ne|eventually.*ne.*IsEquivalent|IsEquivalent.*zero\" Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean | head -100 && cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter
#check IsLittleO.add_isEquivalent
#check IsLittleO.add_isEquivalent'
#check IsEquivalent.eventually_ne
#check IsEquivalent.eventually_ne_iff
#check IsEquivalent.congr_left
#check Finset.sum_eq_add_sum_diff_singleton
#check Finset.sum_erase_add
EOF
lake env lean /tmp/Check.lean"
Asymptotics.IsLittleO.add_isEquivalent.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β}
  {l : Filter α} (hu : u =o[l] w) (hv : v ~[l] w) : u + v ~[l] w
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.add_isEquivalent'`
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.eventually_ne`
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.eventually_ne_iff`
Asymptotics.IsEquivalent.congr_left.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β}
  {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) : w ~[l] v
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `Finset.sum_eq_add_sum_diff_singleton`
Finset.sum_erase_add.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι)
  (f : ι → M) {a : ι} (h : a ∈ s) : ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter Topology
#check IsEquivalent.exists_eq_mul
#check IsEquivalent.exists_eq_mul'
#check IsEquivalent.tendsto_nhds_iff
#check Filter.EventuallyEq.ne
EOF
lake env lean /tmp/Check.lean"
Asymptotics.IsEquivalent.exists_eq_mul.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedField β] {u v : α → β}
  {l : Filter α} (huv : u ~[l] v) : ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsEquivalent.exists_eq_mul'`
Asymptotics.IsEquivalent.tendsto_nhds_iff.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β}
  {l : Filter α} {c : β} (huv : u ~[l] v) : Tendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c)
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Filter.EventuallyEq.ne`

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Filter Topology
#check tendsto_order
#check tendsto_order.1
#check Filter.Tendsto.eventually
#check Metric.tendsto_nhds
EOF
lake env lean /tmp/Check.lean"
tendsto_order.{u, v} {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α}
  {a : α} {x : Filter β} :
  Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
tendsto_order.mp : Tendsto ?m.6 ?m.8 (𝓝 ?m.7) →
  (∀ a' < ?m.7, ∀ᶠ (b : ?m.2) in ?m.8, a' < ?m.6 b) ∧ ∀ a' > ?m.7, ∀ᶠ (b : ?m.2) in ?m.8, ?m.6 b < a'
Filter.Tendsto.eventually.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β}
  {p : β → Prop} (hf : Tendsto f l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) : ∀ᶠ (x : α) in l₁, p (f x)
Metric.tendsto_nhds.{u, v} {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α} :
  Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:206:2: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  b ≥ 0
  a ≥ 0
  a ≥ 0
where
 a := ↑I
 b := ↑J
ChampernowneA.lean:230:4: error: Type mismatch: After simplification, term
  hlt
 has type
  Or ((ofLex (toLex (q.1 + q.2, q.2))).1 < (ofLex (toLex (Q.1 + Q.2, Q.2))).1)
    ((ofLex (toLex (q.1 + q.2, q.2))).1 = (ofLex (toLex (Q.1 + Q.2, Q.2))).1 ∧
      (ofLex (toLex (q.1 + q.2, q.2))).2 < (ofLex (toLex (Q.1 + Q.2, Q.2))).2)
but is expected to have type
  Or (q.1 + q.2 < Q.1 + Q.2) (q.1 + q.2 = Q.1 + Q.2 ∧ q.2 < Q.2)
ChampernowneA.lean:247:4: error: Type mismatch
  Eq.symm (sum_erase_add s ?m.380 hQs)
has type
  ∑ x ∈ s, ?m.380 x = ∑ x ∈ s.erase Q, ?m.380 x + ?m.380 Q
but is expected to have type
  ((fun n => ∑ q ∈ s.erase Q, a q * (↑n ^ q.1 * ↑(nthPrime n) ^ q.2)) + lead) n =
    (fun n => ∑ q ∈ s, a q * (↑n ^ q.1 * ↑(nthPrime n) ^ q.2)) n

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '198,254p'"
198	/-- The ordering on bivariate monomials used in the paper: total degree first,
   199	then the exponent of the prime variable. -/
   200	def monomialKey (q : ℕ × ℕ) : Lex (ℕ × ℕ) :=
   201	  toLex (q.1 + q.2, q.2)
   202	
   203	lemma monomialKey_injective : Function.Injective monomialKey := by
   204	  rintro ⟨i, j⟩ ⟨I, J⟩ h
   205	  simp only [monomialKey, toLex_inj, Prod.mk.injEq] at h
   206	  omega
   207	
   208	/-- A nonempty finite linear combination of distinct monomials in `(n,pₙ)` is
   209	eventually nonzero.  This packages equation (2.3) of the paper. -/
   210	lemma finite_bivariate_sum_eventually_ne_zero (hPNT : PrimeNumberTheorem)
   211	    (s : Finset (ℕ × ℕ)) (a : ℕ × ℕ → ℝ)
   212	    (hs : s.Nonempty) (ha : ∀ q ∈ s, a q ≠ 0) :
   213	    ∀ᶠ n : ℕ in atTop,
   214	      ∑ q ∈ s, a q * ((n : ℝ) ^ q.1 * (nthPrime n : ℝ) ^ q.2) ≠ 0 := by
   215	  let keys : Finset (Lex (ℕ × ℕ)) := s.image monomialKey
   216	  have hkeys : keys.Nonempty := hs.image _
   217	  let K := keys.max' hkeys
   218	  have hKmem : K ∈ keys := keys.max'_mem hkeys
   219	  obtain ⟨Q, hQs, hQK⟩ := Finset.mem_image.mp hKmem
   220	  have hdom : ∀ q ∈ s, q ≠ Q →
   221	      q.1 + q.2 < Q.1 + Q.2 ∨
   222	        q.1 + q.2 = Q.1 + Q.2 ∧ q.2 < Q.2 := by
   223	    intro q hqs hqQ
   224	    have hkq : monomialKey q ∈ keys := Finset.mem_image.mpr ⟨q, hqs, rfl⟩
   225	    have hle : monomialKey q ≤ K := Finset.le_max' keys _ hkq
   226	    rw [← hQK] at hle
   227	    have hne : monomialKey q ≠ monomialKey Q :=
   228	      fun h ↦ hqQ (monomialKey_injective h)
   229	    have hlt : monomialKey q < monomialKey Q := lt_of_le_of_ne hle hne
   230	    simpa only [monomialKey, Prod.Lex.lt_iff, Prod.lex_def] using hlt
   231	  let lead : ℕ → ℝ := fun n ↦
   232	    a Q * ((n : ℝ) ^ Q.1 * (nthPrime n : ℝ) ^ Q.2)
   233	  have hrest :
   234	      (fun n : ℕ ↦
   235	        ∑ q ∈ s.erase Q,
   236	          a q * ((n : ℝ) ^ q.1 * (nthPrime n : ℝ) ^ q.2)) =o[atTop] lead := by
   237	   

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:208:2: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  b ≥ 0
  a ≥ 0
  a ≥ 0
where
 a := ↑I
 b := ↑J
ChampernowneA.lean:207:13: warning: This simp argument is unused:
  ofLex_toLex

Hint: Omit it from the simp argument list.
  [apply] simp only [Prod.mk.injEq] at h'

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:209:2: error: `simp` made no progress

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '202,214p'"
202	
   203	lemma monomialKey_injective : Function.Injective monomialKey := by
   204	  rintro ⟨i, j⟩ ⟨I, J⟩ h
   205	  change toLex (i + j, j) = toLex (I + J, J) at h
   206	  have h' : (i + j, j) = (I + J, J) := congrArg ofLex h
   207	  have hsum : i + j = I + J := congrArg Prod.fst h'
   208	  have hj : j = J := congrArg Prod.snd h'
   209	  simp only at hsum hj
   210	  apply Prod.ext
   211	  · simp only
   212	    omega
   213	  · simpa only using hj
   214

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Polynomial Finset
#check Polynomial.support_nonempty
#check Polynomial.support_nonempty_iff
#check Polynomial.mem_support_iff
#check Polynomial.not_mem_support_iff
#check Finset.biUnion_nonempty
#check Finset.mem_biUnion
#check Polynomial.eval_eq_sum
#check Polynomial.eval₂_eq_sum
EOF
lake env lean /tmp/Check.lean"
Polynomial.support_nonempty.{u} {R : Type u} [Semiring R] {p : R[X]} : p.support.Nonempty ↔ p ≠ 0
/tmp/Check.lean:4:7: error: Application type mismatch: The argument
  Polynomial
has type
  (R : Type ?u.1) → [Semiring R] → Type ?u.1
but is expected to have type
  ?m.1 → ?m.2
in the application
  @Function.support_nonempty_iff ?m.1 ?m.2 ?m.3 Polynomial
Polynomial.mem_support_iff.{u} {R : Type u} {n : ℕ} [Semiring R] {p : R[X]} : n ∈ p.support ↔ p.coeff n ≠ 0
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.not_mem_support_iff`
Finset.biUnion_nonempty.{u_1, u_2} {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] :
  (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
Finset.mem_biUnion.{u_1, u_2} {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] {b : β} :
  b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
Polynomial.eval_eq_sum.{u} {R : Type u} [Semiring R] {p : R[X]} {x : R} : eval x p = p.sum fun e a => a * x ^ e
Polynomial.eval₂_eq_sum.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : R[X]} [Semiring S] {f : R →+* S} {x : S} :
  eval₂ f x p = p.sum fun e a => f a * x ^ e

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:272:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Polynomial.semiring', which is 'noncomputable'
ChampernowneA.lean:280:46: error(lean.unknownIdentifier): Unknown identifier `mem_support_iff`
ChampernowneA.lean:283:4: error: Type mismatch: After simplification, term
  hi
 has type
  i ∈ (P.coeff j).support
but is expected to have type
  (P.coeff j).coeff i ≠ 0
ChampernowneA.lean:286:10: error(lean.unknownIdentifier): Unknown identifier `mem_support_iff`
ChampernowneA.lean:293:16: error(lean.unknownIdentifier): Unknown identifier `mem_support_iff.mpr`
ChampernowneA.lean:302:55: error(lean.unknownIdentifier): Unknown identifier `mem_support_iff.mp`
ChampernowneA.lean:303:45: error(lean.unknownIdentifier): Unknown identifier `mem_support_iff.mp`
ChampernowneA.lean:309:6: error(lean.unknownIdentifier): Unknown identifier `evalEval`
ChampernowneA.lean:308:57: error: unsolved goals
R : Type u_1
inst✝ : CommSemiring R
P : R[X][Y]
x y : R
⊢ Polynomial.evalEval x y P = ∑ q ∈ bivariateSupport P, (P.coeff q.2).coeff q.1 * (x ^ q.1 * y ^ q.2)
ChampernowneA.lean:330:23: error: Application type mismatch: The argument
  P
has type
  ℝ[X][Y]
but is expected to have type
  ℕ[X][Y]
in the application
  Polynomial.evalEval n (nthPrime n) P

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:288:14: error(lean.unknownIdentifier): Unknown identifier `coeff_zero`
ChampernowneA.lean:310:29: error(lean.unknownIdentifier): Unknown identifier `eval_finsetSum`
ChampernowneA.lean:310:45: error(lean.unknownIdentifier): Unknown identifier `eval_mul`
ChampernowneA.lean:310:55: error(lean.unknownIdentifier): Unknown identifier `eval_C`
ChampernowneA.lean:310:63: error(lean.unknownIdentifier): Unknown identifier `eval_pow`
ChampernowneA.lean:311:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ∑ x ∈ Finset.biUnion ?m.60 ?m.61, ?m.58 x
in the target expression
  ∑ x_1 ∈ (Polynomial.eval (Polynomial.C y) P).support, (Polynomial.eval (Polynomial.C y) P).coeff x_1 * x ^ x_1 =
    ∑ q ∈ bivariateSupport P, (P.coeff q.2).coeff q.1 * (x ^ q.1 * y ^ q.2)

R : Type u_1
inst✝ : CommSemiring R
P : R[X][Y]
x y : R
⊢ ∑ x_1 ∈ (Polynomial.eval (Polynomial.C y) P).support, (Polynomial.eval (Polynomial.C y) P).coeff x_1 * x ^ x_1 =
    ∑ q ∈ bivariateSupport P, (P.coeff q.2).coeff q.1 * (x ^ q.1 * y ^ q.2)

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:315:10: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  Polynomial.eval ?m.95 ?m.94
in the target expression
  (Polynomial.evalRingHom x) (P.coeff j) * y ^ j =
    ∑ x_1 ∈ (P.coeff j).support, (P.coeff (x_1, j).2).coeff (x_1, j).1 * (x ^ (x_1, j).1 * y ^ (x_1, j).2)

R : Type u_1
inst✝ : CommSemiring R
P : R[X][Y]
x y : R
j : ℕ
hj : j ∈ P.support
⊢ (Polynomial.evalRingHom x) (P.coeff j) * y ^ j =
    ∑ x_1 ∈ (P.coeff j).support, (P.coeff (x_1, j).2).coeff (x_1, j).1 * (x ^ (x_1, j).1 * y ^ (x_1, j).2)
ChampernowneA.lean:325:4: error: Tactic `subst` failed: did not find equation for eliminating 'j₂'

R : Type u_1
inst✝ : CommSemiring R
P : R[X][Y]
x y : R
j₁ : ℕ
hj₁ : j₁ ∈ ↑P.support
j₂ : ℕ
hj₂ : j₂ ∈ ↑P.support
hj : j₁ ≠ j₂
⊢ Function.onFun Disjoint (fun j => image (fun i => (i, j)) (P.coeff j).support) j₁ j₂

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:321:6: error: `simp` made no progress
ChampernowneA.lean:326:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  Disjoint ?m.168 ?m.169
in the target expression
  Function.onFun Disjoint (fun j => image (fun i => (i, j)) (P.coeff j).support) j₁ j₂

R : Type u_1
inst✝ : CommSemiring R
P : R[X][Y]
x y : R
j₁ : ℕ
hj₁ : j₁ ∈ ↑P.support
j₂ : ℕ
hj₂ : j₂ ∈ ↑P.support
hj : j₁ ≠ j₂
⊢ Function.onFun Disjoint (fun j => image (fun i => (i, j)) (P.coeff j).support) j₁ j₂

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '312,334p'"
312	  · apply sum_congr rfl
   313	    intro j hj
   314	    rw [sum_image]
   315	    · change Polynomial.eval x (P.coeff j) * y ^ j = _
   316	      rw [Polynomial.eval_eq_sum]
   317	      simp only [Polynomial.sum]
   318	      rw [Finset.sum_mul]
   319	      apply sum_congr rfl
   320	      intro i hi
   321	      simp only [Prod.fst, Prod.snd]
   322	      ac_rfl
   323	    · intro i₁ hi₁ i₂ hi₂ h
   324	      simpa using congrArg Prod.fst h
   325	  · intro j₁ hj₁ j₂ hj₂ hj
   326	    rw [Finset.disjoint_left]
   327	    intro q hq₁ hq₂
   328	    simp only [mem_image] at hq₁ hq₂
   329	    obtain ⟨i₁, hi₁, rfl⟩ := hq₁
   330	    obtain ⟨i₂, hi₂, hpair⟩ := hq₂
   331	    exact hj (congrArg Prod.snd hpair).symm
   332	
   333	end BivariatePolynomial
   334

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
#check Submodule.ne_bot_iff
#check Submodule.nontrivial_iff_ne_bot
#check Matrix.mulVecLin_apply
#check Module.finrank_fin_fun
#check Module.finrank_pi
#check Rat.num_divInt_den
#check Nat.dvd_prod_of_mem
#check Finset.dvd_prod_of_mem
#check Nat.prod_pos
#check Finset.prod_pos
EOF
lake env lean /tmp/Check.lean"
Submodule.ne_bot_iff.{u_1, u_3} {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M]
  (p : Submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0
Submodule.nontrivial_iff_ne_bot.{u_1, u_3} {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M]
  {p : Submodule R M} : Nontrivial ↥p ↔ p ≠ ⊥
Matrix.mulVecLin_apply.{u_1, u_4, u_5} {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n]
  (M : Matrix m n R) (v : n → R) : M.mulVecLin v = M.mulVec v
Module.finrank_fin_fun.{u} (R : Type u) [Semiring R] [StrongRankCondition R] {n : ℕ} : Module.finrank R (Fin n → R) = n
Module.finrank_pi.{u, v} (R : Type u) [Semiring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] :
  Module.finrank R (ι → R) = Fintype.card ι
Rat.num_divInt_den (a : ℚ) : Rat.divInt a.num ↑a.den = a
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `Nat.dvd_prod_of_mem`
Finset.dvd_prod_of_mem.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [CommMonoid M] (f : ι → M) {a : ι} {s : Finset ι}
  (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i
/tmp/Check.lean:10:7: error(lean.unknownIdentifier): Unknown constant `Nat.prod_pos`
Finset.prod_pos.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R]
  [PosMulStrictMono R] [Nontrivial R] {f : ι → R} {s : Finset ι} (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i

$ /bin/bash -lc 'rg -n "divInt_eq_div|cast_divInt|num_div_den" Mathlib/Data/Rat Mathlib/Algebra/Ring/Rat.lean | head -100'
Mathlib/Algebra/Ring/Rat.lean:78:lemma num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by
Mathlib/Algebra/Ring/Rat.lean:79:  rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]
Mathlib/Algebra/Ring/Rat.lean:82:  simp [divInt_eq_div, div_pow]
Mathlib/Data/Rat/Lemmas.lean:28:  rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e
Mathlib/Data/Rat/Lemmas.lean:38:    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
Mathlib/Data/Rat/Lemmas.lean:47:    refine (divInt_eq_divInt_iff ?_ hd).mp ?_
Mathlib/Data/Rat/Lemmas.lean:164:    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
Mathlib/Data/Rat/Lemmas.lean:187:  haveI : (n : ℚ) / d = Rat.divInt n d := by rw [← Rat.divInt_eq_div]
Mathlib/Data/Rat/Lemmas.lean:202:  rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
Mathlib/Data/Rat/Lemmas.lean:221:  rw [← divInt_eq_div]
Mathlib/Data/Rat/Lemmas.lean:238:  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
Mathlib/Data/Rat/Lemmas.lean:244:  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
Mathlib/Data/Rat/Lemmas.lean:321:  mpr h q := by simpa [num_div_den] using h q.num q.den (mod_cast q.den_ne_zero)
Mathlib/Data/Rat/Cast/CharZero.lean:30:    rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h
Mathlib/Data/Rat/Cast/CharZero.lean:69:theorem cast_divInt (a b : ℤ) : (a /. b : α) = a / b := by
Mathlib/Data/Rat/Cast/CharZero.lean:70:  simp only [divInt_eq_div, cast_div, cast_intCast]
Mathlib/Data/Rat/Cast/CharZero.lean:80:  on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
Mathlib/Data/Rat/Cast/Defs.lean:144:lemma cast_divInt_of_ne_zero (a : ℤ) {b : ℤ} (b0 : (b : α) ≠ 0) : (a /. b : α) = a / b := by
Mathlib/Data/Rat/Cast/Defs.lean:158:    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
Mathlib/Data/Rat/Cast/Defs.lean:165:  rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:369:59: error: unsolved goals
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
c : ι → ℚ
hc : c ≠ 0
D : ℕ := ∏ i, (c i).den
hDpos : 0 < D
t : ι → ℕ
ht : ∀ (i : ι), D = (c i).den * t i
z : ι → ℤ := fun i => (c i).num * ↑(t i)
i : ι
⊢ ↑(c i).num * ↑(↑(c i).num / ↑(c i).den).den = ↑(c i).den * ↑(↑(c i).num / ↑(c i).den).num
ChampernowneA.lean:373:6: error: mod_cast has type
  (c i).den * t i = D
but is expected to have type
  D = (c i).den * t i
ChampernowneA.lean:375:24: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ↑(c i).den * c i
in the target expression
  ↑(c i).num * ↑(t i) = ↑(c i).den * (↑(t i) * c i)

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
c : ι → ℚ
hc : c ≠ 0
D : ℕ := ∏ i, (c i).den
hDpos : 0 < D
t : ι → ℕ
ht : ∀ (i : ι), D = (c i).den * t i
z : ι → ℤ := fun i => (c i).num * ↑(t i)
i : ι
hnum : ↑(c i).den * c i = ↑(c i).num
htQ : ↑D = ↑(c i).den * ↑(t i)
⊢ ↑(c i).num * ↑(t i) = ↑(c i).den * (↑(t i) * c i)
ChampernowneA.lean:382:43: error: Application type mismatch: The argument
  Ne.symm (Nat.cast_ne_zero.mpr (LT.lt.ne' hDpos))
has type
  0 ≠ ↑D
but is expected to have type
  ¬?m.151 = 0
in the application
  Or.resolve_left (mul_eq_zero.mp ?m.155) (Ne.symm (Nat.cast_ne_zero.mpr (LT.lt.ne' hDpos)))

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:391:24: error: Application type mismatch: The argument
  this
has type
  0 = ↑D * c i
but is expected to have type
  ↑D * c i = 0
in the application
  mul_eq_zero.mp this

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:12: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  f
has type `?m.6.1 ℤ X ?m.7` which does not have the necessary form.
ChampernowneA.lean:401:11: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  f
has type `?m.6.1 ℤ X ?m.7` which does not have the necessary form.
ChampernowneA.lean:396:45: error: failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
X : ?m.1
⊢ ?m.5 ℤ X
ChampernowneA.lean:420:27: error: Invalid argument name `R` for function `Rat.cast_injective`

Hint: Perhaps you meant one of the following parameter names:
  • `α`: R̵α̲
  • `a₁`: R̵a̲₁̲
  • `a₂`: R̵a̲₂̲
ChampernowneA.lean:421:2: error: No goals to be solved
ChampernowneA.lean:445:51: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  f
has type `?m.6.1 ℤ X ?m.7` which does not have the necessary form.
ChampernowneA.lean:452:15: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  f
has type `?m.6.1 ℤ X ?m.7` which does not have the necessary form.
ChampernowneA.lean:450:9: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  f
has type `?m.6.1 ℤ X

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:420:27: error: Invalid argument name `R` for function `Int.cast_injective`

Hint: Perhaps you meant one of the following parameter names:
  • `α`: R̵α̲
  • `a₁`: R̵a̲₁̲
  • `a₂`: R̵a̲₂̲
ChampernowneA.lean:421:2: error: No goals to be solved
ChampernowneA.lean:458:10: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

f : ℤ[X]
d : ℕ
hdeg : f.natDegree = d
h : Fin (d * (d + 1) + 1) → ℕ
c : Fin (d * (d + 1) + 1) → ℤ
hc :
  ∀ (v : Fin d) (u : Fin (d + 1)), ∑ j, c j * (-↑(h j)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff ↑u = 0
v : Fin d
n : ℤ
Q : ℤ[X] := ⋯
⊢ fold max 0
      (Polynomial.natDegree ∘ fun i => Polynomial.C (c i * (-↑(h i)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑i))
      univ ≤
    d
ChampernowneA.lean:468:6: error: Type mismatch: After simplification, term
  hc v uf
 has type
  ∑ j, c j * (-↑(h j)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff ↑uf = 0
but is expected to have type
  (∑ j, Polynomial.C (c j * (-↑(h j)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff u = Polynomial.coeff 0 u
ChampernowneA.lean:474:2: error: Type mismatch: After simplification, term
  heval
 has type
  Polynomial.eval n (∑ j, Polynomial.C (c j * (-↑(h j)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑j)) = 0
but is expected to have type
  ∑ x, c x * (Polynomial.eval (n + ↑↑x) f * (-↑(h x)) ^ ↑v) = 0

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open Polynomial Finset
open scoped BigOperators Polynomial
#check Int.cast_injective
#check Polynomial.natDegree_sum_le
#check Polynomial.natDegree_sum_le_of_forall
#check Finset.natDegree_sum_le
#check Polynomial.coeff_sum
#check Polynomial.coeff_C_mul
#check Polynomial.eval_comp
EOF
lake env lean /tmp/Check.lean"
Int.cast_injective.{u_3} {α : Type u_3} [AddGroupWithOne α] [CharZero α] : Function.Injective Int.cast
Polynomial.natDegree_sum_le.{w, u_1} {ι : Type w} (s : Finset ι) {S : Type u_1} [Semiring S] (f : ι → S[X]) :
  (∑ i ∈ s, f i).natDegree ≤ fold max 0 (natDegree ∘ f) s
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.natDegree_sum_le_of_forall`
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Finset.natDegree_sum_le`
Polynomial.coeff_sum.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : R[X]} [Semiring S] (n : ℕ) (f : ℕ → R → S[X]) :
  (p.sum f).coeff n = p.sum fun a b => (f a b).coeff n
Polynomial.coeff_C_mul.{u} {R : Type u} {a : R} {n : ℕ} [Semiring R] (p : R[X]) : (C a * p).coeff n = a * p.coeff n
Polynomial.eval_comp.{u} {R : Type u} [CommSemiring R] {p q : R[X]} {x : R} : eval x (p.comp q) = eval (eval x q) p

$ /bin/bash -lc 'rg -n "natDegree.*sum.*forall|natDegree_sum.*trans|sum.*natDegree.*≤|natDegree.*sum_le" Mathlib/Algebra/Polynomial | head -120 && rg -n "fold.*le.*forall|fold_le" Mathlib/Algebra/Order Mathlib/Data/Finset | head -100'
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean:75:theorem sumIDeriv_apply_of_le {p : R[X]} {n : ℕ} (hn : p.natDegree ≤ n) :
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean:110:  refine ⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean:190:  · refine (natDegree_sum_le _ _).trans ?_
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean:222:  · refine (natDegree_sum_le _ _).trans ?_
Mathlib/Algebra/Polynomial/HasseDeriv.lean:179:    refine (natDegree_sum_le _ _).trans ?_
Mathlib/Algebra/Polynomial/Homogenize.lean:195:    exact (natDegree_prod_le _ _).trans (sum_le_sum h.2)
Mathlib/Algebra/Polynomial/BigOperators.lean:51:theorem natDegree_list_sum_le (l : List S[X]) :
Mathlib/Algebra/Polynomial/BigOperators.lean:57:theorem natDegree_multiset_sum_le (l : Multiset S[X]) :
Mathlib/Algebra/Polynomial/BigOperators.lean:59:  Quotient.inductionOn l (by simpa using natDegree_list_sum_le)
Mathlib/Algebra/Polynomial/BigOperators.lean:61:theorem natDegree_sum_le (f : ι → S[X]) :
Mathlib/Algebra/Polynomial/BigOperators.lean:63:  simpa using! natDegree_multiset_sum_le (s.val.map f)
Mathlib/Algebra/Polynomial/BigOperators.lean:65:lemma natDegree_sum_le_of_forall_le {n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) :
Mathlib/Algebra/Polynomial/BigOperators.lean:67:  le_trans (natDegree_sum_le s f) <| (Finset.fold_max_le n).mpr <| by simpa
Mathlib/Algebra/Polynomial/BigOperators.lean:81:    · aesop (add safe natDegree_sum_le_of_forall_le)
Mathlib/Algebra/Polynomial/BigOperators.lean:312:  · exact natDegree_sum_le_of_forall_le _ _ fun i hi ↦ (natDegree_smul_le _ _).trans <|

$ /bin/bash -lc "rg -n \"coeff_finset|coeff_sum.*Finset|map_sum.*coeff\" Mathlib/Algebra/Polynomial | head -100 && cat > /tmp/Test.lean <<'EOF'
import Mathlib
open scoped Polynomial BigOperators
open Finset
example {ι : Type*} [Fintype ι] (p : ι → ℤ[X]) (u : ℕ) :
  (∑ i, p i).coeff u = ∑ i, (p i).coeff u := by simp
EOF
lake env lean /tmp/Test.lean"

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:420:2: error: failed to synthesize
  CharZero ?α

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
ChampernowneA.lean:459:11: error: Function expected at
  Polynomial.natDegree_mul_le
but this term has type
  (?m.186 * ?m.187).natDegree ≤ Polynomial.natDegree ?m.186 + Polynomial.natDegree ?m.187

Note: Expected a function because this term is being applied to the argument
  _
ChampernowneA.lean:460:4: error: No goals to be solved
ChampernowneA.lean:469:6: error: Type mismatch: After simplification, term
  hc v uf
 has type
  ∑ x, c x * (-↑(h x)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑x)).coeff u = 0
but is expected to have type
  (∑ j, Polynomial.C (c j * (-↑(h j)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff u = 0
ChampernowneA.lean:477:10: error: Invalid rewrite argument: Expected an equality or iff proof or definition name, but `Q` is a value of type
  ℤ[X]

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
#check Int.cast_eq_zero
#check Int.cast_inj
#check Int.cast_injective
#check Polynomial.natDegree_mul_le
#check Polynomial.natDegree_C_mul_le
#check Polynomial.coeff_finset_sum
#check Polynomial.eval_finsetSum
EOF
lake env lean /tmp/Check.lean"
Int.cast_eq_zero.{u_3} {α : Type u_3} [AddGroupWithOne α] [CharZero α] {n : ℤ} : ↑n = 0 ↔ n = 0
Int.cast_inj.{u_3} {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m n : ℤ} : ↑m = ↑n ↔ m = n
Int.cast_injective.{u_3} {α : Type u_3} [AddGroupWithOne α] [CharZero α] : Function.Injective Int.cast
Polynomial.natDegree_mul_le.{u} {R : Type u} [Semiring R] {p q : Polynomial R} :
  (p * q).natDegree ≤ p.natDegree + q.natDegree
Polynomial.natDegree_C_mul_le.{u} {R : Type u} [Semiring R] (a : R) (f : Polynomial R) :
  (Polynomial.C a * f).natDegree ≤ f.natDegree
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.coeff_finset_sum`
Polynomial.eval_finsetSum.{u, y} {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (g : ι → Polynomial R) (x : R) :
  Polynomial.eval x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval x (g i)

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:456:34: error: unsolved goals
f : ℤ[X]
d : ℕ
hdeg : f.natDegree = d
h : Fin (d * (d + 1) + 1) → ℕ
c : Fin (d * (d + 1) + 1) → ℤ
hc :
  ∀ (v : Fin d) (u : Fin (d + 1)), ∑ j, c j * (-↑(h j)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff ↑u = 0
v : Fin d
n : ℤ
Q : ℤ[X] := ∑ j, Polynomial.C (c j * (-↑(h j)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑j)
j : Fin (d * (d + 1) + 1)
hj : j ∈ univ
⊢ d * (Polynomial.X + ↑↑j).natDegree ≤ d
ChampernowneA.lean:469:6: error: `simp` made no progress

$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
open scoped Polynomial
#check Polynomial.natDegree_X_add_C
#check Polynomial.natDegree_add_C
#check Polynomial.natDegree_X_add_C_eq_one
#check Polynomial.natDegree_X
EOF
lake env lean /tmp/Check.lean && nl -ba ChampernowneA.lean | sed -n '462,473p'"
Polynomial.natDegree_X_add_C.{u} {R : Type u} [Nontrivial R] [Semiring R] (x : R) :
  (Polynomial.X + Polynomial.C x).natDegree = 1
Polynomial.natDegree_add_C.{u} {R : Type u} [Semiring R] {p : R[X]} {a : R} :
  (p + Polynomial.C a).natDegree = p.natDegree
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.natDegree_X_add_C_eq_one`
Polynomial.natDegree_X.{u} {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.natDegree = 1

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '464,480p'"
464	    intro u
   465	    change Q.coeff u = 0
   466	    by_cases hu : u < d + 1
   467	    · let uf : Fin (d + 1) := ⟨u, hu⟩
   468	      dsimp [Q]
   469	      simp only [map_sum, Polynomial.coeff_C_mul]
   470	      exact hc v uf
   471	    · have hdu : d < u := by omega
   472	      exact (Polynomial.coeff_eq_zero_of_natDegree_lt
   473	        (lt_of_le_of_lt hQdeg hdu))
   474	  have heval : Q.eval n = 0 := by rw [hQ, Polynomial.eval_zero]
   475	  calc
   476	    ∑ j, c j * f.eval (n + (j : ℤ)) * (-(h j : ℤ)) ^ (v : ℕ) =
   477	        Q.eval n := by
   478	      change _ = Polynomial.eval n
   479	        (∑ j, Polynomial.C (c j * (-(h j : ℤ)) ^ (v : ℕ)) *
   480	          f.comp (Polynomial.X + Polynomial.C (j : ℤ)))

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:470:6: error: Type mismatch
  hc v uf
has type
  ∑ j, c j * (-↑(h j)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff ↑uf = 0
but is expected to have type
  (∑ j, Polynomial.C (c j * (-↑(h j)) ^ ↑v) * f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff u = 0

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:470:6: error: Type mismatch: After simplification, term
  hc v uf
 has type
  ∑ x, c x * (-↑(h x)) ^ ↑v * (f.comp (Polynomial.X + ↑↑x)).coeff ↑uf = 0
but is expected to have type
  ∑ b, (↑(c b) * (-↑(h b)) ^ ↑v * f.comp (Polynomial.X + ↑↑b)).coeff u = 0

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open scoped Polynomial BigOperators
#check Polynomial.natDegree_smul_le
#check Polynomial.coeff_smul
#check Polynomial.eval_smul
EOF
lake env lean /tmp/Check.lean"
Polynomial.natDegree_smul_le.{u, u_2} {R : Type u} [Semiring R] {S : Type u_2} [SMulZeroClass S R] (a : S) (p : R[X]) :
  (a • p).natDegree ≤ p.natDegree
Polynomial.coeff_smul.{u, v} {R : Type u} {S : Type v} [Semiring R] [SMulZeroClass S R] (r : S) (p : R[X]) (n : ℕ) :
  (r • p).coeff n = r • p.coeff n
Polynomial.eval_smul.{u, v} {R : Type u} {S : Type v} [Semiring R] [SMulZeroClass S R] [IsScalarTower S R R] (s : S)
  (p : R[X]) (x : R) : Polynomial.eval x (s • p) = s • Polynomial.eval x p

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:470:6: error: Type mismatch: After simplification, term
  hc v uf
 has type
  ∑ x, c x * (-↑(h x)) ^ ↑v * (f.comp (Polynomial.X + ↑↑x)).coeff ↑uf = 0
but is expected to have type
  ∑ b, (↑(c b) * (-↑(h b)) ^ ↑v * f.comp (Polynomial.X + ↑↑b)).coeff u = 0
Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
ChampernowneA.lean:477:20: error: unsolved goals
f : ℤ[X]
d : ℕ
hdeg : f.natDegree = d
h : Fin (d * (d + 1) + 1) → ℕ
c : Fin (d * (d + 1) + 1) → ℤ
hc :
  ∀ (v : Fin d) (u : Fin (d + 1)), ∑ j, c j * (-↑(h j)) ^ ↑v * (f.comp (Polynomial.X + Polynomial.C ↑↑j)).coeff ↑u = 0
v : Fin d
n : ℤ
Q : ℤ[X] := ∑ j, (c j * (-↑(h j)) ^ ↑v) • f.comp (Polynomial.X + Polynomial.C ↑↑j)
hQdeg : Q.natDegree ≤ d
hQ : Q = 0
heval : Polynomial.eval n Q = 0
j : Fin (d * (d + 1) + 1)
hj : j ∈ univ
⊢ c j * Polynomial.eval (n + ↑↑j) f * ↑(h j) ^ ↑v * (-1) ^ ↑v =
    c j * ↑(h j) ^ ↑v * Polynomial.eval (n + Polynomial.eval n (Polynomial.C ↑↑j)) f * (-1) 

$ /bin/bash -lc 'rg -n "def .*coeff.*Hom|lcoeff|coeffAdd" Mathlib/Algebra/Polynomial/Coeff.lean Mathlib/Algebra/Polynomial | head -120'
Mathlib/Algebra/Polynomial/Coeff.lean:80:def lcoeff (n : ℕ) : R[X] →ₗ[R] R where
Mathlib/Algebra/Polynomial/Coeff.lean:86:theorem lcoeff_apply (n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n :=
Mathlib/Algebra/Polynomial/Coeff.lean:92:  map_sum (lcoeff R n) _ _
Mathlib/Algebra/Polynomial/Coeff.lean:97:    l.sum.coeff n = (l.map (lcoeff R n)).sum :=
Mathlib/Algebra/Polynomial/Coeff.lean:98:  map_list_sum (lcoeff R n) _
Mathlib/Algebra/Polynomial/Coeff.lean:102:  simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
Mathlib/Algebra/Polynomial/Coeff.lean:294:  rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]
Mathlib/Algebra/Polynomial/Coeff.lean:295:  simp only [lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C]
Mathlib/Algebra/Polynomial/AlgebraMap.lean:198:lemma lcoeff_comp_mapAlgHom_eq (f : A →ₐ[R] B) (n : ℕ) :
Mathlib/Algebra/Polynomial/AlgebraMap.lean:199:    (lcoeff B n).restrictScalars R ∘ₗ (mapAlgHom f).toLinearMap =
Mathlib/Algebra/Polynomial/AlgebraMap.lean:200:      f.toLinearMap ∘ₗ (lcoeff A n).restrictScalars R := by
Mathlib/Algebra/Polynomial/OfFn.lean:34:noncomputable def toFn (n : ℕ) : R[X] →ₗ[R] Fin n → R := LinearMap.pi (fun i ↦ lcoeff R i)
Mathlib/Algebra/Polynomial/Taylor.lean:69:  show (lcoeff R n).comp (taylor r) f = (leval r).comp (hasseDeriv n) f by
Mathlib/Algebra/Polynomial/Taylor.lean:73:    simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C,
Mathlib/Algebra/Polynomial/Coeff.lean:80:def lcoeff (n : ℕ) : R[X] →ₗ[R] R where
Mathlib/Algebra/Polynomial/Coeff.lean:86:theorem lcoeff_apply (n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n :=
Mathlib/Algebra/Polynomial/Coeff.lean:92:  map_sum (lcoeff R n) _ _
Mathlib/Algebra/Polynomial/Coeff.lean:97:    l.sum.coeff n = (l.map (lcoeff R n)).sum :=
Mathlib/Algebra/Polynomial/Coeff.lean:98:  map_list_sum (lcoeff R n) _
Mathlib/Algebra/Polynomial/Coeff.lean:102:  simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
Mathlib/Algeb

$ /bin/bash -lc "sed -n '74,96p' Mathlib/Algebra/Polynomial/Coeff.lean"
map_smul' c p := by
    rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
    simp only [sum_def, Finset.smul_sum, coeff_smul, map_smul, RingHom.id_apply]

variable (R) in
/-- The nth coefficient, as a linear map. -/
def lcoeff (n : ℕ) : R[X] →ₗ[R] R where
  toFun p := coeff p n
  map_add' p q := coeff_add p q n
  map_smul' r p := coeff_smul r p n

@[simp]
theorem lcoeff_apply (n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n :=
  rfl

@[simp]
theorem finsetSum_coeff {ι : Type*} (s : Finset ι) (f : ι → R[X]) (n : ℕ) :
    coeff (∑ b ∈ s, f b) n = ∑ b ∈ s, coeff (f b) n :=
  map_sum (lcoeff R n) _ _

@[deprecated (since := "2026-04-08")] alias finset_sum_coeff := finsetSum_coeff

lemma coeff_list_sum (l : List R[X]) (n : ℕ) :

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:521:2: error: No goals to be solved
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:547:68: error: unexpected token ':='; expected ')', ',' or ':'
ChampernowneA.lean:526:30: error: unsolved goals
case hsingle
m : ℕ
f : ℤ[X]
hf : f ≠ 0
h : Fin (m + 1) → ℕ
hh : StrictMono h
c : Fin (m + 1) → ℤ
hc : c ≠ 0
j : Fin (m + 1)
hcj : c j ≠ 0
hzero : auxiliaryPhi f h c = 0
heval :
  ∑ i,
      Polynomial.eval (Polynomial.C (-↑(h j)))
        (Polynomial.C (Polynomial.C (c i) * f.comp (Polynomial.X + Polynomial.C ↑↑i)) *
          ∏ i ∈ univ.erase i, (Y + Polynomial.C (Polynomial.C ↑(h i)))) =
    0
⊢ ∑ l,
      Polynomial.eval (Polynomial.C (-↑(h j)))
        (Polynomial.C (Polynomial.C (c l) * f.comp (Polynomial.X + Polynomial.C ↑↑l)) *
         

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '512,570p' && cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Finset
#check Finset.prod_eq_zero
#check Finset.prod_eq_zero_iff
#check Finset.sum_eq_single
EOF
lake env lean /tmp/Check.lean"
Finset.prod_eq_zero.{u_1, u_4} {ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι}
  {i : ι} (hi : i ∈ s) (h : f i = 0) : ∏ j ∈ s, f j = 0
Finset.prod_eq_zero_iff.{u_1, u_4} {ι : Type u_1} {M₀ : Type u_4} [CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι}
  [Nontrivial M₀] [NoZeroDivisors M₀] : ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0
Finset.sum_eq_single.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι)
  (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) : ∑ x ∈ s, f x = f a

$ /bin/bash -lc "sed -n '514,554p' ChampernowneA.lean"
rw [auxiliaryPhi, Polynomial.evalEval_finsetSum]
  apply sum_congr rfl
  intro j hj
  simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C,
    Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_comp,
    Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod,
    Polynomial.evalEval_add, Polynomial.evalEval_X, Polynomial.evalEval_CC]
  ring

lemma auxiliaryPhi_ne_zero {m : ℕ} (f : ℤ[X]) (hf : f ≠ 0)
    (h : Fin (m + 1) → ℕ) (hh : StrictMono h)
    (c : Fin (m + 1) → ℤ) (hc : c ≠ 0) :
    auxiliaryPhi f h c ≠ 0 := by
  obtain ⟨j, hcj⟩ : ∃ j, c j ≠ 0 := by
    simpa only [ne_eq, funext_iff, not_forall, not_not, Pi.zero_apply] using hc
  intro hzero
  have heval :
      Polynomial.eval (Polynomial.C (-(h j : ℤ))) (auxiliaryPhi f h c) = 0 := by
    rw [hzero, Polynomial.eval_zero]
  rw [auxiliaryPhi, Polynomial.eval_finsetSum] at heval
  have hsingle :
      ∑ l,
          Polynomial.eval (Polynomial.C (-(h j : ℤ)))
            (Polynomial.C
                (Polynomial.C (c l) *
                  f.comp (Polynomial.X + Polynomial.C (l : ℤ))) *
              ∏ i ∈ Finset.univ.erase l,
                (Polynomial.X + Polynomial.C (Polynomial.C (h i : ℤ)))) =
        Polynomial.eval (Polynomial.C (-(h j : ℤ)))
          (Polynomial.C
              (Polynomial.C (c j) *
                f.comp (Polynomial.X + Polynomial.C (j : ℤ))) *
            ∏ i ∈ Finset.univ.erase j,
              (Polynomial.X + Polynomial.C (Polynomial.C (h i : ℤ))) := by
    apply Finset.sum_eq_single j
    · intro l hl hlj
      rw [Polynomial.eval_mul, Polynomial.eval_prod]
      apply mul_eq_zero_of_right
      apply Finset.prod_eq_zero (i := j)
      · exact Finset.mem_erase.mpr ⟨hlj, Finset.mem_univ _⟩
      · simp

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:552:36: error: Application type mismatch: The argument
  hlj
has type
  l ≠ j
but is expected to have type
  ?m.292 ≠ l
in the application
  And.intro hlj
ChampernowneA.lean:553:6: error: unsolved goals
case h
m : ℕ
f : ℤ[X]
hf : f ≠ 0
h : Fin (m + 1) → ℕ
hh : StrictMono h
c : Fin (m + 1) → ℤ
hc : c ≠ 0
j : Fin (m + 1)
hcj : c j ≠ 0
hzero : auxiliaryPhi f h c = 0
heval :
  ∑ i,
      Polynomial.eval (Polynomial.C (-↑(h j)))
        (Polynomial.C (Polynomial.C (c i) * f.comp (Polynomial.X + Polynomial.C ↑↑i)) *
          ∏ i ∈ univ.erase i, (Y + Polynomial.C (Polynomial.C ↑(h i)))) =
    0
l : Fin (m + 1)
hl : l ∈ univ
hlj : l ≠ j
⊢ -↑(h j) + ↑(h ?m.292) = 0
ChampernowneA.lean:570:4: error: omega could not pr

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:4: error: mod_cast has type
  Polynomial.C ↑(h i) = -Polynomial.C (-↑(h j))
but is expected to have type
  h i = h j
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:574:4: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  k ≤ -1
  g ≥ 0
  e ≥ 0
  e - g ≤ 0
  d ≥ 0
  d - e ≥ 1
  d - g ≤ 0
  b ≤ -1
  a ≥ 0
  a - b ≥ 0
where
 a := ↑(h i)
 b := Polynomial.coeff 0 0
 d := ↑↑j
 e := ↑↑i
 g := ↑m
 k := c j
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter
#check IsBigO.div_isLittleO
#check IsLittleO.div
#check IsLittleO.div_isEquivalent
#check IsBigO.div
#check IsLittleO.div_isBigO
#check IsLittleO.tendsto_zero
#check IsLittleO.tendsto_zero_of_tendsto_norm_atTop
#check IsLittleO.trans_isBigO
#check IsBigO.trans
#check IsEquivalent.add_isLittleO
#check IsLittleO.add_isEquivalent
EOF
lake env lean /tmp/Check.lean"
/tmp/Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsBigO.div_isLittleO`
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.div`
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.div_isEquivalent`
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsBigO.div`
/tmp/Check.lean:7:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.div_isBigO`
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.tendsto_zero`
/tmp/Check.lean:9:7: error(lean.unknownIdentifier): Unknown constant `Asymptotics.IsLittleO.tendsto_zero_of_tendsto_norm_atTop`
Asymptotics.IsLittleO.trans_isBigO.{u_1, u_3, u_4, u_8} {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8}
  [Norm E] [Norm F] [SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'} (hfg : f =o[l] g)
  (hgk : g =O[l] k) : f =o[l] k
Asymptotics.IsBigO.trans.{u_1, u_3, u_5, u_7} {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E]
  [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g)
  (hgk : g =O[l] k) : f =O[l] k
Asymptotics.IsEquivalent.add_isLittleO.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β}
  {l : Filter α} (huv : u ~[l] v) (hwv : w =o[l] v) : u + w ~[l] v
Asymptotics.IsLittleO.add_isEquivalent.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β}
  {l : Filter α} (hu : u =o[l] w) (hv : v ~[l] w) : u + v ~[l] w

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter Topology
#check isLittleO_iff_tendsto'
#check IsBigO.comp_tendsto
#check Polynomial.isEquivalent_atTop_lead
#check isLittleO_const_id_atTop
#check Filter.Tendsto.const_add
EOF
lake env lean /tmp/Check.lean"
Asymptotics.isLittleO_iff_tendsto'.{u_1, u_15} {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α}
  {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : f =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0)
Asymptotics.IsBigO.comp_tendsto.{u_1, u_2, u_3, u_4} {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4}
  [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (hfg : f =O[l] g) {k : β → α} {l' : Filter β}
  (hk : Tendsto k l' l) : (f ∘ k) =O[l'] (g ∘ k)
Polynomial.isEquivalent_atTop_lead.{u_1} {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  (P : Polynomial 𝕜) [OrderTopology 𝕜] :
  (fun x => Polynomial.eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree
Asymptotics.isLittleO_const_id_atTop.{u_9} {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') :
  (fun _x => c) =o[atTop] id
Filter.Tendsto.const_add.{u_1, u_2} {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M]
  {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Tendsto f x (𝓝 a)) :
  Tendsto (fun x => b + f x) x (𝓝 (b + a))

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Asymptotics Filter
#check isBigO_const_mul_self
#check isBigO_self_const_mul
#check IsBigO.const_mul_left
#check IsBigO.const_mul_right
#check IsBigOWith.const_mul_left
#check IsEquivalent.isBigO
#check Polynomial.natDegree_map_eq_of_injective
#check Polynomial.natDegree_map
EOF
lake env lean /tmp/Check.lean"
Asymptotics.isBigO_const_mul_self.{u_1, u_13} {α : Type u_1} {R : Type u_13} [SeminormedRing R] (c : R) (f : α → R)
  (l : Filter α) : (fun x => c * f x) =O[l] f
Asymptotics.isBigO_self_const_mul.{u_1, u_17} {α : Type u_1} {S : Type u_17} [NormedRing S] [NormMulClass S] {c : S}
  (hc : c ≠ 0) (f : α → S) (l : Filter α) : f =O[l] fun x => c * f x
Asymptotics.IsBigO.const_mul_left.{u_1, u_4, u_13} {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F]
  [SeminormedRing R] {g : α → F} {l : Filter α} {f : α → R} (h : f =O[l] g) (c' : R) : (fun x => c' * f x) =O[l] g
Asymptotics.IsBigO.const_mul_right.{u_1, u_3, u_17} {α : Type u_1} {E : Type u_3} [Norm E] {S : Type u_17}
  [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (hc : c ≠ 0) (h : f =O[l] g) :
  f =O[l] fun x => c * g x
Asymptotics.IsBigOWith.const_mul_left.{u_1, u_4, u_13} {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F]
  [SeminormedRing R] {c : ℝ} {g : α → F} {l : Filter α} {f : α → R} (h : IsBigOWith c l f g) (c' : R) :
  IsBigOWith (‖c'‖ * c) l (fun x => c' * f x) g
Asymptotics.IsEquivalent.isBigO.{u_1, u_2} {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β}
  {l : Filter α} (h : u ~[l] v) : u =O[l] v
Polynomial.natDegree_map_eq_of_injective.{u, v} {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S}
  (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).natDegree = p.natDegree
Polynomial.natDegree_map.{u, v} {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S]
  {p : Polynomial R} (f : R →+* S) : (Polynomial.map f p).natDegree = p.natDegree

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:602:6: error: linarith failed to find a contradiction
case succ.h1
p h : ℚ
hp : p ≠ 0
hph : p + h ≠ 0
d 

$ /bin/bash -lc 'rg -n "geom_sum.*(mul|sub)|sum_geom|geom.*sum" Mathlib/Algebra/GroupPower Mathlib | head -160'
rg: Mathlib/Algebra/GroupPower: No such file or directory (os error 2)
Mathlib/NumberTheory/EulerProduct/Basic.lean:285:lemma one_sub_inv_eq_geometric_of_summable_norm {f : ℕ →*₀ F} {p : ℕ} (hp : p.Prime)
Mathlib/NumberTheory/EulerProduct/Basic.lean:289:  refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm
Mathlib/NumberTheory/EulerProduct/Basic.lean:307:    exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2
Mathlib/NumberTheory/EulerProduct/Basic.lean:317:lemma prod_filter_prime_geometric_eq_tsum_factoredNumbers {f : ℕ →* F} (hsum : Summable f)
Mathlib/NumberTheory/EulerProduct/Basic.lean:320:  refine (summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm
Mathlib/NumberTheory/EulerProduct/Basic.lean:336:lemma prod_primesBelow_geometric_eq_tsum_smoothNumbers {f : ℕ →* F} (hsum : Summable f) (N : ℕ) :
Mathlib/NumberTheory/EulerProduct/Basic.lean:339:  exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _
Mathlib/NumberTheory/EulerProduct/Basic.lean:349:    funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum
Mathlib/NumberTheory/EulerProduct/Basic.lean:377:    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
Mathlib/NumberTheory/Basic.lean:37:    rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']
Mathlib/NumberTheory/Basic.lean:42:    rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
Mathlib/NumberTheory/Ostrowski.lean:68:  rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range,
Mathlib/NumberTheory/Multiplicity.lean:39:theorem dvd_geom_sum₂_iff_of_dvd_sub {x y p : R} (h : p ∣ x - y) :
Mathlib/NumberTheory/Multiplicity.lean:42:  simp only [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, h, geom_sum₂_self,
Mathlib/NumberTheory/Multiplicity.lean:45:theorem dvd_geom_sum₂_iff_of_dvd_sub' {x y p : R} (h : p ∣ x - y) :
Mathlib/NumberTheory/Multip

$ /bin/bash -lc "perl -0pi -e 's/\\(f\\.eval \\(\\(n : ℤ\\) \\+ \\(j : ℤ\\)\\) : ℚ\\)/((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ)/g' ChampernowneA.lean
rg -n \"f\\.eval.*: ℚ\" ChampernowneA.lean | tail -30"
613:    ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) /
615:      ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
623:    ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) /
625:        ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
637:          (∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
640:        ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
659:            (∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
668:            ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *

$ /bin/bash -lc "cat >/tmp/Geom.lean <<'EOF'
import Mathlib
open Finset
open scoped BigOperators
example (d : ℕ) {p h : ℚ} (hp : p ≠ 0) (hph : p+h ≠ 0) :
    1 / (p + h) =
      ∑ v ∈ range d, (-h) "'^ v / p ''^ (v + 1) +
        (-h) ''^ d / (p ''^ d * (p + h)) := by
  have hsum : (∑ v ∈ range d, (-h) ''^ v / p ''^ (v + 1)) =
      (1/p) * ∑ v ∈ range d, (-h/p)''^v := by
    rw [Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro v hv
    field_simp
    ring
  rw [hsum]
  have hg := geom_sum_mul (-h/p) d
  field_simp [hp, hph] at hg ⊢
  ring_nf at hg ⊢
  linear_combination hg
EOF
lake env lean /tmp/Geom.lean'
Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
/tmp/Geom.lean:9:41: error: unsolved goals
d : ℕ
p h : ℚ
hp : p ≠ 0
hph : p + h ≠ 0
v : ℕ
hv : v ∈ range d
⊢ h ^ v * p * (-1) ^ v = h ^ v * p * p ^ v * p⁻¹ ^ v * (-1) ^ v
/tmp/Geom.lean:19:2: error: ring failed, ring expressions not equal
d : ℕ
p h : ℚ
hp : p ≠ 0
hph : p + h ≠ 0
hsum : ∑ v ∈ range d, (-h) ^ v / p ^ (v + 1) = 1 / p * ∑ v ∈ range d, (-h / p) ^ v
hg :
  -(h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x) - p * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x =
    h ^ d * p * p⁻¹ ^ d * (-1) ^ d - p
⊢ -p + p * p ^ d - p * p ^ d * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x + p * h ^ d * p⁻¹ ^ d * (-1) ^ d -
            p * h ^ d * (-1) ^ d +
          p * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x -
        p ^ d * h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x +
      h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x =
    0

$ /bin/bash -lc "python3 - <<'PY'
p='/tmp/Geom.lean'
s=open(p).read().replace('    field_simp\\n    ring\\n','    rw [div_pow, pow_succ]\\n    field_simp\\n    ring\\n',1)
open(p,'w').write(s)
PY
lake env lean /tmp/Geom.lean"
/tmp/Geom.lean:15:4: error: No goals to be solved
/tmp/Geom.lean:20:2: error: ring failed, ring expressions not equal
d : ℕ
p h : ℚ
hp : p ≠ 0
hph : p + h ≠ 0
hsum : ∑ v ∈ range d, (-h) ^ v / p ^ (v + 1) = 1 / p * ∑ v ∈ range d, (-h / p) ^ v
hg :
  -(h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x) - p * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x =
    h ^ d * p * p⁻¹ ^ d * (-1) ^ d - p
⊢ -p + p * p ^ d - p * p ^ d * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x + p * h ^ d * p⁻¹ ^ d * (-1) ^ d -
            p * h ^ d * (-1) ^ d +
          p * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x -
        p ^ d * h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x +
      h * ∑ x ∈ range d, h ^ x * p⁻¹ ^ x * (-1) ^ x =
    0

$ /bin/bash -lc "cat >/tmp/Geom.lean <<'EOF'
import Mathlib
open Finset
open scoped BigOperators
example (d : ℕ) {p h : ℚ} (hp : p ≠ 0) (hph : p+h ≠ 0) :
    1 / (p + h) =
      ∑ v ∈ range d, (-h) "'^ v / p ''^ (v + 1) +
        (-h) ''^ d / (p ''^ d * (p + h)) := by
  have hsum : (∑ v ∈ range d, (-h) ''^ v / p ''^ (v + 1)) =
      (1/p) * ∑ v ∈ range d, (-h/p)''^v := by
    rw [Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro v hv
    rw [div_pow, pow_succ]
    field_simp
  rw [hsum]
  have hrem : (-h)''^d / (p''^d * (p+h)) = (-h/p)''^d / (p+h) := by
    rw [div_pow]
    field_simp
  rw [hrem]
  have hg := geom_sum_mul (-h/p) d
  have hg'"' : (∑ v ∈ range d, (-h/p)"'^v) * (1-(-h/p)) + (-h/p)''^d = 1 := by
    linarith
  have hr : 1-(-h/p) = (p+h)/p := by
    field_simp
    ring
  rw [hr] at hg'"'
  field_simp [hp, hph]
  exact hg'
EOF
lake env lean /tmp/Geom.lean"
/tmp/Geom.lean:28:2: error: Type mismatch
  hg'
has type
  (∑ v ∈ range d, (-h / p) ^ v) * ((p + h) / p) + (-h / p) ^ d = 1
but is expected to have type
  p = (p + h) * ∑ x ∈ range d, (-(h / p)) ^ x + p * (-(h / p)) ^ d

$ /bin/bash -lc "python3 - <<'PY'
p='/tmp/Geom.lean';s=open(p).read();s=s.replace('  rw [hr] at hg\\'\\n  field_simp [hp, hph]\\n  exact hg\\'\\n', \"  rw [hr] at hg'\\n  field_simp [hp] at hg'\\n  field_simp [hp, hph]\\n  nlinarith\\n\")
open(p,'w').write(s)
PY
lake env lean /tmp/Geom.lean"

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:650:26: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  1 / ?a
in the target

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:658:6: error: No goals to be solved
ChampernowneA.lean:670:10: error: Tactic `rewrite` failed: Did not f

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '648,678p'"
648	      apply sum_congr rfl
   649	      intro j hj
   650	      rw [div_eq_mul_inv]
   651	      rw [show ((nthPrime n : ℚ) + h j)⁻¹ =
   652	          ∑ v ∈ Finset.range d,
   653	              (-(h j : ℚ)) ^ v / (nthPrime n : ℚ) ^ (v + 1) +
   654	            (-(h j : ℚ)) ^ d /
   655	              ((nthPrime n : ℚ) ^ d * ((nthPrime n : ℚ) + h j)) by
   656	        simpa only [one_div] using
   657	          finite_geometric_reciprocal d hp (hph j)]
   658	      ring
   659	    _ =
   660	        (∑ v ∈ Finset.range d,
   661	          (∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
   662	            (-(h j : ℚ)) ^ v) /
   663	              (nthPrime n : ℚ) ^ (v + 1)) +
   664	        ∑ j, (c j : ℚ) * ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℚ) *
   665	          (-(h j : ℚ)) ^ d /
   666	            ((nthPrime n : ℚ) ^ d * ((nthPrime n : ℚ) + h j)) := by
   667	      simp_rw [mul_add]
   668	      rw [Finset.sum_add_distrib]
   669	      congr 1
   670	      rw [Finset.mul_sum, Finset.sum_comm]
   671	      apply sum_congr rfl
   672	      intro v hv
   673	      rw [Finset.sum_div]
   674	      apply congrArg (fun z : ℚ ↦ z / (nthPrime n : ℚ) ^ (v + 1))
   675	      apply sum_congr rfl
   676	      intro l hl
   677	      ring
   678	    _ = _ := by

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:687:10: error: Tactic `apply` failed: could not unify the conclusion of `congrArg fun z => z / ↑(nthPrim

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:686:12: error: Tactic `apply` failed: could not unify the conclusion of `sum_congr rfl`
  Finset.sum ?m.

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Filter
#check StrictMono.tendsto_atTop
#check tendsto_natCast_atTop_iff
#check tendsto_natCast_atTop_atTop
#check Polynomial.map_eval
#check Polynomial.eval_map
#check Polynomial.eval₂_at_apply
#check Polynomial.eval₂_hom
EOF
lake env lean /tmp/Check.lean"
StrictMono.tendsto_atTop {φ : ℕ → ℕ} (h : StrictMono φ) : Tendsto φ atTop atTop
tendsto_natCast_atTop_iff.{u_1, u_2} {α : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
  [Archimedean R] {f : α → ℕ} {l : Filter α} : Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
tendsto_natCast_atTop_atTop.{u_2} {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
  Tendsto Nat.cast atTop atTop
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.map_eval`
Polynomial.eval_map.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S)
  (x : S) : Polynomial.eval x (Polynomial.map f p) = Polynomial.eval₂ f x p
Polynomial.eval₂_at_apply.{u, u_1} {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S]
  (f : R →+* S) (r : R) : Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)
Polynomial.eval₂_hom.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S)
  (x : R) : Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Filter Topology Finset
#check Filter.Tendsto.finset_sum
#check tendsto_finset_sum
#check Filter.Tendsto.sum
#check tendsto_sum
EOF
lake env lean /tmp/Check.lean"
/tmp/Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Filter.Tendsto.finset_sum`
tendsto_finset_sum.{u_1, u_2, u_3} {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M]
  [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
  (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => ∑ c ∈ s, f c b) x (𝓝 (∑ c ∈ s, a c))
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Filter.Tendsto.sum`
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown identifier `tendsto_sum`

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:723:8: error: Invalid rewrite argument: Expected an equality or iff proof or definition name, but `P` is

$ /bin/bash -lc "nl -ba ChampernowneA.lean | sed -n '714,738p;792,806p;818,834p'"
714	
   715	lemma shifted_polynomial_eval_isBigO (f : ℤ[X]) (d : ℕ)
   716	    (hdeg : f.natDegree = d) (j : ℕ) :
   717	    (fun n : ℕ ↦ ((f.eval ((n : ℤ) + (j : ℤ)) : ℤ) : ℝ)) =O[atTop]
   718	      (fun n : ℕ ↦ (n : ℝ) ^ d) := by
   719	  let P : ℝ[X] :=
   720	    (f.map (Int.castRingHom ℝ)).comp
   721	      (Polynomial.X + Polynomial.C (j : ℝ))
   722	  have hPdeg : P.natDegree = d := by
   723	    rw [P, Polynomial.natDegree_comp,
   724	      Polynomial.natDegree_map_eq_of_injective Int.cast_injective,
   725	      hdeg, Polynomial.natDegree_X_add_C]
   726	    simp
   727	  have hOreal :
   728	      (fun x : ℝ ↦ P.eval x) =O[atTop] (fun x : ℝ ↦ x ^ P.natDegree) :=
   729	    P.isEquivalent_atTop_lead.isBigO.trans
   730	      (isBigO_const_mul_self P.leadingCoeff (fun x : ℝ ↦ x ^ P.natDegree) atTop)
   731	  have hOnat := hOreal.comp_tendsto (tendsto_natCast_atTop_atTop (R := ℝ))
   732	  refine hOnat.congr' (Eventually.of_forall fun n ↦ ?_)
   733	    (Eventually.of_forall fun n ↦ by rw [hPdeg])
   734	  simp only [Function.comp_apply, P, Polynomial.eval_comp, Polynomial.eval_add,
   735	    Polynomial.eval_X, Polynomial.eval_C, Polynomial.eval_map]
   736	  rw [show (n : ℝ) + (j : ℝ) = (((n : ℤ) + (j : ℤ) : ℤ) : ℝ) by norm_cast]
   737	  exact Polynomial.eval₂_at_apply _ _
   738	
   792	        (c : ℝ) * ((f.eval (n : ℤ) : ℤ) : ℝ) * (-(h : ℝ)) ^ d) =o[atTop]
   793	        (fun n : ℕ ↦
   794	          (nthPrime n : ℝ) ^ d * ((nthPrime n : ℝ) + h)) :=
   795	    (hnumO.trans_isLittleO hpowSmall).trans_isBigO hden.isBigO_symm
   796	  apply (isLittleO_iff_tendsto' ?_).mp hsmall
   797	  filter_upwards with n
   798	  intro hz
   799	  exfalso
   800	  have hp : (0 : ℝ) < nthPrime n := by positivity
   801	  have hph : (0 : ℝ) < nthPrime n + h := by positivity
   802	  exact (mul_pos (pow_pos hp _) hph).ne' hz
   803	
   804	/-- The complete remainder sum in (2.4) tends to zero. -/
   805	lemma remainder_sum_tendsto_zero (hPNT : PrimeNumberTheorem)
   806

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead

$ /bin/bash -lc 'rg -n "natAbs.*dvd|dvd.*natAbs|abs.*le.*dvd|le.*natAbs.*dvd" Mathlib/Data/Int Mathlib | head -160 && rg -n "natDegree_eq_zero.*C|eq_C.*natDegree|natDegree_eq_zero" Mathlib/Algebra/Polynomial | head -120'
Mathlib/Data/Int/NatPrime.lean:30:  have hpm' : p ^ k ∣ m.natAbs := Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpm
Mathlib/Data/Int/NatPrime.lean:31:  have hpn' : p ^ l ∣ n.natAbs := Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpn
Mathlib/Data/Int/NatPrime.lean:33:    rw [← Int.natAbs_mul]; apply Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpmn
Mathlib/Data/Int/NatPrime.lean:35:  hsd.elim (fun hsd1 => Or.inl (by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd1))
Mathlib/Data/Int/NatPrime.lean:36:    fun hsd2 => Or.inr (by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd2)
Mathlib/Data/Int/NatPrime.lean:38:theorem Prime.dvd_natAbs_of_coe_dvd_sq {p : ℕ} (hp : p.Prime) (k : ℤ) (h : (p : ℤ) ∣ k ^ 2) :
Mathlib/Data/Int/NatPrime.lean:41:  rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]
Mathlib/Data/Int/ModEq.lean:215:  · rw [gcd_div (gcd_dvd_left ..) (gcd_dvd_right ..), natAbs_natCast,
Mathlib/Data/Int/Basic.lean:72:lemma natCast_dvd {m : ℕ} : (m : ℤ) ∣ n ↔ m ∣ n.natAbs := by
Mathlib/Data/Int/Basic.lean:73:  obtain hn | hn := natAbs_eq n <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.dvd_neg]
Mathlib/Data/Int/Basic.lean:75:lemma dvd_natCast {n : ℕ} : m ∣ (n : ℤ) ↔ m.natAbs ∣ n := by
Mathlib/Data/Int/Basic.lean:76:  obtain hn | hn := natAbs_eq m <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.neg_dvd]
Mathlib/Data/Int/Basic.lean:79:  eq_zero_of_dvd_of_natAbs_lt_natAbs hnm (natAbs_lt_natAbs_of_nonneg_of_lt hm hmn)
Mathlib/Data/Int/Basic.lean:84:  Int.eq_of_sub_eq_zero (eq_zero_of_dvd_of_natAbs_lt_natAbs (dvd_self_sub_of_emod_eq h1) h2)
Mathlib/Data/Int/Basic.lean:86:lemma natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
Mathlib/Data/Int/Basic.lean:87:  not_lt.mp (mt (eq_zero_of_dvd_of_natAbs_lt_natAbs hmn) hn)
Mathlib/RingTheory/LittleWedderburn.lean:94:    refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
Mathlib/RingTheory/LittleWedderburn.lean:96:    · convert! Int.natAbs_dv

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Filter
#check Filter.eventually_atTop.1
#check eventually_atTop.2
#check Filter.Eventually.exists_forall_ge
#check tendsto_add_atTop_iff_nat
#check tendsto_atTop_add_const_right
#check Set.Infinite.exists_not_mem_finset
#check Set.Infinite.exists_mem_and_gt
#check Set.Infinite.exists_gt
EOF
lake env lean /tmp/Check.lean"
eventually_atTop.mp : (∀ᶠ (x : ?m.1) in atTop, ?m.4 x) → ∃ a, ∀ (b : ?m.1), a ≤ b → ?m.4 b
eventually_atTop.mpr : (∃ a, ∀ (b : ?m.1), a ≤ b → ?m.4 b) → ∀ᶠ (x : ?m.1) in atTop, ?m.4 x
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Filter.Eventually.exists_forall_ge`
Filter.tendsto_add_atTop_iff_nat.{u_3} {α : Type u_3} {f : ℕ → α} {l : Filter α} (k : ℕ) :
  Tendsto (fun n => f (n + k)) atTop l ↔ Tendsto f atTop l
Filter.tendsto_atTop_add_const_right.{u_1, u_2} {α : Type u_1} {G : Type u_2} [AddCommGroup G] [PartialOrder G]
  [IsOrderedAddMonoid G] (l : Filter α) {f : α → G} (C : G) (hf : Tendsto f l atTop) :
  Tendsto (fun x => f x + C) l atTop
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `Set.Infinite.exists_not_mem_finset`
/tmp/Check.lean:9:7: error(lean.unknownIdentifier): Unknown constant `Set.Infinite.exists_mem_and_gt`
Set.Infinite.exists_gt.{u_2} {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} (hs : s.Infinite)
  (a : α) : ∃ b ∈ s, a < b

$ /bin/bash -lc "rg -n \"map_ne_zero_iff|map_eq_zero_iff|map_injective\" Mathlib/Algebra/Polynomial | head -120 && cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Polynomial.map_injective
#check Polynomial.map_eq_zero_iff
#check Polynomial.map_ne_zero_iff
#check Polynomial.map_mapRingHom_evalEval
#check Polynomial.mapRingHom_injective
EOF
lake env lean /tmp/Check.lean"
Polynomial.map_injective.{u, v} {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S)
  (hf : Function.Injective ⇑f) : Function.Injective (Polynomial.map f)
Polynomial.map_eq_zero_iff.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S}
  (hf : Function.Injective ⇑f) : Polynomial.map f p = 0 ↔ p = 0
Polynomial.map_ne_zero_iff.{u, v} {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S}
  (hf : Function.Injective ⇑f) : Polynomial.map f p ≠ 0 ↔ p ≠ 0
Polynomial.map_mapRingHom_evalEval.{u_1, u_2} {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S)
  (p : Polynomial (Polynomial R)) (x y : R) :
  Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.evalEval x y p)
/tmp/Check.lean:6:7: error(lean.unknownIdentifier): Unknown constant `Polynomial.mapRingHom_injective`

$ /bin/bash -lc "rg -n \"abs_lt_one.*Int|Int.*abs.*one|eq_zero.*abs_lt|natAbs.*lt_one\" Mathlib/Data/Int Mathlib | head -100 && cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Int.natAbs_ofNat
#check Int.natAbs_eq_zero
#check Int.natAbs_pos
#check Int.eq_zero_of_abs_lt_one
#check Int.cast_abs
#check Int.cast_inj
EOF
lake env lean /tmp/Check.lean"
/tmp/Check.lean:2:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`
Int.natAbs_eq_zero {a : ℤ} : a.natAbs = 0 ↔ a = 0
Int.natAbs_pos {a : ℤ} : 0 < a.natAbs ↔ a ≠ 0
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Int.eq_zero_of_abs_lt_one`
Int.cast_abs.{u_1} {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : ℤ} : ↑|a| = |↑a|
Int.cast_inj.{u_3} {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m n : ℤ} : ↑m = ↑n ↔ m = n

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
open Finset
#check Finset.mul_prod_erase
#check Finset.prod_erase_mul
#check Finset.prod_erase_mul
#check Finset.prod_erase
#check Polynomial.map_mapRingHom_evalEval
EOF
lake env lean /tmp/Check.lean"
Finset.mul_prod_erase.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M)
  {a : ι} (h : a ∈ s) : f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
Finset.prod_erase_mul.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M)
  {a : ι} (h : a ∈ s) : (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
Finset.prod_erase_mul.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M)
  {a : ι} (h : a ∈ s) : (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
Finset.prod_erase.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) {f : ι → M}
  {a : ι} (h : f a = 1) : ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
Polynomial.map_mapRingHom_evalEval.{u_1, u_2} {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S)
  (p : Polynomial (Polynomial R)) (x y : R) :
  Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.evalEval x y p)

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead
ChampernowneA

$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Set.not_infinite
#check Set.not_infinite_iff_finite
#check Set.infinite_iff_not_finite
#check Set.Finite
#check dist_zero_right
#check Real.dist_eq
EOF
lake env lean /tmp/Check.lean"
Set.not_infinite.{u} {α : Type u} {s : Set α} : ¬s.Infinite ↔ s.Finite
/tmp/Check.lean:3:7: error(lean.unknownIdentifier): Unknown constant `Set.not_infinite_iff_finite`
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Set.infinite_iff_not_finite`
Set.Finite.{u} {α : Type u} (s : Set α) : Prop
dist_zero_right.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist a 0 = ‖a‖
Real.dist_eq (x y : ℝ) : dist x y = |x - y|

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead
ChampernowneA

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead
ChampernowneA

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead
ChampernowneA

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coeff_zero] at hz0

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:836:14: warning: `tendsto_finset_sum` has been deprecated: Use `tendsto_finsetSum` instead

$ /bin/bash -lc "rg -n '\\bsorry\\b|\\badmit\\b|"'^'"\\s*axiom\\b' ChampernowneA.lean README.md || true
git status --short
git diff --stat -- ChampernowneA.lean README.md
wc -l ChampernowneA.lean README.md
lake env lean ChampernowneA.lean"
M README.md
?? ChampernowneA.lean
 README.md | 228 +++++++++++++++++++++++++-------------------------------------
 1 file changed, 91 insertions(+), 137 deletions(-)
 1041 ChampernowneA.lean
  122 README.md
 1163 total
ChampernowneA.lean:289:6: warning: Try `simp at hq` instead of `simpa using hq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
ChampernowneA.lean:397:5: warning: Variable name `hdeg` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hdeg

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ChampernowneA.lean:422:22: warning: This simp argument is unused:
  Int.cast_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Int.cast_sum, Int.cast_mul, Int.cast_pow, Int.cast_neg, Int.cast_natCast]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:520:52: warning: This simp argument is unused:
  Polynomial.evalEval_CC

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.evalEval_mul, Polynomial.evalEval_C, Polynomial.eval_mul, Polynomial.eval_C,
    Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_X, Polynomial.evalEval_prod, Polynomial.evalEval_add,
    Polynomial.evalEval_X]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:568:13: warning: This simp argument is unused:
  Polynomial.C_eq_zero

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, ne_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ChampernowneA.lean:572:37: warning: This simp argument is unused:
  Polynomial.coeff_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [Polynomial.coeff_add, Polynomial.coeff_C_zero, Polynomial.coef

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'

$ /bin/bash -lc 'lake env lean AxiomAudit.lean'
AxiomAudit.lean:1:0: error: unknown module prefix 'ChampernowneA'

No directory 'ChampernowneA' or file 'ChampernowneA.olean' in the search path entries:
/work/repro/.lake/packages/Cli/.lake/build/lib/lean
/work/repro/.lake/packages/batteries/.lake/build/lib/lean
/work/repro/.lake/packages/Qq/.lake/build/lib/lean
/work/repro/.lake/packages/aesop/.lake/build/lib/lean
/work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean
/work/repro/.lake/packages/importGraph/.lake/build/lib/lean
/work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/work/repro/.lake/packages/plausible/.lake/build/lib/lean
/work/repro/.lake/build/lib/lean
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean

$ /bin/bash -lc 'lake env lean ChampernowneA.lean'
'ChampernowneA.theorem_1_1' depends on axioms: [propext, Classical.choice, Quot.sound]

$ /bin/bash -lc "rg -n '\\bsorry\\b|\\badmit\\b|"'^'"\\s*axiom\\b' ChampernowneA.lean || true
lake env lean ChampernowneA.lean
git status --short
git diff --check -- README.md ChampernowneA.lean
tail -35 README.md"
M README.md
?? ChampernowneA.lean
   polynomial.

5. `finite_geometric_reciprocal` proves the exact finite reciprocal expansion.
   `reciprocal_sum_eq_remainder` applies all cancellation equations, and
   `remainder_sum_tendsto_zero` proves the surviving remainder tends to zero.
   Divisibility on a recurring prime cluster makes the reciprocal sum an
   integer.  Its real norm is eventually less than one, so it is zero.

6. The resulting equality `Φ(n,p_n)=0` contradicts the PNT nonvanishing lemma.
   `infinitely_many_nthPrime_not_dvd` proves the zero-indexed form, and
   `theorem_1_1` shifts the polynomial by one to obtain the paper's exact
   one-indexed statement.

The degree-zero case is not split off: all definitions and estimates remain
valid for `d=0`, so the same proof covers nonzero constant polynomials.

## Verification

From this directory:

```bash
lake env lean ChampernowneA.lean
```

The command succeeds with Lean's exit code 0.  Integrity checks used for this
report:

```bash
rg -n '\bsorry\b|\badmit\b|^\s*axiom\b' ChampernowneA.lean
lake env lean ChampernowneA.lean
```

There are no `sorry`, `admit`, or locally declared axioms.  The only
unformalized mathematical inputs are the two explicit proposition parameters
`PrimeNumberTheorem` and `MaynardTaoBoundedGaps` above.