Open Proof Network

Problems / erdos-1050 / spec-ffd3137a

Padé numerator coefficient closed form

spec-ffd3137a erdos_1050_pade_numerator_closed_form

proved

Proposed by a contributor.

$\displaystyle \forall k\le n:\quad \sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\;=\;Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}}-\sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1}-\sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr)+\sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1}$

For any $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ fixed by hypothesis as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, and all natural numbers $k\le n$, the identity holds in $\mathbb{Q}$. Exponent subtractions are natural-number subtraction (none of $k-j$, $n+1+i-k$, $n-k$ truncates under $k\le n$) and $k(k-1)/2$ is natural-number division; on the left the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so the left side is in effect $p_k=\sum_{j<k}Q_c(n,j)/(2^{k-j}-1)$, and every denominator on the right is nonzero. The doc comment's 2-adic valuation claim is not part of the statement.

unverified · history

Lean
theorem erdos_1050_pade_numerator_closed_form : ∀ (Qc : ℕ → ℕ → ℚ),
    (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - 1) / 2) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - k - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) →
    ∀ n k : ℕ, k ≤ n →
      ∑ j ∈ Finset.range (k + 1), Qc n j / ((2 : ℚ) ^ (k - j) - 1) =
        Qc n k * (∑ i ∈ Finset.range n, 1 / (1 - (2 : ℚ) ^ (n + 1 + i - k)) -
            ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) -
            ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1))) +
          ∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/8fb80b6847ea….md, written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06.

Overview

Draft · drafted, by the model named above

The proof is a partial-fraction computation evaluated at a pole. Take the nodes $x_l = 2^l$ ($0 \le l \le n$), the points $y_i = 2^{n+1+i}$ ($0 \le i < n$), and weights $w_j = Q_c(n,j)\,2^j$. Three general facts are proved first, then specialised: a residue identity for the weights (lag_test), the partial-fraction expansion of $\prod_i (X - y_i)$ over the nodes (pf_test), and its derivative at one node (pf2_test). The specialisation (hpf) gives $$\sum_{j \ne k}\frac{Q_c(n,j)2^j}{2^k - 2^j} = Q_c(n,k)\,2^k\Bigl(\sum_{i<n}\frac{1}{2^k - 2^{n+1+i}} - \sum_{l \ne k}\frac{1}{2^k-2^l}\Bigr),$$ and steps T0 to T3 rewrite each piece into the form of the statement. The final line is linear_combination hpf - T1 + T2 - T3, after T0.

Read it step by step (5 more sections)

The residue identity

Draft · drafted, by the model named above

lag_test: for $j \le n$, $Q_c(n,j)\cdot 2^j\cdot\prod_{l<j}(2^j-2^l)\cdot\prod_{s<n-j}(2^j-2^{j+1+s}) = \prod_{i<n}(2^j - 2^{n+1+i})$, with $Q_c(n,j)$ written out. Each product is evaluated: $\prod_{l<j}(2^j-2^l) = 2^{j(j-1)/2}\prod_{s<j}(2^{s+1}-1)$ (lag_test.hb, factoring $2^j - 2^l = 2^l(2^{j-l}-1)$, lag_test.hb.h1); $\prod_{s<n-j}(2^j - 2^{j+1+s}) = (-2^j)^{n-j}\prod_{s<n-j}(2^{s+1}-1)$ (lag_test.hc); $\prod_{i<n}(2^j-2^{n+1+i}) = (-2^j)^n\prod_{i<n}(2^{n+1+i-j}-1)$ (lag_test.hd). lag_test.he merges $\prod_{i<j}(2^{n-i}-1)$ and $\prod_{s<n-j}(2^{s+1}-1)$ into $\prod_{s<n}(2^{s+1}-1)$; lag_test.hf reindexes $\prod_{i<n}(2^{2n-j-i}-1)$ as $\prod_{i<n}(2^{n+1+i-j}-1)$. The sign and power bookkeeping is lag_test.hjj ($j\cdot j = 2\lfloor j(j-1)/2\rfloor + j$) and lag_test.hpow ($(-2^j)^n$ split into the factors that appear). With the denominators nonzero (lag_test.hpos, lag_test.hF, lag_test.hB), field_simp and ring close it.

Partial fractions over the nodes

Draft · drafted, by the model named above

pf_test, for arbitrary rational $x$, $y$, $w$ with the $x_0,\dots,x_n$ distinct: if $w_j\prod_{l\ne j}(x_j - x_l) = \prod_{i<n}(x_j - y_i)$ for every $j \le n$, then, as polynomials, $\sum_{j\le n} w_j\prod_{l \ne j}(X - x_l) = \prod_{i<n}(X - y_i)$. Both sides have degree at most $n$ (pf_test.hL, pf_test.hE; the degree bound is pf_test.s3), so it is enough that they agree at the $n+1$ distinct points $x_j$ (pf_test.s4). At $X = x_j$ only the $j$-th summand on the left survives, the others containing the factor $x_j - x_j = 0$, and the hypothesis is exactly the equality there.

The derivative at a node

Draft · drafted, by the model named above

pf2_test: under the same hypotheses, and with $x_k \ne y_i$ for all $i$, $$\sum_{j \ne k}\frac{w_j}{x_k - x_j} = w_k\Bigl(\sum_{i<n}\frac{1}{x_k-y_i} - \sum_{l\ne k}\frac{1}{x_k - x_l}\Bigr).$$ It differentiates the polynomial identity of pf_test (pf2_test.hLE) and evaluates at $x_k$ (pf2_test.hd). Let $P = \prod_{l\ne k}(x_k - x_l)$, nonzero by distinctness (pf2_test.hne, pf2_test.hP0). On the left, a summand with $j \ne k$ contributes $w_j P/(x_k - x_j)$ (pf2_test.h1, summed in pf2_test.h1'), and the summand $j = k$ contributes $w_k P\sum_{m\ne k}1/(x_k-x_m)$ (pf2_test.h2). On the right the derivative of $\prod_i(X - y_i)$ at $x_k$ is $\prod_i(x_k-y_i)\sum_i 1/(x_k-y_i)$, which is $w_k P \sum_i 1/(x_k-y_i)$ by the hypothesis at $j=k$ (pf2_test.h3). Cancelling $P$ gives the identity.

Specialising to the nodes 2^l

Draft · drafted, by the model named above

hc unfolds $Q_c$. Then the hypotheses of pf2_test are checked for $x_l = 2^l$, $y_i = 2^{n+1+i}$, $w_j = Q_c(n,j)2^j$: the nodes are distinct because $l \mapsto 2^l$ is injective (hinj, hx); $2^k \ne 2^{n+1+i}$ because $k \le n$ (hxy); and the weight condition hw is lag_test after splitting $\prod_{l \ne j}(2^j - 2^l)$ into $l<j$ and $l = j+1+s$ (hw.e1 to hw.e3). hpf is the result, displayed in the overview. Supporting facts: $k \le n$ (hk1), powers of two are nonzero (h2), $2^{b+1}-1 \ne 0$ and $1-2^{b+1} \ne 0$ (hs1, hs1'), and $2^{k-j}-1 \ne 0$ for $j<k$ (hpk).

Matching the statement

Draft · drafted, by the model named above

T0: the term $j = k$ of the statement's sum divides by $2^0-1 = 0$ and is $0$, so the sum is over $j<k$. T1: the left side of hpf splits into $j<k$, where $\frac{Q_c(n,j)2^j}{2^k-2^j} = \frac{Q_c(n,j)}{2^{k-j}-1}$ (T1.ga), and $j = k+1+b$ with $b < n-k$, where it equals $-\frac{Q_c(n,k+b+1)2^{b+1}}{2^{b+1}-1}$ (T1.gb). T2: $Q_c(n,k)2^k\sum_i \frac{1}{2^k-2^{n+1+i}} = Q_c(n,k)\sum_i\frac{1}{1-2^{n+1+i-k}}$. T3a splits $\sum_{l\ne k}\frac{1}{2^k-2^l}$ into $l<k$ and $l = k+1+b$; T3b gives $2^k\sum_{l<k}\frac{1}{2^k-2^l} = \sum_{b<k}\frac{2^{b+1}}{2^{b+1}-1}$ (each term is $\frac{2^{k-l}}{2^{k-l}-1}$, T3b.e1, then reindexed); T3c gives $2^k\sum_{b<n-k}\frac{1}{2^k-2^{k+1+b}} = \sum_{b<n-k}\frac{1}{1-2^{b+1}}$; T3 combines them. Substituting T1, T2, T3 into hpf and rearranging is the statement.

Improve these words →

History: 1 version on record

  1. 2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · current · explainer/8fb80b6847ea….md · the first version of its chain

    Read this version

    Overview

    The proof is a partial-fraction computation evaluated at a pole. Take the nodes $x_l = 2^l$ ($0 \le l \le n$), the points $y_i = 2^{n+1+i}$ ($0 \le i < n$), and weights $w_j = Q_c(n,j)\,2^j$. Three general facts are proved first, then specialised: a residue identity for the weights (lag_test), the partial-fraction expansion of $\prod_i (X - y_i)$ over the nodes (pf_test), and its derivative at one node (pf2_test). The specialisation (hpf) gives $$\sum_{j \ne k}\frac{Q_c(n,j)2^j}{2^k - 2^j} = Q_c(n,k)\,2^k\Bigl(\sum_{i<n}\frac{1}{2^k - 2^{n+1+i}} - \sum_{l \ne k}\frac{1}{2^k-2^l}\Bigr),$$ and steps T0 to T3 rewrite each piece into the form of the statement. The final line is linear_combination hpf - T1 + T2 - T3, after T0.

    The residue identity (lag_test lag_test.hpos lag_test.hpos.this lag_test.hpos.this.s1 lag_test.hpos.this.s2 lag_test.hb lag_test.hb.h1 lag_test.hb.h1.hl' lag_test.hb.h1.this lag_test.hb.hs' lag_test.hc lag_test.hc.s1 lag_test.hc.s2 lag_test.hd lag_test.hd.s1 lag_test.hd.s2 lag_test.he lag_test.he.hn lag_test.he.ht' lag_test.hf lag_test.hf.hi' lag_test.hF lag_test.hB lag_test.hjj lag_test.hjj.h2 lag_test.hjj.s2 lag_test.hjj.s3 lag_test.hpow)

    lag_test: for $j \le n$, $Q_c(n,j)\cdot 2^j\cdot\prod_{l<j}(2^j-2^l)\cdot\prod_{s<n-j}(2^j-2^{j+1+s}) = \prod_{i<n}(2^j - 2^{n+1+i})$, with $Q_c(n,j)$ written out. Each product is evaluated: $\prod_{l<j}(2^j-2^l) = 2^{j(j-1)/2}\prod_{s<j}(2^{s+1}-1)$ (lag_test.hb, factoring $2^j - 2^l = 2^l(2^{j-l}-1)$, lag_test.hb.h1); $\prod_{s<n-j}(2^j - 2^{j+1+s}) = (-2^j)^{n-j}\prod_{s<n-j}(2^{s+1}-1)$ (lag_test.hc); $\prod_{i<n}(2^j-2^{n+1+i}) = (-2^j)^n\prod_{i<n}(2^{n+1+i-j}-1)$ (lag_test.hd). lag_test.he merges $\prod_{i<j}(2^{n-i}-1)$ and $\prod_{s<n-j}(2^{s+1}-1)$ into $\prod_{s<n}(2^{s+1}-1)$; lag_test.hf reindexes $\prod_{i<n}(2^{2n-j-i}-1)$ as $\prod_{i<n}(2^{n+1+i-j}-1)$. The sign and power bookkeeping is lag_test.hjj ($j\cdot j = 2\lfloor j(j-1)/2\rfloor + j$) and lag_test.hpow ($(-2^j)^n$ split into the factors that appear). With the denominators nonzero (lag_test.hpos, lag_test.hF, lag_test.hB), field_simp and ring close it.

    Partial fractions over the nodes (pf_test pf_test.hL pf_test.hE pf_test.s3 pf_test.s3.s1 pf_test.s3.s2 pf_test.s4 pf_test.s4.s1 pf_test.s4.s2 pf_test.s4.s3 pf_test.s4.s4)

    pf_test, for arbitrary rational $x$, $y$, $w$ with the $x_0,\dots,x_n$ distinct: if $w_j\prod_{l\ne j}(x_j - x_l) = \prod_{i<n}(x_j - y_i)$ for every $j \le n$, then, as polynomials, $\sum_{j\le n} w_j\prod_{l \ne j}(X - x_l) = \prod_{i<n}(X - y_i)$. Both sides have degree at most $n$ (pf_test.hL, pf_test.hE; the degree bound is pf_test.s3), so it is enough that they agree at the $n+1$ distinct points $x_j$ (pf_test.s4). At $X = x_j$ only the $j$-th summand on the left survives, the others containing the factor $x_j - x_j = 0$, and the hypothesis is exactly the equality there.

    The derivative at a node (pf2_test pf2_test.hLE pf2_test.hne pf2_test.hP0 pf2_test.hd pf2_test.h1 pf2_test.h1.hjs pf2_test.h1.hjk pf2_test.h1.hks pf2_test.h1.s4 pf2_test.h1.s4.this pf2_test.h1.s5 pf2_test.h1.s6 pf2_test.h2 pf2_test.h2.this pf2_test.h3 pf2_test.h3.this pf2_test.h1')

    pf2_test: under the same hypotheses, and with $x_k \ne y_i$ for all $i$, $$\sum_{j \ne k}\frac{w_j}{x_k - x_j} = w_k\Bigl(\sum_{i<n}\frac{1}{x_k-y_i} - \sum_{l\ne k}\frac{1}{x_k - x_l}\Bigr).$$ It differentiates the polynomial identity of pf_test (pf2_test.hLE) and evaluates at $x_k$ (pf2_test.hd). Let $P = \prod_{l\ne k}(x_k - x_l)$, nonzero by distinctness (pf2_test.hne, pf2_test.hP0). On the left, a summand with $j \ne k$ contributes $w_j P/(x_k - x_j)$ (pf2_test.h1, summed in pf2_test.h1'), and the summand $j = k$ contributes $w_k P\sum_{m\ne k}1/(x_k-x_m)$ (pf2_test.h2). On the right the derivative of $\prod_i(X - y_i)$ at $x_k$ is $\prod_i(x_k-y_i)\sum_i 1/(x_k-y_i)$, which is $w_k P \sum_i 1/(x_k-y_i)$ by the hypothesis at $j=k$ (pf2_test.h3). Cancelling $P$ gives the identity.

    Specialising to the nodes 2^l (hc hk1 h2 hs1 hs1.this hs1.this.s1 hs1.this.s2 hs1' hinj hinj.this hx hxy hxy.this hw hw.hjn hw.e1 hw.e2 hw.e3 hw.e3.ga hw.e3.ga.this hw.e3.gb hpf hpk)

    hc unfolds $Q_c$. Then the hypotheses of pf2_test are checked for $x_l = 2^l$, $y_i = 2^{n+1+i}$, $w_j = Q_c(n,j)2^j$: the nodes are distinct because $l \mapsto 2^l$ is injective (hinj, hx); $2^k \ne 2^{n+1+i}$ because $k \le n$ (hxy); and the weight condition hw is lag_test after splitting $\prod_{l \ne j}(2^j - 2^l)$ into $l<j$ and $l = j+1+s$ (hw.e1 to hw.e3). hpf is the result, displayed in the overview. Supporting facts: $k \le n$ (hk1), powers of two are nonzero (h2), $2^{b+1}-1 \ne 0$ and $1-2^{b+1} \ne 0$ (hs1, hs1'), and $2^{k-j}-1 \ne 0$ for $j<k$ (hpk).

    Matching the statement (T0 T1 T1.e1 T1.ga T1.ga.hjk T1.gb T1.gb.this T2 T2.e T2.this T3a T3a.e1 T3a.ha T3a.ha.this T3a.hb T3b T3b.e1 T3b.e1.hlk T3b.this T3c T3c.this T3)

    T0: the term $j = k$ of the statement's sum divides by $2^0-1 = 0$ and is $0$, so the sum is over $j<k$. T1: the left side of hpf splits into $j<k$, where $\frac{Q_c(n,j)2^j}{2^k-2^j} = \frac{Q_c(n,j)}{2^{k-j}-1}$ (T1.ga), and $j = k+1+b$ with $b < n-k$, where it equals $-\frac{Q_c(n,k+b+1)2^{b+1}}{2^{b+1}-1}$ (T1.gb). T2: $Q_c(n,k)2^k\sum_i \frac{1}{2^k-2^{n+1+i}} = Q_c(n,k)\sum_i\frac{1}{1-2^{n+1+i-k}}$. T3a splits $\sum_{l\ne k}\frac{1}{2^k-2^l}$ into $l<k$ and $l = k+1+b$; T3b gives $2^k\sum_{l<k}\frac{1}{2^k-2^l} = \sum_{b<k}\frac{2^{b+1}}{2^{b+1}-1}$ (each term is $\frac{2^{k-l}}{2^{k-l}-1}$, T3b.e1, then reindexed); T3c gives $2^k\sum_{b<n-k}\frac{1}{2^k-2^{k+1+b}} = \sum_{b<n-k}\frac{1}{1-2^{b+1}}$; T3 combines them. Substituting T1, T2, T3 into hpf and rearranging is the statement.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000311, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000311.json, merge commit 1e6a4209cd14.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. lag_test have ∀ (n j : ℕ), j ≤ n → ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i))

    Leaves ∀ (Qc : ℕ → ℕ → ℚ), (Qc = fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) → ∀ (n k : ℕ), k ≤ n → ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with lag_test : ∀ (n j : ℕ), j ≤ n → ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_div_distrib.

    Lean, lines 21–108
      have lag_test : ∀ (n j : ℕ), j ≤ n →
        (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
          ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * 2 ^ j *
        (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
        ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) := by
    intro n j hj
    have hpos : ∀ s : ℕ, (2 : ℚ) ^ (s + 1) - 1 ≠ 0 := by
      intro s
      have : (2 : ℚ) ≤ 2 ^ (s + 1) := by
        calc (2 : ℚ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    -- (b) the nodes below j
    have hb : ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) =
        (2 : ℚ) ^ (j * (j - 1) / 2) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) := by
      have h1 : ∀ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) = 2 ^ l * ((2 : ℚ) ^ (j - l) - 1) := by
        intro l hl
        have hl' := Finset.mem_range.mp hl
        have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega
        rw [this]; ring
      rw [Finset.prod_congr rfl h1, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
        Finset.sum_range_id]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun s hs => ?_)
      have hs' := Finset.mem_range.mp hs
      congr 2
      omega
    -- (c) the nodes above j
    have hc : ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
        (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) := by
      calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s))
          = ∏ s ∈ Finset.range (n - j), ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (s + 1) - 1)) := by
            refine Finset.prod_congr rfl (fun s _ => ?_)
            rw [show j + 1 + s = j + (s + 1) by omega, pow_add]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
    -- (d) the right side
    have hd : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) =
        (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i))
          = ∏ i ∈ Finset.range n, ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (n + 1 + i - j) - 1)) := by
            refine Finset.prod_congr rfl (fun i _ => ?_)
            rw [show n + 1 + i = j + (n + 1 + i - j) by omega, pow_add, Nat.add_sub_cancel_left]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
    -- (e) the q-factorial splits at j
    have he : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1)) *
        ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) =
        ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) := by
      have hn : n = (n - j) + j := by omega
      conv_rhs => rw [hn]
      rw [Finset.prod_range_add, mul_comm]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun t ht => ?_)
      have ht' := Finset.mem_range.mp ht
      congr 2
      omega
    -- (f) reflect the second Gaussian binomial's numerator
    have hf : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) =
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun i hi => ?_)
      have hi' := Finset.mem_range.mp hi
      congr 2
      omega
    have hF : ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
    have hB : ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
    have hjj : j * j = j * (j - 1) / 2 + j * (j - 1) / 2 + j := by
      have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
      rcases j with _ | j
      · simp
      · simp only [Nat.add_sub_cancel] at h2 ⊢
        linarith
    have hpow : (-(2 : ℚ) ^ j) ^ n = (-1) ^ j * 2 ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j *
        (-(2 : ℚ) ^ j) ^ (n - j) := by
      rw [show n = j + (n - j) by omega, pow_add, Nat.add_sub_cancel_left, neg_pow, ← pow_mul, hjj,
        pow_add, pow_add]
      ring
    rw [Finset.prod_div_distrib, Finset.prod_div_distrib, hb, hc, hd, hf, hpow]
    field_simp
    rw [← he]
    ring

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 21–108 at 1e6a4209cd14 ↗

    1. lag_test.hpos have ∀ (s : ℕ), (2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ)

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hpos : ∀ (s : ℕ), (2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ).

      Lean, lines 29–34
          have hpos : ∀ s : ℕ, (2 : ℚ) ^ (s + 1) - 1 ≠ 0 := by
      intro s
      have : (2 : ℚ) ≤ 2 ^ (s + 1) := by
        calc (2 : ℚ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 29–34 at 1e6a4209cd14 ↗

      1. lag_test.hpos.this have (2 : ℚ) ≤ (2 : ℚ) ^ (s + (1 : ℕ))

        Leaves (2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ), with this : (2 : ℚ) ≤ (2 : ℚ) ^ (s + (1 : ℕ)).

        Lean, lines 31–33
              have : (2 : ℚ) ≤ 2 ^ (s + 1) := by
        calc (2 : ℚ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 31–33 at 1e6a4209cd14 ↗

        1. lag_test.hpos.this.s1 calc (2 : ℚ) = (2 : ℚ) ^ (1 : ℕ) routine: norm_num

          Closes the goal.

          Lean, line 32
                  calc (2 : ℚ) = 2 ^ 1 := by norm_num

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 32 at 1e6a4209cd14 ↗

        2. lag_test.hpos.this.s2 calc (2 : ℚ) ^ (1 : ℕ) ≤ (2 : ℚ) ^ (s + (1 : ℕ))

          Closes the goal.

          Uses library pow_le_pow_right₀.

          Lean, line 33
                    _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 33 at 1e6a4209cd14 ↗

    2. lag_test.hb have ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l) = (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ))

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hb : ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l) = (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, Finset.sum_range_id Gauss' summation formula , Finset.prod_range_reflect.

      Lean, lines 36–50
          have hb : ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) =
        (2 : ℚ) ^ (j * (j - 1) / 2) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) := by
      have h1 : ∀ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) = 2 ^ l * ((2 : ℚ) ^ (j - l) - 1) := by
        intro l hl
        have hl' := Finset.mem_range.mp hl
        have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega
        rw [this]; ring
      rw [Finset.prod_congr rfl h1, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
        Finset.sum_range_id]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun s hs => ?_)
      have hs' := Finset.mem_range.mp hs
      congr 2
      omega

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 36–50 at 1e6a4209cd14 ↗

      1. lag_test.hb.h1 have ∀ l ∈ Finset.range j, (2 : ℚ) ^ j - (2 : ℚ) ^ l = (2 : ℚ) ^ l * ((2 : ℚ) ^ (j - l) - (1 : ℚ))

        Leaves ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l) = (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)), with h1 : ∀ l ∈ Finset.range j, (2 : ℚ) ^ j - (2 : ℚ) ^ l = (2 : ℚ) ^ l * ((2 : ℚ) ^ (j - l) - (1 : ℚ)).

        Uses library Finset.range range n is the set of natural numbers less than n. .

        Lean, lines 38–42
              have h1 : ∀ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) = 2 ^ l * ((2 : ℚ) ^ (j - l) - 1) := by
        intro l hl
        have hl' := Finset.mem_range.mp hl
        have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega
        rw [this]; ring

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 38–42 at 1e6a4209cd14 ↗

        1. lag_test.hb.h1.hl' have l < j

          Leaves (2 : ℚ) ^ j - (2 : ℚ) ^ l = (2 : ℚ) ^ l * ((2 : ℚ) ^ (j - l) - (1 : ℚ)), with hl' : l < j.

          Uses library Finset.mem_range.

          Lean, line 40
                  have hl' := Finset.mem_range.mp hl

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 40 at 1e6a4209cd14 ↗

        2. lag_test.hb.h1.this have (2 : ℚ) ^ j = (2 : ℚ) ^ l * (2 : ℚ) ^ (j - l)

          Leaves (2 : ℚ) ^ j - (2 : ℚ) ^ l = (2 : ℚ) ^ l * ((2 : ℚ) ^ (j - l) - (1 : ℚ)), with this : (2 : ℚ) ^ j = (2 : ℚ) ^ l * (2 : ℚ) ^ (j - l).

          Uses library pow_add.

          Lean, line 41
                  have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 41 at 1e6a4209cd14 ↗

      2. lag_test.hb.hs' have s < j

        Leaves (2 : ℚ) ^ (j - (j - (1 : ℕ) - s)) - (1 : ℚ) = (2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ), with hs' : s < j.

        Uses library Finset.mem_range.

        Lean, line 48
              have hs' := Finset.mem_range.mp hs

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 48 at 1e6a4209cd14 ↗

    3. lag_test.hc have ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ))

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hc : ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. .

      Lean, lines 52–59
          have hc : ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
        (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) := by
      calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s))
          = ∏ s ∈ Finset.range (n - j), ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (s + 1) - 1)) := by
            refine Finset.prod_congr rfl (fun s _ => ?_)
            rw [show j + 1 + s = j + (s + 1) by omega, pow_add]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 52–59 at 1e6a4209cd14 ↗

      1. lag_test.hc.s1 calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ s ∈ Finset.range (n - j), -(2 : ℚ) ^ j * ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ))

        Closes the goal.

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , pow_add.

        Lean, lines 54–58
              calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s))
          = ∏ s ∈ Finset.range (n - j), ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (s + 1) - 1)) := by
            refine Finset.prod_congr rfl (fun s _ => ?_)
            rw [show j + 1 + s = j + (s + 1) by omega, pow_add]
            ring

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 54–58 at 1e6a4209cd14 ↗

      2. lag_test.hc.s2 calc

        Closes the goal.

        Uses library Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range.

        Lean, line 59
                _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 59 at 1e6a4209cd14 ↗

    4. lag_test.hd have ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ))

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hd : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. .

      Lean, lines 61–68
          have hd : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) =
        (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i))
          = ∏ i ∈ Finset.range n, ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (n + 1 + i - j) - 1)) := by
            refine Finset.prod_congr rfl (fun i _ => ?_)
            rw [show n + 1 + i = j + (n + 1 + i - j) by omega, pow_add, Nat.add_sub_cancel_left]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 61–68 at 1e6a4209cd14 ↗

      1. lag_test.hd.s1 calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = ∏ i ∈ Finset.range n, -(2 : ℚ) ^ j * ((2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ))

        Closes the goal.

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , pow_add, Nat.add_sub_cancel_left.

        Lean, lines 63–67
              calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i))
          = ∏ i ∈ Finset.range n, ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (n + 1 + i - j) - 1)) := by
            refine Finset.prod_congr rfl (fun i _ => ?_)
            rw [show n + 1 + i = j + (n + 1 + i - j) by omega, pow_add, Nat.add_sub_cancel_left]
            ring

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 63–67 at 1e6a4209cd14 ↗

      2. lag_test.hd.s2 calc

        Closes the goal.

        Uses library Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range.

        Lean, line 68
                _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 68 at 1e6a4209cd14 ↗

    5. lag_test.he have (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ))) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) = ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ))

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with he : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ))) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) = ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_range_add, mul_comm, Finset.prod_range_reflect, Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 70–81
          have he : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1)) *
        ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) =
        ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) := by
      have hn : n = (n - j) + j := by omega
      conv_rhs => rw [hn]
      rw [Finset.prod_range_add, mul_comm]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun t ht => ?_)
      have ht' := Finset.mem_range.mp ht
      congr 2
      omega

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 70–81 at 1e6a4209cd14 ↗

      1. lag_test.he.hn have n = n - j + j routine: omega

        Leaves (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ))) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) = ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)), with hn : n = n - j + j.

        Lean, line 73
              have hn : n = (n - j) + j := by omega

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 73 at 1e6a4209cd14 ↗

      2. lag_test.he.ht' have t < j

        Leaves (2 : ℚ) ^ (n - (j - (1 : ℕ) - t)) - (1 : ℚ) = (2 : ℚ) ^ (n - j + t + (1 : ℕ)) - (1 : ℚ), with ht' : t < j.

        Uses library Finset.mem_range.

        Lean, line 79
              have ht' := Finset.mem_range.mp ht

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 79 at 1e6a4209cd14 ↗

    6. lag_test.hf have ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ))

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hf : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_range_reflect, Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 83–89
          have hf : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) =
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun i hi => ?_)
      have hi' := Finset.mem_range.mp hi
      congr 2
      omega

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 83–89 at 1e6a4209cd14 ↗

      1. lag_test.hf.hi' have i < n

        Leaves (2 : ℚ) ^ ((2 : ℕ) * n - j - (n - (1 : ℕ) - i)) - (1 : ℚ) = (2 : ℚ) ^ (n + (1 : ℕ) + i - j) - (1 : ℚ), with hi' : i < n.

        Uses library Finset.mem_range.

        Lean, line 87
              have hi' := Finset.mem_range.mp hi

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 87 at 1e6a4209cd14 ↗

    7. lag_test.hF have ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hF : ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_ne_zero_iff.

      Lean, lines 90–91
          have hF : ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 90–91 at 1e6a4209cd14 ↗

    8. lag_test.hB have ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ)

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hB : ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + (1 : ℕ)) - (1 : ℚ)) ≠ (0 : ℚ).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_ne_zero_iff.

      Lean, lines 92–93
          have hB : ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 92–93 at 1e6a4209cd14 ↗

    9. lag_test.hjj have j * j = j * (j - (1 : ℕ)) / (2 : ℕ) + j * (j - (1 : ℕ)) / (2 : ℕ) + j

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hjj : j * j = j * (j - (1 : ℕ)) / (2 : ℕ) + j * (j - (1 : ℕ)) / (2 : ℕ) + j.

      Lean, lines 94–99
          have hjj : j * j = j * (j - 1) / 2 + j * (j - 1) / 2 + j := by
      have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
      rcases j with _ | j
      · simp
      · simp only [Nat.add_sub_cancel] at h2 ⊢
        linarith

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 94–99 at 1e6a4209cd14 ↗

      1. lag_test.hjj.h2 have (2 : ℕ) * (j * (j - (1 : ℕ)) / (2 : ℕ)) = j * (j - (1 : ℕ))

        Leaves j * j = j * (j - (1 : ℕ)) / (2 : ℕ) + j * (j - (1 : ℕ)) / (2 : ℕ) + j, with h2 : (2 : ℕ) * (j * (j - (1 : ℕ)) / (2 : ℕ)) = j * (j - (1 : ℕ)).

        Uses library Nat.two_mul_div_two_of_even, Nat.even_mul_pred_self.

        Lean, line 95
              have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 95 at 1e6a4209cd14 ↗

      2. lag_test.hjj.s2 case routine: simp

        Leaves (0 : ℕ) * (0 : ℕ) = (0 : ℕ) * ((0 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (0 : ℕ) * ((0 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (0 : ℕ).

        Lean, line 97
              · simp

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 97 at 1e6a4209cd14 ↗

      3. lag_test.hjj.s3 case routine: simp, linarith

        Leaves (j + (1 : ℕ)) * (j + (1 : ℕ)) = (j + (1 : ℕ)) * (j + (1 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (j + (1 : ℕ)) * (j + (1 : ℕ) - (1 : ℕ)) / (2 : ℕ) + (j + (1 : ℕ)).

        Uses library Nat.add_sub_cancel.

        Lean, lines 98–99
              · simp only [Nat.add_sub_cancel] at h2 ⊢
        linarith

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 98–99 at 1e6a4209cd14 ↗

    10. lag_test.hpow have (-(2 : ℚ) ^ j) ^ n = (-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ j * (-(2 : ℚ) ^ j) ^ (n - j)

      Leaves ((((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * (2 : ℚ) ^ j * ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)) = ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + i)), with hpow : (-(2 : ℚ) ^ j) ^ n = (-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * (2 : ℚ) ^ j * (-(2 : ℚ) ^ j) ^ (n - j).

      Uses library pow_add, Nat.add_sub_cancel_left, neg_pow, pow_mul.

      Lean, lines 100–104
          have hpow : (-(2 : ℚ) ^ j) ^ n = (-1) ^ j * 2 ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j *
        (-(2 : ℚ) ^ j) ^ (n - j) := by
      rw [show n = j + (n - j) by omega, pow_add, Nat.add_sub_cancel_left, neg_pow, ← pow_mul, hjj,
        pow_add, pow_add]
      ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 100–104 at 1e6a4209cd14 ↗

  2. pf_test have ∀ (n : ℕ) (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), x a = x b → a = b) → (∀ j ∈ Finset.range (n + (1 : ℕ)), w j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) → ∑ j ∈ Finset.range (n + (1 : ℕ)), (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))

    Leaves ∀ (Qc : ℕ → ℕ → ℚ), (Qc = fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) → ∀ (n k : ℕ), k ≤ n → ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with pf_test : ∀ (n : ℕ) (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), x a = x b → a = b) → (∀ j ∈ Finset.range (n + (1 : ℕ)), w j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) → ∑ j ∈ Finset.range (n + (1 : ℕ)), (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Polynomial.C C a is the constant polynomial a. , Polynomial.X X is the polynomial variable (aka indeterminate). , Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq.

    Lean, lines 110–138
      have pf_test : ∀ (n : ℕ) (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1), x a = x b → a = b) →
        (∀ j ∈ Finset.range (n + 1),
          w j * ∏ l ∈ (Finset.range (n + 1)).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) →
        (∑ j ∈ Finset.range (n + 1), Polynomial.C (w j) * ∏ l ∈ (Finset.range (n + 1)).erase j, (X - Polynomial.C (x l))) =
        ∏ i ∈ Finset.range n, (X - Polynomial.C (y i)) := by
    intro n x y w hx hw
    set s := Finset.range (n + 1) with hs
    have hL : (∑ j ∈ s, Polynomial.C (w j) * ∏ l ∈ s.erase j, (X - Polynomial.C (x l))).natDegree ≤ n := by
      refine natDegree_sum_le_of_forall_le _ _ (fun j hj => ?_)
      refine (natDegree_C_mul_le _ _).trans ((natDegree_prod_le _ _).trans ?_)
      simp only [natDegree_X_sub_C, Finset.sum_const, smul_eq_mul, mul_one]
      rw [Finset.card_erase_of_mem hj, hs, Finset.card_range]
      omega
    have hE : (∏ i ∈ Finset.range n, (X - Polynomial.C (y i))).natDegree ≤ n := by
      refine (natDegree_prod_le _ _).trans ?_
      simp [natDegree_X_sub_C]
    apply Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq (s.image x)
    · rw [Finset.card_image_of_injOn (fun a ha b hb h => hx a ha b hb h), hs, Finset.card_range]
      refine lt_of_le_of_lt (degree_sub_le _ _) (max_lt ?_ ?_)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hL) (by exact_mod_cast Nat.lt_succ_self n)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hE) (by exact_mod_cast Nat.lt_succ_self n)
    · intro z hz
      obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hz
      simp only [eval_finset_sum, eval_mul, eval_C, eval_prod, eval_sub, eval_X]
      rw [Finset.sum_eq_single j]
      · exact hw j hj
      · intro i hi hij
        rw [Finset.prod_eq_zero (i := j) (Finset.mem_erase.mpr ⟨Ne.symm hij, hj⟩) (sub_self _), mul_zero]
      · intro hj'; exact absurd hj hj'

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 110–138 at 1e6a4209cd14 ↗

    1. pf_test.hL have (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l))).natDegree ≤ n

      Leaves ∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i)), with hL : (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l))).natDegree ≤ n.

      Uses library Polynomial.C C a is the constant polynomial a. , Polynomial.X X is the polynomial variable (aka indeterminate). , Polynomial.natDegree_sum_le_of_forall_le, Polynomial.natDegree_C_mul_le, Polynomial.natDegree_prod_le, Polynomial.natDegree_X_sub_C, Finset.sum_const, smul_eq_mul, mul_one, Finset.card_erase_of_mem $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. , Finset.card_range.

      Lean, lines 117–122
          have hL : (∑ j ∈ s, Polynomial.C (w j) * ∏ l ∈ s.erase j, (X - Polynomial.C (x l))).natDegree ≤ n := by
      refine natDegree_sum_le_of_forall_le _ _ (fun j hj => ?_)
      refine (natDegree_C_mul_le _ _).trans ((natDegree_prod_le _ _).trans ?_)
      simp only [natDegree_X_sub_C, Finset.sum_const, smul_eq_mul, mul_one]
      rw [Finset.card_erase_of_mem hj, hs, Finset.card_range]
      omega

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 117–122 at 1e6a4209cd14 ↗

    2. pf_test.hE have (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))).natDegree ≤ n

      Leaves ∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i)), with hE : (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))).natDegree ≤ n.

      Uses library Finset.range range n is the set of natural numbers less than n. , Polynomial.X X is the polynomial variable (aka indeterminate). , Polynomial.C C a is the constant polynomial a. , Polynomial.natDegree_prod_le, Polynomial.natDegree_X_sub_C.

      Lean, lines 123–125
          have hE : (∏ i ∈ Finset.range n, (X - Polynomial.C (y i))).natDegree ≤ n := by
      refine (natDegree_prod_le _ _).trans ?_
      simp [natDegree_X_sub_C]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 123–125 at 1e6a4209cd14 ↗

    3. pf_test.s3 case

      Leaves (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) - ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))).degree < (↑(Finset.image x s).card : WithBot ℕ).

      Uses library Finset.card_image_of_injOn, Finset.card_range, lt_of_le_of_lt, Polynomial.degree_sub_le, max_lt.

      Lean, lines 127–130
          · rw [Finset.card_image_of_injOn (fun a ha b hb h => hx a ha b hb h), hs, Finset.card_range]
      refine lt_of_le_of_lt (degree_sub_le _ _) (max_lt ?_ ?_)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hL) (by exact_mod_cast Nat.lt_succ_self n)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hE) (by exact_mod_cast Nat.lt_succ_self n)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 127–130 at 1e6a4209cd14 ↗

      1. pf_test.s3.s1 case

        Leaves (∑ j ∈ Finset.range (n + (1 : ℕ)), (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l))).degree < (↑(n + (1 : ℕ)) : WithBot ℕ).

        Uses library lt_of_le_of_lt, Polynomial.degree_le_of_natDegree_le Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le. , Nat.lt_succ_self.

        Lean, line 129
              · exact lt_of_le_of_lt (degree_le_of_natDegree_le hL) (by exact_mod_cast Nat.lt_succ_self n)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 129 at 1e6a4209cd14 ↗

      2. pf_test.s3.s2 case

        Leaves (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))).degree < (↑(n + (1 : ℕ)) : WithBot ℕ).

        Uses library lt_of_le_of_lt, Polynomial.degree_le_of_natDegree_le Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le. , Nat.lt_succ_self.

        Lean, line 130
              · exact lt_of_le_of_lt (degree_le_of_natDegree_le hE) (by exact_mod_cast Nat.lt_succ_self n)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 130 at 1e6a4209cd14 ↗

    4. pf_test.s4 case

      Leaves ∀ x_1 ∈ Finset.image x s, Polynomial.eval x_1 (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l))) = Polynomial.eval x_1 (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))).

      Uses library Polynomial.eval_finset_sum Alias of Polynomial.eval_finsetSum. , Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_prod Polynomial evaluation commutes with Finset.prod , Polynomial.eval_sub, Polynomial.eval_X, Finset.sum_eq_single.

      Lean, lines 131–138
          · intro z hz
      obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hz
      simp only [eval_finset_sum, eval_mul, eval_C, eval_prod, eval_sub, eval_X]
      rw [Finset.sum_eq_single j]
      · exact hw j hj
      · intro i hi hij
        rw [Finset.prod_eq_zero (i := j) (Finset.mem_erase.mpr ⟨Ne.symm hij, hj⟩) (sub_self _), mul_zero]
      · intro hj'; exact absurd hj hj'

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 131–138 at 1e6a4209cd14 ↗

      1. pf_test.s4.s1 obtain ∃ a ∈ s, x a = z

        Leaves Polynomial.eval (x j) (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l))) = Polynomial.eval (x j) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))), with j : ℕ, hj : j ∈ s, hz : x j ∈ Finset.image x s.

        Uses library Finset.mem_image.

        Lean, line 132
              obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hz

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 132 at 1e6a4209cd14 ↗

      2. pf_test.s4.s2 case

        Leaves w j * ∏ x_1 ∈ s.erase j, (x j - x x_1) = ∏ x_1 ∈ Finset.range n, (x j - y x_1).

        Lean, line 135
              · exact hw j hj

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 135 at 1e6a4209cd14 ↗

      3. pf_test.s4.s3 case

        Leaves ∀ b ∈ s, b ≠ j → w b * ∏ x_1 ∈ s.erase b, (x j - x x_1) = (0 : ℚ).

        Uses library Finset.prod_eq_zero, Finset.mem_erase, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , Ne.symm, sub_self, MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

        Lean, lines 136–137
              · intro i hi hij
        rw [Finset.prod_eq_zero (i := j) (Finset.mem_erase.mpr ⟨Ne.symm hij, hj⟩) (sub_self _), mul_zero]

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 136–137 at 1e6a4209cd14 ↗

      4. pf_test.s4.s4 case

        Leaves j ∉ s → w j * ∏ x_1 ∈ s.erase j, (x j - x x_1) = (0 : ℚ).

        Uses library absurd Anything follows from two contradictory hypotheses. .

        Lean, line 138
              · intro hj'; exact absurd hj hj'

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 138 at 1e6a4209cd14 ↗

  3. pf2_test have ∀ (n k : ℕ), k ∈ Finset.range (n + (1 : ℕ)) → ∀ (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), x a = x b → a = b) → (∀ i ∈ Finset.range n, x k - y i ≠ (0 : ℚ)) → (∀ j ∈ Finset.range (n + (1 : ℕ)), w j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) → ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / (x k - x l))

    Leaves ∀ (Qc : ℕ → ℕ → ℚ), (Qc = fun (n k : ℕ) => ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - k - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) → ∀ (n k : ℕ), k ≤ n → ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with pf2_test : ∀ (n k : ℕ), k ∈ Finset.range (n + (1 : ℕ)) → ∀ (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), x a = x b → a = b) → (∀ i ∈ Finset.range n, x k - y i ≠ (0 : ℚ)) → (∀ j ∈ Finset.range (n + (1 : ℕ)), w j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) → ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / (x k - x l)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Polynomial.derivative_sum, Polynomial.derivative_mul, Polynomial.derivative_C, MulZeroClass.zero_mul Zero is a left absorbing element for multiplication , zero_add, Polynomial.derivative_prod_finset, Polynomial.derivative_sub, Polynomial.derivative_X, sub_zero, mul_one, Polynomial.eval_finset_sum Alias of Polynomial.eval_finsetSum. , Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_prod Polynomial evaluation commutes with Finset.prod , Polynomial.eval_sub, Polynomial.eval_X, Finset.add_sum_erase Taking a sum over s : Finset ι is the same as adding the value on a single element f a to the sum over s.erase a. , mul_left_cancel₀.

    Lean, lines 140–204
      have pf2_test : ∀ (n k : ℕ), k ∈ Finset.range (n + 1) → ∀ (x y w : ℕ → ℚ),
        (∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1), x a = x b → a = b) →
        (∀ i ∈ Finset.range n, x k - y i ≠ 0) →
        (∀ j ∈ Finset.range (n + 1),
          w j * ∏ l ∈ (Finset.range (n + 1)).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) →
        ∑ j ∈ (Finset.range (n + 1)).erase k, w j / (x k - x j) =
        w k * (∑ i ∈ Finset.range n, 1 / (x k - y i) -
          ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / (x k - x l)) := by
    intro n k hk x y w hx hxy hw
    have hLE := pf_test n x y w hx hw
    set s := Finset.range (n + 1) with hs
    have hne : ∀ j ∈ s, j ≠ k → x k - x j ≠ 0 := by
      intro j hj hjk h
      exact hjk (hx j hj k hk (sub_eq_zero.mp h).symm)
    set P := ∏ l ∈ s.erase k, (x k - x l) with hP
    have hP0 : P ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun l hl =>
      hne l (Finset.mem_of_mem_erase hl) (Finset.ne_of_mem_erase hl))
    have hd := congrArg (fun p => (derivative p).eval (x k)) hLE
    simp only [derivative_sum, derivative_mul, derivative_C, zero_mul, zero_add, derivative_prod_finset,
      derivative_sub, derivative_X, sub_zero, mul_one, eval_finset_sum, eval_mul, eval_C, eval_prod,
      eval_sub, eval_X] at hd
    -- the terms j ≠ k
    have h1 : ∀ j ∈ s.erase k, (∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l)) =
        P * (1 / (x k - x j)) := by
      intro j hj
      have hjs := Finset.mem_of_mem_erase hj
      have hjk := Finset.ne_of_mem_erase hj
      have hks : k ∈ s.erase j := Finset.mem_erase.mpr ⟨Ne.symm hjk, hk⟩
      rw [Finset.sum_eq_single k]
      · have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hj
        rw [Finset.erase_right_comm]
        field_simp [hne j hjs hjk]
        rw [hP, ← this]
        ring
      · intro m hm hmk
        exact Finset.prod_eq_zero (i := k) (Finset.mem_erase.mpr ⟨Ne.symm hmk, hks⟩) (sub_self _)
      · intro h; exact absurd hks h
    -- the term j = k
    have h2 : (∑ m ∈ s.erase k, ∏ l ∈ (s.erase k).erase m, (x k - x l)) =
        P * ∑ m ∈ s.erase k, 1 / (x k - x m) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun m hm => ?_)
      have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hm
      field_simp [hne m (Finset.mem_of_mem_erase hm) (Finset.ne_of_mem_erase hm)]
      rw [hP, ← this]
      ring
    -- the right side
    have h3 : (∑ i ∈ Finset.range n, ∏ i' ∈ (Finset.range n).erase i, (x k - y i')) =
        (w k * P) * ∑ i ∈ Finset.range n, 1 / (x k - y i) := by
      rw [hw k hk, Finset.mul_sum]
      refine Finset.sum_congr rfl (fun i hi => ?_)
      have := Finset.mul_prod_erase (Finset.range n) (fun i' => x k - y i') hi
      field_simp [hxy i hi]
      rw [← this]
      ring
    rw [← Finset.add_sum_erase s _ hk, h2, h3] at hd
    have h1' : ∑ j ∈ s.erase k, w j * ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) =
        P * ∑ j ∈ s.erase k, w j / (x k - x j) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun j hj => ?_)
      rw [h1 j hj]
      ring
    rw [h1'] at hd
    apply mul_left_cancel₀ hP0
    linear_combination hd

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 140–204 at 1e6a4209cd14 ↗

    1. pf2_test.hLE have ∑ j ∈ Finset.range (n + (1 : ℕ)), (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))

      Leaves ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / (x k - x l)), with hLE : ∑ j ∈ Finset.range (n + (1 : ℕ)), (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)) = ∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i)).

      Lean, line 149
          have hLE := pf_test n x y w hx hw

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 149 at 1e6a4209cd14 ↗

    2. pf2_test.hne have ∀ j ∈ s, j ≠ k → x k - x j ≠ (0 : ℚ)

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with hne : ∀ j ∈ s, j ≠ k → x k - x j ≠ (0 : ℚ).

      Uses library sub_eq_zero.

      Lean, lines 151–153
          have hne : ∀ j ∈ s, j ≠ k → x k - x j ≠ 0 := by
      intro j hj hjk h
      exact hjk (hx j hj k hk (sub_eq_zero.mp h).symm)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 151–153 at 1e6a4209cd14 ↗

    3. pf2_test.hP0 have P ≠ (0 : ℚ)

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with hP0 : P ≠ (0 : ℚ).

      Uses library Finset.prod_ne_zero_iff, Finset.mem_of_mem_erase, Finset.ne_of_mem_erase.

      Lean, lines 155–156
          have hP0 : P ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun l hl =>
      hne l (Finset.mem_of_mem_erase hl) (Finset.ne_of_mem_erase hl))

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 155–156 at 1e6a4209cd14 ↗

    4. pf2_test.hd have Polynomial.eval (x k) ((Polynomial.derivative : Polynomial ℚ → Polynomial ℚ) (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)))) = Polynomial.eval (x k) ((Polynomial.derivative : Polynomial ℚ → Polynomial ℚ) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i))))

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with hd : Polynomial.eval (x k) ((Polynomial.derivative : Polynomial ℚ → Polynomial ℚ) (∑ j ∈ s, (Polynomial.C : ℚ → Polynomial ℚ) (w j) * ∏ l ∈ s.erase j, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (x l)))) = Polynomial.eval (x k) ((Polynomial.derivative : Polynomial ℚ → Polynomial ℚ) (∏ i ∈ Finset.range n, (Polynomial.X - (Polynomial.C : ℚ → Polynomial ℚ) (y i)))).

      Uses library congrArg Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. , Polynomial.derivative derivative p is the formal derivative of the polynomial p .

      Lean, line 157
          have hd := congrArg (fun p => (derivative p).eval (x k)) hLE

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 157 at 1e6a4209cd14 ↗

    5. pf2_test.h1 have ∀ j ∈ s.erase k, ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x j))

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with h1 : ∀ j ∈ s.erase k, ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x j)).

      Uses library Finset.sum_eq_single.

      Lean, lines 162–176
          have h1 : ∀ j ∈ s.erase k, (∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l)) =
        P * (1 / (x k - x j)) := by
      intro j hj
      have hjs := Finset.mem_of_mem_erase hj
      have hjk := Finset.ne_of_mem_erase hj
      have hks : k ∈ s.erase j := Finset.mem_erase.mpr ⟨Ne.symm hjk, hk⟩
      rw [Finset.sum_eq_single k]
      · have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hj
        rw [Finset.erase_right_comm]
        field_simp [hne j hjs hjk]
        rw [hP, ← this]
        ring
      · intro m hm hmk
        exact Finset.prod_eq_zero (i := k) (Finset.mem_erase.mpr ⟨Ne.symm hmk, hks⟩) (sub_self _)
      · intro h; exact absurd hks h

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 162–176 at 1e6a4209cd14 ↗

      1. pf2_test.h1.hjs have j ∈ s

        Leaves ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x j)), with hjs : j ∈ s.

        Uses library Finset.mem_of_mem_erase.

        Lean, line 165
              have hjs := Finset.mem_of_mem_erase hj

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 165 at 1e6a4209cd14 ↗

      2. pf2_test.h1.hjk have j ≠ k

        Leaves ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x j)), with hjk : j ≠ k.

        Uses library Finset.ne_of_mem_erase.

        Lean, line 166
              have hjk := Finset.ne_of_mem_erase hj

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 166 at 1e6a4209cd14 ↗

      3. pf2_test.h1.hks have k ∈ s.erase j

        Leaves ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x j)), with hks : k ∈ s.erase j.

        Uses library Finset.mem_erase, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , Ne.symm.

        Lean, line 167
              have hks : k ∈ s.erase j := Finset.mem_erase.mpr ⟨Ne.symm hjk, hk⟩

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 167 at 1e6a4209cd14 ↗

      4. pf2_test.h1.s4 case

        Leaves ∏ l ∈ (s.erase j).erase k, (x k - x l) = P * ((1 : ℚ) / (x k - x j)).

        Uses library Finset.erase_right_comm.

        Lean, lines 169–173
              · have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hj
        rw [Finset.erase_right_comm]
        field_simp [hne j hjs hjk]
        rw [hP, ← this]
        ring

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 169–173 at 1e6a4209cd14 ↗

        1. pf2_test.h1.s4.this have (x k - x j) * ∏ x_1 ∈ (s.erase k).erase j, (x k - x x_1) = ∏ x_1 ∈ s.erase k, (x k - x x_1)

          Leaves ∏ l ∈ (s.erase j).erase k, (x k - x l) = P * ((1 : ℚ) / (x k - x j)), with this : (x k - x j) * ∏ x_1 ∈ (s.erase k).erase j, (x k - x x_1) = ∏ x_1 ∈ s.erase k, (x k - x x_1).

          Uses library Finset.mul_prod_erase Taking a product over s : Finset ι is the same as multiplying the value on a single element f a by the product of s.erase a. .

          Lean, line 169
                · have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hj

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 169 at 1e6a4209cd14 ↗

      5. pf2_test.h1.s5 case

        Leaves ∀ b ∈ s.erase j, b ≠ k → ∏ l ∈ (s.erase j).erase b, (x k - x l) = (0 : ℚ).

        Uses library Finset.prod_eq_zero, Finset.mem_erase, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , Ne.symm, sub_self.

        Lean, lines 174–175
              · intro m hm hmk
        exact Finset.prod_eq_zero (i := k) (Finset.mem_erase.mpr ⟨Ne.symm hmk, hks⟩) (sub_self _)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 174–175 at 1e6a4209cd14 ↗

      6. pf2_test.h1.s6 case

        Leaves k ∉ s.erase j → ∏ l ∈ (s.erase j).erase k, (x k - x l) = (0 : ℚ).

        Uses library absurd Anything follows from two contradictory hypotheses. .

        Lean, line 176
              · intro h; exact absurd hks h

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 176 at 1e6a4209cd14 ↗

    6. pf2_test.h2 have ∑ m ∈ s.erase k, ∏ l ∈ (s.erase k).erase m, (x k - x l) = P * ∑ m ∈ s.erase k, (1 : ℚ) / (x k - x m)

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with h2 : ∑ m ∈ s.erase k, ∏ l ∈ (s.erase k).erase m, (x k - x l) = P * ∑ m ∈ s.erase k, (1 : ℚ) / (x k - x m).

      Uses library Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , Finset.mem_of_mem_erase, Finset.ne_of_mem_erase.

      Lean, lines 178–185
          have h2 : (∑ m ∈ s.erase k, ∏ l ∈ (s.erase k).erase m, (x k - x l)) =
        P * ∑ m ∈ s.erase k, 1 / (x k - x m) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun m hm => ?_)
      have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hm
      field_simp [hne m (Finset.mem_of_mem_erase hm) (Finset.ne_of_mem_erase hm)]
      rw [hP, ← this]
      ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 178–185 at 1e6a4209cd14 ↗

      1. pf2_test.h2.this have (x k - x m) * ∏ x_1 ∈ (s.erase k).erase m, (x k - x x_1) = ∏ x_1 ∈ s.erase k, (x k - x x_1)

        Leaves ∏ l ∈ (s.erase k).erase m, (x k - x l) = P * ((1 : ℚ) / (x k - x m)), with this : (x k - x m) * ∏ x_1 ∈ (s.erase k).erase m, (x k - x x_1) = ∏ x_1 ∈ s.erase k, (x k - x x_1).

        Uses library Finset.mul_prod_erase Taking a product over s : Finset ι is the same as multiplying the value on a single element f a by the product of s.erase a. .

        Lean, line 182
              have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hm

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 182 at 1e6a4209cd14 ↗

    7. pf2_test.h3 have ∑ i ∈ Finset.range n, ∏ i' ∈ (Finset.range n).erase i, (x k - y i') = w k * P * ∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i)

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with h3 : ∑ i ∈ Finset.range n, ∏ i' ∈ (Finset.range n).erase i, (x k - y i') = w k * P * ∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 187–194
          have h3 : (∑ i ∈ Finset.range n, ∏ i' ∈ (Finset.range n).erase i, (x k - y i')) =
        (w k * P) * ∑ i ∈ Finset.range n, 1 / (x k - y i) := by
      rw [hw k hk, Finset.mul_sum]
      refine Finset.sum_congr rfl (fun i hi => ?_)
      have := Finset.mul_prod_erase (Finset.range n) (fun i' => x k - y i') hi
      field_simp [hxy i hi]
      rw [← this]
      ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 187–194 at 1e6a4209cd14 ↗

      1. pf2_test.h3.this have (x k - y i) * ∏ x_1 ∈ (Finset.range n).erase i, (x k - y x_1) = ∏ x_1 ∈ Finset.range n, (x k - y x_1)

        Leaves ∏ i' ∈ (Finset.range n).erase i, (x k - y i') = (∏ i ∈ Finset.range n, (x k - y i)) * ((1 : ℚ) / (x k - y i)), with this : (x k - y i) * ∏ x_1 ∈ (Finset.range n).erase i, (x k - y x_1) = ∏ x_1 ∈ Finset.range n, (x k - y x_1).

        Uses library Finset.mul_prod_erase Taking a product over s : Finset ι is the same as multiplying the value on a single element f a by the product of s.erase a. , Finset.range range n is the set of natural numbers less than n. .

        Lean, line 191
              have := Finset.mul_prod_erase (Finset.range n) (fun i' => x k - y i') hi

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 191 at 1e6a4209cd14 ↗

    8. pf2_test.h1' have ∑ j ∈ s.erase k, w j * ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ∑ j ∈ s.erase k, w j / (x k - x j)

      Leaves ∑ j ∈ s.erase k, w j / (x k - x j) = w k * (∑ i ∈ Finset.range n, (1 : ℚ) / (x k - y i) - ∑ l ∈ s.erase k, (1 : ℚ) / (x k - x l)), with h1' : ∑ j ∈ s.erase k, w j * ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) = P * ∑ j ∈ s.erase k, w j / (x k - x j).

      Uses library Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 196–201
          have h1' : ∑ j ∈ s.erase k, w j * ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) =
        P * ∑ j ∈ s.erase k, w j / (x k - x j) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun j hj => ?_)
      rw [h1 j hj]
      ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 196–201 at 1e6a4209cd14 ↗

  4. hc have ∀ (j : ℕ), Qc n j = ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hc : ∀ (j : ℕ), Qc n j = ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - (1 : ℕ)) / (2 : ℕ)) * ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ))) * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ ((2 : ℕ) * n - j - i) - (1 : ℚ)) / ((2 : ℚ) ^ (i + (1 : ℕ)) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 206–209
      have hc : ∀ j, Qc n j = ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
        ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro j; rw [hQc]

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 206–209 at 1e6a4209cd14 ↗

  5. hk1 have k ∈ Finset.range (n + (1 : ℕ))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hk1 : k ∈ Finset.range (n + (1 : ℕ)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range.

    Lean, line 210
      have hk1 : k ∈ Finset.range (n + 1) := Finset.mem_range.mpr (by omega)

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 210 at 1e6a4209cd14 ↗

  6. h2 have ∀ (m : ℕ), (2 : ℚ) ^ m ≠ (0 : ℚ)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with h2 : ∀ (m : ℕ), (2 : ℚ) ^ m ≠ (0 : ℚ).

    Lean, line 211
      have h2 : ∀ m : ℕ, (2 : ℚ) ^ m ≠ 0 := fun m => by positivity

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 211 at 1e6a4209cd14 ↗

  7. hs1 have ∀ (b : ℕ), (2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hs1 : ∀ (b : ℕ), (2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ).

    Lean, lines 212–217
      have hs1 : ∀ b : ℕ, (2 : ℚ) ^ (b + 1) - 1 ≠ 0 := by
    intro b
    have : (2 : ℚ) ≤ 2 ^ (b + 1) := by
      calc (2 : ℚ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ (b + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
    linarith

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 212–217 at 1e6a4209cd14 ↗

    1. hs1.this have (2 : ℚ) ≤ (2 : ℚ) ^ (b + (1 : ℕ))

      Leaves (2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ) ≠ (0 : ℚ), with this : (2 : ℚ) ≤ (2 : ℚ) ^ (b + (1 : ℕ)).

      Lean, lines 214–216
          have : (2 : ℚ) ≤ 2 ^ (b + 1) := by
      calc (2 : ℚ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ (b + 1) := pow_le_pow_right₀ (by norm_num) (by omega)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 214–216 at 1e6a4209cd14 ↗

      1. hs1.this.s1 calc (2 : ℚ) = (2 : ℚ) ^ (1 : ℕ) routine: norm_num

        Closes the goal.

        Lean, line 215
              calc (2 : ℚ) = 2 ^ 1 := by norm_num

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 215 at 1e6a4209cd14 ↗

      2. hs1.this.s2 calc (2 : ℚ) ^ (1 : ℕ) ≤ (2 : ℚ) ^ (b + (1 : ℕ))

        Closes the goal.

        Uses library pow_le_pow_right₀.

        Lean, line 216
                _ ≤ 2 ^ (b + 1) := pow_le_pow_right₀ (by norm_num) (by omega)

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 216 at 1e6a4209cd14 ↗

  8. hs1' have ∀ (b : ℕ), (1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)) ≠ (0 : ℚ)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hs1' : ∀ (b : ℕ), (1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)) ≠ (0 : ℚ).

    Lean, line 218
      have hs1' : ∀ b : ℕ, (1 : ℚ) - 2 ^ (b + 1) ≠ 0 := fun b h => hs1 b (by linarith)

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 218 at 1e6a4209cd14 ↗

  9. hinj have ∀ (a b : ℕ), (2 : ℚ) ^ a = (2 : ℚ) ^ b → a = b

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hinj : ∀ (a b : ℕ), (2 : ℚ) ^ a = (2 : ℚ) ^ b → a = b.

    Uses library Nat.pow_right_injective, le_refl The relation ≤ on a preorder is reflexive. .

    Lean, lines 219–222
      have hinj : ∀ a b : ℕ, (2 : ℚ) ^ a = 2 ^ b → a = b := by
    intro a b h
    have : (2 : ℕ) ^ a = 2 ^ b := by exact_mod_cast h
    exact Nat.pow_right_injective (le_refl 2) this

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 219–222 at 1e6a4209cd14 ↗

    1. hinj.this have (2 : ℕ) ^ a = (2 : ℕ) ^ b

      Leaves a = b, with this : (2 : ℕ) ^ a = (2 : ℕ) ^ b.

      Lean, line 221
          have : (2 : ℕ) ^ a = 2 ^ b := by exact_mod_cast h

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 221 at 1e6a4209cd14 ↗

  10. hx have ∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), (fun (l : ℕ) => (2 : ℚ) ^ l) a = (fun (l : ℕ) => (2 : ℚ) ^ l) b → a = b

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hx : ∀ a ∈ Finset.range (n + (1 : ℕ)), ∀ b ∈ Finset.range (n + (1 : ℕ)), (fun (l : ℕ) => (2 : ℚ) ^ l) a = (fun (l : ℕ) => (2 : ℚ) ^ l) b → a = b.

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 223–225
      have hx : ∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1),
      (fun l : ℕ => (2 : ℚ) ^ l) a = (fun l : ℕ => (2 : ℚ) ^ l) b → a = b :=
    fun a _ b _ h => hinj a b h

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 223–225 at 1e6a4209cd14 ↗

  11. hxy have ∀ i ∈ Finset.range n, (fun (l : ℕ) => (2 : ℚ) ^ l) k - (fun (i : ℕ) => (2 : ℚ) ^ (n + (1 : ℕ) + i)) i ≠ (0 : ℚ)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hxy : ∀ i ∈ Finset.range n, (fun (l : ℕ) => (2 : ℚ) ^ l) k - (fun (i : ℕ) => (2 : ℚ) ^ (n + (1 : ℕ) + i)) i ≠ (0 : ℚ).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 226–230
      have hxy : ∀ i ∈ Finset.range n,
      (fun l : ℕ => (2 : ℚ) ^ l) k - (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i)) i ≠ 0 := by
    intro i _ h
    have := hinj _ _ (sub_eq_zero.mp h)
    omega

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 226–230 at 1e6a4209cd14 ↗

    1. hxy.this have k = n + (1 : ℕ) + i

      Leaves False, with this : k = n + (1 : ℕ) + i.

      Uses library sub_eq_zero.

      Lean, line 229
          have := hinj _ _ (sub_eq_zero.mp h)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 229 at 1e6a4209cd14 ↗

  12. hw have ∀ j ∈ Finset.range (n + (1 : ℕ)), (fun (j : ℕ) => Qc n j * (2 : ℚ) ^ j) j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (l : ℕ) => (2 : ℚ) ^ l) l) = ∏ i ∈ Finset.range n, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (i : ℕ) => (2 : ℚ) ^ (n + (1 : ℕ) + i)) i)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hw : ∀ j ∈ Finset.range (n + (1 : ℕ)), (fun (j : ℕ) => Qc n j * (2 : ℚ) ^ j) j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (l : ℕ) => (2 : ℚ) ^ l) l) = ∏ i ∈ Finset.range n, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (i : ℕ) => (2 : ℚ) ^ (n + (1 : ℕ) + i)) i).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 231–257
      have hw : ∀ j ∈ Finset.range (n + 1),
      (fun j => Qc n j * (2 : ℚ) ^ j) j *
        ∏ l ∈ (Finset.range (n + 1)).erase j, ((fun l : ℕ => (2 : ℚ) ^ l) j - (fun l : ℕ => (2 : ℚ) ^ l) l) =
      ∏ i ∈ Finset.range n, ((fun l : ℕ => (2 : ℚ) ^ l) j - (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i)) i) := by
    intro j hj
    have hjn : j ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hj)
    simp only []
    let g : ℕ → ℚ := fun l => if l = j then 1 else (2 : ℚ) ^ j - 2 ^ l
    have e1 : ∏ l ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ l) =
        ∏ l ∈ (Finset.range (n + 1)).erase j, g l :=
      Finset.prod_congr rfl (fun l hl => by simp only [g, if_neg (Finset.ne_of_mem_erase hl)])
    have e2 : ∏ l ∈ (Finset.range (n + 1)).erase j, g l = ∏ l ∈ Finset.range (n + 1), g l :=
      Finset.prod_erase _ (if_pos rfl)
    have e3 : ∏ l ∈ Finset.range (n + 1), g l =
        (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) := by
      rw [show n + 1 = (j + 1) + (n - j) by omega, Finset.prod_range_add, Finset.prod_range_succ]
      have ga : ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) :=
        Finset.prod_congr rfl (fun l hl => by
          have := Finset.mem_range.mp hl
          simp only [g, if_neg (show l ≠ j by omega)])
      have gb : ∏ s ∈ Finset.range (n - j), g (j + 1 + s) =
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) :=
        Finset.prod_congr rfl (fun s _ => by simp only [g, if_neg (show j + 1 + s ≠ j by omega)])
      rw [ga, gb, show g j = 1 from if_pos rfl, mul_one]
    rw [e1, e2, e3, ← lag_test n j hjn, hc j]
    ring

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 231–257 at 1e6a4209cd14 ↗

    1. hw.hjn have j ≤ n

      Leaves (fun (j : ℕ) => Qc n j * (2 : ℚ) ^ j) j * ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (l : ℕ) => (2 : ℚ) ^ l) l) = ∏ i ∈ Finset.range n, ((fun (l : ℕ) => (2 : ℚ) ^ l) j - (fun (i : ℕ) => (2 : ℚ) ^ (n + (1 : ℕ) + i)) i), with hjn : j ≤ n.

      Uses library Nat.lt_succ_iff, Finset.mem_range.

      Lean, line 236
          have hjn : j ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hj)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 236 at 1e6a4209cd14 ↗

    2. hw.e1 have ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l) = ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, g l

      Leaves Qc n j * (2 : ℚ) ^ j * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x) = ∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x)), with e1 : ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l) = ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, g l.

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg, Finset.ne_of_mem_erase.

      Lean, lines 239–241
          have e1 : ∏ l ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ l) =
        ∏ l ∈ (Finset.range (n + 1)).erase j, g l :=
      Finset.prod_congr rfl (fun l hl => by simp only [g, if_neg (Finset.ne_of_mem_erase hl)])

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 239–241 at 1e6a4209cd14 ↗

    3. hw.e2 have ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, g l = ∏ l ∈ Finset.range (n + (1 : ℕ)), g l

      Leaves Qc n j * (2 : ℚ) ^ j * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x) = ∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x)), with e2 : ∏ l ∈ (Finset.range (n + (1 : ℕ))).erase j, g l = ∏ l ∈ Finset.range (n + (1 : ℕ)), g l.

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_erase If a function applied at a point is 1, a product is unchanged by removing that point, if present, from a Finset. , if_pos, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 242–243
          have e2 : ∏ l ∈ (Finset.range (n + 1)).erase j, g l = ∏ l ∈ Finset.range (n + 1), g l :=
      Finset.prod_erase _ (if_pos rfl)

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 242–243 at 1e6a4209cd14 ↗

    4. hw.e3 have ∏ l ∈ Finset.range (n + (1 : ℕ)), g l = (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s))

      Leaves Qc n j * (2 : ℚ) ^ j * ∏ x ∈ (Finset.range (n + (1 : ℕ))).erase j, ((2 : ℚ) ^ j - (2 : ℚ) ^ x) = ∏ x ∈ Finset.range n, ((2 : ℚ) ^ j - (2 : ℚ) ^ (n + (1 : ℕ) + x)), with e3 : ∏ l ∈ Finset.range (n + (1 : ℕ)), g l = (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_range_add, Finset.prod_range_succ, if_pos, rfl rfl : a = a is the unique constructor of the equality type. , mul_one.

      Lean, lines 244–255
          have e3 : ∏ l ∈ Finset.range (n + 1), g l =
        (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) := by
      rw [show n + 1 = (j + 1) + (n - j) by omega, Finset.prod_range_add, Finset.prod_range_succ]
      have ga : ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) :=
        Finset.prod_congr rfl (fun l hl => by
          have := Finset.mem_range.mp hl
          simp only [g, if_neg (show l ≠ j by omega)])
      have gb : ∏ s ∈ Finset.range (n - j), g (j + 1 + s) =
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) :=
        Finset.prod_congr rfl (fun s _ => by simp only [g, if_neg (show j + 1 + s ≠ j by omega)])
      rw [ga, gb, show g j = 1 from if_pos rfl, mul_one]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 244–255 at 1e6a4209cd14 ↗

      1. hw.e3.ga have ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)

        Leaves (∏ x ∈ Finset.range j, g x) * g j * ∏ x ∈ Finset.range (n - j), g (j + (1 : ℕ) + x) = (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)), with ga : ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l).

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg.

        Lean, lines 248–251
              have ga : ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) :=
        Finset.prod_congr rfl (fun l hl => by
          have := Finset.mem_range.mp hl
          simp only [g, if_neg (show l ≠ j by omega)])

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 248–251 at 1e6a4209cd14 ↗

        1. hw.e3.ga.this have l < j

          Leaves g l = (2 : ℚ) ^ j - (2 : ℚ) ^ l, with this : l < j.

          Uses library Finset.mem_range.

          Lean, line 250
                    have := Finset.mem_range.mp hl

          targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 250 at 1e6a4209cd14 ↗

      2. hw.e3.gb have ∏ s ∈ Finset.range (n - j), g (j + (1 : ℕ) + s) = ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s))

        Leaves (∏ x ∈ Finset.range j, g x) * g j * ∏ x ∈ Finset.range (n - j), g (j + (1 : ℕ) + x) = (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - (2 : ℚ) ^ l)) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)), with gb : ∏ s ∈ Finset.range (n - j), g (j + (1 : ℕ) + s) = ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - (2 : ℚ) ^ (j + (1 : ℕ) + s)).

        Uses library Finset.range range n is the set of natural numbers less than n. , Finset.prod_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg.

        Lean, lines 252–254
              have gb : ∏ s ∈ Finset.range (n - j), g (j + 1 + s) =
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) :=
        Finset.prod_congr rfl (fun s _ => by simp only [g, if_neg (show j + 1 + s ≠ j by omega)])

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 252–254 at 1e6a4209cd14 ↗

  13. hpf have ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = Qc n k * (2 : ℚ) ^ k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (n + (1 : ℕ) + i)) - ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hpf : ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = Qc n k * (2 : ℚ) ^ k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (n + (1 : ℕ) + i)) - ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l)).

    Lean, lines 258–259
      have hpf := pf2_test n k hk1 (fun l : ℕ => (2 : ℚ) ^ l) (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i))
    (fun j => Qc n j * (2 : ℚ) ^ j) hx hxy hw

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 258–259 at 1e6a4209cd14 ↗

  14. hpk have ∀ j < k, (2 : ℚ) ^ (k - j) - (1 : ℚ) ≠ (0 : ℚ)

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with hpk : ∀ j < k, (2 : ℚ) ^ (k - j) - (1 : ℚ) ≠ (0 : ℚ).

    Lean, lines 261–264
      have hpk : ∀ j, j < k → (2 : ℚ) ^ (k - j) - 1 ≠ 0 := by
    intro j hj
    rw [show k - j = (k - j - 1) + 1 by omega]
    exact hs1 _

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 261–264 at 1e6a4209cd14 ↗

  15. T0 have ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T0 : ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_range_succ, Nat.sub_self, pow_zero, sub_self, div_zero, add_zero.

    Lean, lines 266–268
      have T0 : ∑ j ∈ Finset.range (k + 1), Qc n j / ((2 : ℚ) ^ (k - j) - 1) =
      ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) := by
    rw [Finset.sum_range_succ, Nat.sub_self, pow_zero, sub_self, div_zero, add_zero]

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 266–268 at 1e6a4209cd14 ↗

  16. T1 have ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T1 : ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_erase If a function applied at a point is 0, a sum is unchanged by removing that point, if present, from a Finset. , if_pos, rfl rfl : a = a is the unique constructor of the equality type. , Finset.sum_range_add, Finset.sum_range_succ, add_zero.

    Lean, lines 270–297
      have T1 : ∑ j ∈ (Finset.range (n + 1)).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j) =
      ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) -
        ∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
    let G : ℕ → ℚ := fun j => if j = k then 0 else Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j)
    have e1 : ∑ j ∈ (Finset.range (n + 1)).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j) =
        ∑ j ∈ (Finset.range (n + 1)).erase k, G j :=
      Finset.sum_congr rfl (fun j hj => by simp only [G, if_neg (Finset.ne_of_mem_erase hj)])
    rw [e1, Finset.sum_erase _ (show G k = 0 from if_pos rfl),
      show n + 1 = (k + 1) + (n - k) by omega, Finset.sum_range_add, Finset.sum_range_succ]
    have ga : ∑ j ∈ Finset.range k, G j = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) := by
      refine Finset.sum_congr rfl (fun j hj => ?_)
      have hjk := Finset.mem_range.mp hj
      simp only [G, show j ≠ k by omega, if_false]
      rw [show (2 : ℚ) ^ k = 2 ^ j * 2 ^ (k - j) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 j, hpk j hjk]
    have gb : ∑ b ∈ Finset.range (n - k), G (k + 1 + b) =
        -∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
      rw [← Finset.sum_neg_distrib]
      refine Finset.sum_congr rfl (fun b _ => ?_)
      simp only [G]
      rw [if_neg (by omega : k + 1 + b ≠ k), show k + 1 + b = k + b + 1 by omega]
      rw [show (2 : ℚ) ^ (k + b + 1) = 2 ^ k * 2 ^ (b + 1) by
        rw [show k + b + 1 = k + (b + 1) by omega, pow_add]]
      have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = -(2 ^ k * (2 ^ (b + 1) - 1)) := by ring
      rw [this]
      field_simp [h2 k, hs1 b]
    rw [ga, gb, show G k = 0 from if_pos rfl, add_zero]
    ring

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 270–297 at 1e6a4209cd14 ↗

    1. T1.e1 have ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, G j

      Leaves ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with e1 : ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - (2 : ℚ) ^ j) = ∑ j ∈ (Finset.range (n + (1 : ℕ))).erase k, G j.

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg, Finset.ne_of_mem_erase.

      Lean, lines 274–276
          have e1 : ∑ j ∈ (Finset.range (n + 1)).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j) =
        ∑ j ∈ (Finset.range (n + 1)).erase k, G j :=
      Finset.sum_congr rfl (fun j hj => by simp only [G, if_neg (Finset.ne_of_mem_erase hj)])

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 274–276 at 1e6a4209cd14 ↗

    2. T1.ga have ∑ j ∈ Finset.range k, G j = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ))

      Leaves ∑ x ∈ Finset.range k, G x + G k + ∑ x ∈ Finset.range (n - k), G (k + (1 : ℕ) + x) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with ga : ∑ j ∈ Finset.range k, G j = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_false, pow_add.

      Lean, lines 279–284
          have ga : ∑ j ∈ Finset.range k, G j = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) := by
      refine Finset.sum_congr rfl (fun j hj => ?_)
      have hjk := Finset.mem_range.mp hj
      simp only [G, show j ≠ k by omega, if_false]
      rw [show (2 : ℚ) ^ k = 2 ^ j * 2 ^ (k - j) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 j, hpk j hjk]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 279–284 at 1e6a4209cd14 ↗

      1. T1.ga.hjk have j < k

        Leaves G j = Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)), with hjk : j < k.

        Uses library Finset.mem_range.

        Lean, line 281
              have hjk := Finset.mem_range.mp hj

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 281 at 1e6a4209cd14 ↗

    3. T1.gb have ∑ b ∈ Finset.range (n - k), G (k + (1 : ℕ) + b) = -∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))

      Leaves ∑ x ∈ Finset.range k, G x + G k + ∑ x ∈ Finset.range (n - k), G (k + (1 : ℕ) + x) = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with gb : ∑ b ∈ Finset.range (n - k), G (k + (1 : ℕ) + b) = -∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_neg_distrib, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg, pow_add.

      Lean, lines 285–295
          have gb : ∑ b ∈ Finset.range (n - k), G (k + 1 + b) =
        -∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
      rw [← Finset.sum_neg_distrib]
      refine Finset.sum_congr rfl (fun b _ => ?_)
      simp only [G]
      rw [if_neg (by omega : k + 1 + b ≠ k), show k + 1 + b = k + b + 1 by omega]
      rw [show (2 : ℚ) ^ (k + b + 1) = 2 ^ k * 2 ^ (b + 1) by
        rw [show k + b + 1 = k + (b + 1) by omega, pow_add]]
      have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = -(2 ^ k * (2 ^ (b + 1) - 1)) := by ring
      rw [this]
      field_simp [h2 k, hs1 b]

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 285–295 at 1e6a4209cd14 ↗

      1. T1.gb.this have (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ)) = -((2 : ℚ) ^ k * ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))) routine: ring

        Leaves Qc n (k + b + (1 : ℕ)) * ((2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ))) / ((2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ))) = -(Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))), with this : (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ)) = -((2 : ℚ) ^ k * ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))).

        Lean, line 293
              have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = -(2 ^ k * (2 ^ (b + 1) - 1)) := by ring

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 293 at 1e6a4209cd14 ↗

  17. T2 have Qc n k * (2 : ℚ) ^ k * ∑ i ∈ Finset.range n, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = Qc n k * ∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T2 : Qc n k * (2 : ℚ) ^ k * ∑ i ∈ Finset.range n, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (n + (1 : ℕ) + i)) = Qc n k * ∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)).

    Uses library Finset.range range n is the set of natural numbers less than n. , mul_assoc, Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , pow_add.

    Lean, lines 299–307
      have T2 : Qc n k * (2 : ℚ) ^ k * ∑ i ∈ Finset.range n, 1 / ((2 : ℚ) ^ k - 2 ^ (n + 1 + i)) =
      Qc n k * ∑ i ∈ Finset.range n, 1 / (1 - (2 : ℚ) ^ (n + 1 + i - k)) := by
    rw [mul_assoc, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    have e : n + 1 + i - k = (n - k + i) + 1 := by omega
    rw [show (2 : ℚ) ^ (n + 1 + i) = 2 ^ k * 2 ^ (n + 1 + i - k) by rw [← pow_add]; congr 1; omega, e]
    have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (n - k + i + 1) = 2 ^ k * (1 - 2 ^ (n - k + i + 1)) := by ring
    rw [this]
    field_simp [h2 k, hs1' (n - k + i)] <;> ring

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 299–307 at 1e6a4209cd14 ↗

    1. T2.e have n + (1 : ℕ) + i - k = n - k + i + (1 : ℕ) routine: omega

      Leaves Qc n k * ((2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (n + (1 : ℕ) + i)))) = Qc n k * ((1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k))), with e : n + (1 : ℕ) + i - k = n - k + i + (1 : ℕ).

      Lean, line 303
          have e : n + 1 + i - k = (n - k + i) + 1 := by omega

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 303 at 1e6a4209cd14 ↗

    2. T2.this have (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (n - k + i + (1 : ℕ)) = (2 : ℚ) ^ k * ((1 : ℚ) - (2 : ℚ) ^ (n - k + i + (1 : ℕ))) routine: ring

      Leaves Qc n k * ((2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (n - k + i + (1 : ℕ))))) = Qc n k * ((1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n - k + i + (1 : ℕ)))), with this : (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (n - k + i + (1 : ℕ)) = (2 : ℚ) ^ k * ((1 : ℚ) - (2 : ℚ) ^ (n - k + i + (1 : ℕ))).

      Lean, line 305
          have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (n - k + i + 1) = 2 ^ k * (1 - 2 ^ (n - k + i + 1)) := by ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 305 at 1e6a4209cd14 ↗

  18. T3a have ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T3a : ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_erase If a function applied at a point is 0, a sum is unchanged by removing that point, if present, from a Finset. , if_pos, rfl rfl : a = a is the unique constructor of the equality type. , Finset.sum_range_add, Finset.sum_range_succ, add_zero.

    Lean, lines 309–325
      have T3a : ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) +
        ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) := by
    let H : ℕ → ℚ := fun l => if l = k then 0 else 1 / ((2 : ℚ) ^ k - 2 ^ l)
    have e1 : ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
        ∑ l ∈ (Finset.range (n + 1)).erase k, H l :=
      Finset.sum_congr rfl (fun l hl => by simp only [H, if_neg (Finset.ne_of_mem_erase hl)])
    rw [e1, Finset.sum_erase _ (show H k = 0 from if_pos rfl),
      show n + 1 = (k + 1) + (n - k) by omega, Finset.sum_range_add, Finset.sum_range_succ]
    have ha : ∑ l ∈ Finset.range k, H l = ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) :=
      Finset.sum_congr rfl (fun l hl => by
        have := Finset.mem_range.mp hl
        simp only [H, if_neg (show l ≠ k by omega)])
    have hb : ∑ b ∈ Finset.range (n - k), H (k + 1 + b) =
        ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) :=
      Finset.sum_congr rfl (fun b _ => by simp only [H, if_neg (show k + 1 + b ≠ k by omega)])
    rw [ha, hb, show H k = 0 from if_pos rfl, add_zero]

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 309–325 at 1e6a4209cd14 ↗

    1. T3a.e1 have ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, H l

      Leaves ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)), with e1 : ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, H l.

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg, Finset.ne_of_mem_erase.

      Lean, lines 313–315
          have e1 : ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
        ∑ l ∈ (Finset.range (n + 1)).erase k, H l :=
      Finset.sum_congr rfl (fun l hl => by simp only [H, if_neg (Finset.ne_of_mem_erase hl)])

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 313–315 at 1e6a4209cd14 ↗

    2. T3a.ha have ∑ l ∈ Finset.range k, H l = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l)

      Leaves ∑ x ∈ Finset.range k, H x + H k + ∑ x ∈ Finset.range (n - k), H (k + (1 : ℕ) + x) = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)), with ha : ∑ l ∈ Finset.range k, H l = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg.

      Lean, lines 318–321
          have ha : ∑ l ∈ Finset.range k, H l = ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) :=
      Finset.sum_congr rfl (fun l hl => by
        have := Finset.mem_range.mp hl
        simp only [H, if_neg (show l ≠ k by omega)])

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 318–321 at 1e6a4209cd14 ↗

      1. T3a.ha.this have l < k

        Leaves H l = (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l), with this : l < k.

        Uses library Finset.mem_range.

        Lean, line 320
                have := Finset.mem_range.mp hl

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 320 at 1e6a4209cd14 ↗

    3. T3a.hb have ∑ b ∈ Finset.range (n - k), H (k + (1 : ℕ) + b) = ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b))

      Leaves ∑ x ∈ Finset.range k, H x + H k + ∑ x ∈ Finset.range (n - k), H (k + (1 : ℕ) + x) = ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)), with hb : ∑ b ∈ Finset.range (n - k), H (k + (1 : ℕ) + b) = ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , if_neg.

      Lean, lines 322–324
          have hb : ∑ b ∈ Finset.range (n - k), H (k + 1 + b) =
        ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) :=
      Finset.sum_congr rfl (fun b _ => by simp only [H, if_neg (show k + 1 + b ≠ k by omega)])

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 322–324 at 1e6a4209cd14 ↗

  19. T3b have (2 : ℚ) ^ k * ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T3b : (2 : ℚ) ^ k * ∑ l ∈ Finset.range k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , Finset.sum_range_reflect.

    Lean, lines 326–338
      have T3b : (2 : ℚ) ^ k * ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
    rw [Finset.mul_sum]
    have e1 : ∀ l ∈ Finset.range k, (2 : ℚ) ^ k * (1 / ((2 : ℚ) ^ k - 2 ^ l)) =
        (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - 1) := by
      intro l hl
      have hlk := Finset.mem_range.mp hl
      rw [show (2 : ℚ) ^ k = 2 ^ l * 2 ^ (k - l) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 l, hpk l hlk] <;> ring
    rw [Finset.sum_congr rfl e1, ← Finset.sum_range_reflect]
    refine Finset.sum_congr rfl (fun b hb => ?_)
    have := Finset.mem_range.mp hb
    rw [show k - (k - 1 - b) = b + 1 by omega]

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 326–338 at 1e6a4209cd14 ↗

    1. T3b.e1 have ∀ l ∈ Finset.range k, (2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l)) = (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - (1 : ℚ))

      Leaves ∑ i ∈ Finset.range k, (2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ i)) = ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with e1 : ∀ l ∈ Finset.range k, (2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l)) = (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - (1 : ℚ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , pow_add.

      Lean, lines 329–334
          have e1 : ∀ l ∈ Finset.range k, (2 : ℚ) ^ k * (1 / ((2 : ℚ) ^ k - 2 ^ l)) =
        (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - 1) := by
      intro l hl
      have hlk := Finset.mem_range.mp hl
      rw [show (2 : ℚ) ^ k = 2 ^ l * 2 ^ (k - l) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 l, hpk l hlk] <;> ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 329–334 at 1e6a4209cd14 ↗

      1. T3b.e1.hlk have l < k

        Leaves (2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l)) = (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - (1 : ℚ)), with hlk : l < k.

        Uses library Finset.mem_range.

        Lean, line 332
              have hlk := Finset.mem_range.mp hl

        targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 332 at 1e6a4209cd14 ↗

    2. T3b.this have b < k

      Leaves (2 : ℚ) ^ (k - (k - (1 : ℕ) - b)) / ((2 : ℚ) ^ (k - (k - (1 : ℕ) - b)) - (1 : ℚ)) = (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with this : b < k.

      Uses library Finset.mem_range.

      Lean, line 337
          have := Finset.mem_range.mp hb

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 337 at 1e6a4209cd14 ↗

  20. T3c have (2 : ℚ) ^ k * ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)) = ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T3c : (2 : ℚ) ^ k * ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ (k + (1 : ℕ) + b)) = ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ))).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , pow_add.

    Lean, lines 339–347
      have T3c : (2 : ℚ) ^ k * ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) =
      ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1)) := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun b _ => ?_)
    rw [show (2 : ℚ) ^ (k + 1 + b) = 2 ^ k * 2 ^ (b + 1) by
      rw [show k + 1 + b = k + (b + 1) by omega, pow_add]]
    have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = 2 ^ k * (1 - 2 ^ (b + 1)) := by ring
    rw [this]
    field_simp [h2 k, hs1' b] <;> ring

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 339–347 at 1e6a4209cd14 ↗

    1. T3c.this have (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ)) = (2 : ℚ) ^ k * ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ))) routine: ring

      Leaves (2 : ℚ) ^ k * ((1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ)))) = (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ))), with this : (2 : ℚ) ^ k - (2 : ℚ) ^ k * (2 : ℚ) ^ (b + (1 : ℕ)) = (2 : ℚ) ^ k * ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ))).

      Lean, line 345
          have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = 2 ^ k * (1 - 2 ^ (b + 1)) := by ring

      targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, line 345 at 1e6a4209cd14 ↗

  21. T3 have Qc n k * (2 : ℚ) ^ k * ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = Qc n k * (∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ))))

    Leaves ∑ j ∈ Finset.range (k + (1 : ℕ)), Qc n j / ((2 : ℚ) ^ (k - j) - (1 : ℚ)) = Qc n k * (∑ i ∈ Finset.range n, (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (n + (1 : ℕ) + i - k)) - ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) - ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))) + ∑ b ∈ Finset.range (n - k), Qc n (k + b + (1 : ℕ)) * (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)), with T3 : Qc n k * (2 : ℚ) ^ k * ∑ l ∈ (Finset.range (n + (1 : ℕ))).erase k, (1 : ℚ) / ((2 : ℚ) ^ k - (2 : ℚ) ^ l) = Qc n k * (∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + (1 : ℕ)) / ((2 : ℚ) ^ (b + (1 : ℕ)) - (1 : ℚ)) + ∑ b ∈ Finset.range (n - k), (1 : ℚ) / ((1 : ℚ) - (2 : ℚ) ^ (b + (1 : ℕ)))).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 348–352
      have T3 : Qc n k * (2 : ℚ) ^ k * ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      Qc n k * (∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) +
        ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1))) := by
    rw [T3a]
    linear_combination (Qc n k) * T3b + (Qc n k) * T3c

    targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, lines 348–352 at 1e6a4209cd14 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000311.json, merge commit 1e6a4209cd14.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean, sha256 e513f32b0a48.
import Mathlib
import Nodes.«spec-ffd3137a».Context

/-- erdos-1050, hole `hpint` of the skeleton on erdos-1050--h1-v2--h3 (graph PR #253): a closed form
for the Padé numerator coefficient p_k = ∑_{j<k} Qc n j / (2^(k-j) - 1), k ≤ n (the j = k term is
0 in ℚ). It is the regular part at z = 2^k of the rational function ∑_j Qc n j / (z/2^j - 1), whose
product form is spec-f2b55478's, corrected for the terms j > k that p_k leaves out. Every term on the
right has 2-adic valuation at least k(k-1)/2, which is the 2-adic half of `hpint`. Checked exactly
(Python fractions) for 1 ≤ n ≤ 13 and every k ≤ n, and with 2 replaced by 3 and 5. -/
theorem erdos_1050_pade_numerator_closed_form : ∀ (Qc : ℕ → ℕ → ℚ),
    (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - 1) / 2) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - k - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) →
    ∀ n k : ℕ, k ≤ n →
      ∑ j ∈ Finset.range (k + 1), Qc n j / ((2 : ℚ) ^ (k - j) - 1) =
        Qc n k * (∑ i ∈ Finset.range n, 1 / (1 - (2 : ℚ) ^ (n + 1 + i - k)) -
            ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) -
            ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1))) +
          ∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
  have lag_test : ∀ (n j : ℕ), j ≤ n →
        (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
          ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * 2 ^ j *
        (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
        ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) := by
    intro n j hj
    have hpos : ∀ s : ℕ, (2 : ℚ) ^ (s + 1) - 1 ≠ 0 := by
      intro s
      have : (2 : ℚ) ≤ 2 ^ (s + 1) := by
        calc (2 : ℚ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
      linarith
    -- (b) the nodes below j
    have hb : ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) =
        (2 : ℚ) ^ (j * (j - 1) / 2) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) := by
      have h1 : ∀ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) = 2 ^ l * ((2 : ℚ) ^ (j - l) - 1) := by
        intro l hl
        have hl' := Finset.mem_range.mp hl
        have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega
        rw [this]; ring
      rw [Finset.prod_congr rfl h1, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
        Finset.sum_range_id]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun s hs => ?_)
      have hs' := Finset.mem_range.mp hs
      congr 2
      omega
    -- (c) the nodes above j
    have hc : ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
        (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) := by
      calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s))
          = ∏ s ∈ Finset.range (n - j), ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (s + 1) - 1)) := by
            refine Finset.prod_congr rfl (fun s _ => ?_)
            rw [show j + 1 + s = j + (s + 1) by omega, pow_add]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
    -- (d) the right side
    have hd : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) =
        (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i))
          = ∏ i ∈ Finset.range n, ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (n + 1 + i - j) - 1)) := by
            refine Finset.prod_congr rfl (fun i _ => ?_)
            rw [show n + 1 + i = j + (n + 1 + i - j) by omega, pow_add, Nat.add_sub_cancel_left]
            ring
        _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
    -- (e) the q-factorial splits at j
    have he : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1)) *
        ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) =
        ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) := by
      have hn : n = (n - j) + j := by omega
      conv_rhs => rw [hn]
      rw [Finset.prod_range_add, mul_comm]
      congr 1
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun t ht => ?_)
      have ht' := Finset.mem_range.mp ht
      congr 2
      omega
    -- (f) reflect the second Gaussian binomial's numerator
    have hf : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) =
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
      rw [← Finset.prod_range_reflect]
      refine Finset.prod_congr rfl (fun i hi => ?_)
      have hi' := Finset.mem_range.mp hi
      congr 2
      omega
    have hF : ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
    have hB : ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
    have hjj : j * j = j * (j - 1) / 2 + j * (j - 1) / 2 + j := by
      have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
      rcases j with _ | j
      · simp
      · simp only [Nat.add_sub_cancel] at h2 ⊢
        linarith
    have hpow : (-(2 : ℚ) ^ j) ^ n = (-1) ^ j * 2 ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j *
        (-(2 : ℚ) ^ j) ^ (n - j) := by
      rw [show n = j + (n - j) by omega, pow_add, Nat.add_sub_cancel_left, neg_pow, ← pow_mul, hjj,
        pow_add, pow_add]
      ring
    rw [Finset.prod_div_distrib, Finset.prod_div_distrib, hb, hc, hd, hf, hpow]
    field_simp
    rw [← he]
    ring
  open Polynomial in
  have pf_test : ∀ (n : ℕ) (x y w : ℕ → ℚ), (∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1), x a = x b → a = b) →
        (∀ j ∈ Finset.range (n + 1),
          w j * ∏ l ∈ (Finset.range (n + 1)).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) →
        (∑ j ∈ Finset.range (n + 1), Polynomial.C (w j) * ∏ l ∈ (Finset.range (n + 1)).erase j, (X - Polynomial.C (x l))) =
        ∏ i ∈ Finset.range n, (X - Polynomial.C (y i)) := by
    intro n x y w hx hw
    set s := Finset.range (n + 1) with hs
    have hL : (∑ j ∈ s, Polynomial.C (w j) * ∏ l ∈ s.erase j, (X - Polynomial.C (x l))).natDegree ≤ n := by
      refine natDegree_sum_le_of_forall_le _ _ (fun j hj => ?_)
      refine (natDegree_C_mul_le _ _).trans ((natDegree_prod_le _ _).trans ?_)
      simp only [natDegree_X_sub_C, Finset.sum_const, smul_eq_mul, mul_one]
      rw [Finset.card_erase_of_mem hj, hs, Finset.card_range]
      omega
    have hE : (∏ i ∈ Finset.range n, (X - Polynomial.C (y i))).natDegree ≤ n := by
      refine (natDegree_prod_le _ _).trans ?_
      simp [natDegree_X_sub_C]
    apply Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq (s.image x)
    · rw [Finset.card_image_of_injOn (fun a ha b hb h => hx a ha b hb h), hs, Finset.card_range]
      refine lt_of_le_of_lt (degree_sub_le _ _) (max_lt ?_ ?_)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hL) (by exact_mod_cast Nat.lt_succ_self n)
      · exact lt_of_le_of_lt (degree_le_of_natDegree_le hE) (by exact_mod_cast Nat.lt_succ_self n)
    · intro z hz
      obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hz
      simp only [eval_finset_sum, eval_mul, eval_C, eval_prod, eval_sub, eval_X]
      rw [Finset.sum_eq_single j]
      · exact hw j hj
      · intro i hi hij
        rw [Finset.prod_eq_zero (i := j) (Finset.mem_erase.mpr ⟨Ne.symm hij, hj⟩) (sub_self _), mul_zero]
      · intro hj'; exact absurd hj hj'
  open Polynomial in
  have pf2_test : ∀ (n k : ℕ), k ∈ Finset.range (n + 1) → ∀ (x y w : ℕ → ℚ),
        (∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1), x a = x b → a = b) →
        (∀ i ∈ Finset.range n, x k - y i ≠ 0) →
        (∀ j ∈ Finset.range (n + 1),
          w j * ∏ l ∈ (Finset.range (n + 1)).erase j, (x j - x l) = ∏ i ∈ Finset.range n, (x j - y i)) →
        ∑ j ∈ (Finset.range (n + 1)).erase k, w j / (x k - x j) =
        w k * (∑ i ∈ Finset.range n, 1 / (x k - y i) -
          ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / (x k - x l)) := by
    intro n k hk x y w hx hxy hw
    have hLE := pf_test n x y w hx hw
    set s := Finset.range (n + 1) with hs
    have hne : ∀ j ∈ s, j ≠ k → x k - x j ≠ 0 := by
      intro j hj hjk h
      exact hjk (hx j hj k hk (sub_eq_zero.mp h).symm)
    set P := ∏ l ∈ s.erase k, (x k - x l) with hP
    have hP0 : P ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun l hl =>
      hne l (Finset.mem_of_mem_erase hl) (Finset.ne_of_mem_erase hl))
    have hd := congrArg (fun p => (derivative p).eval (x k)) hLE
    simp only [derivative_sum, derivative_mul, derivative_C, zero_mul, zero_add, derivative_prod_finset,
      derivative_sub, derivative_X, sub_zero, mul_one, eval_finset_sum, eval_mul, eval_C, eval_prod,
      eval_sub, eval_X] at hd
    -- the terms j ≠ k
    have h1 : ∀ j ∈ s.erase k, (∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l)) =
        P * (1 / (x k - x j)) := by
      intro j hj
      have hjs := Finset.mem_of_mem_erase hj
      have hjk := Finset.ne_of_mem_erase hj
      have hks : k ∈ s.erase j := Finset.mem_erase.mpr ⟨Ne.symm hjk, hk⟩
      rw [Finset.sum_eq_single k]
      · have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hj
        rw [Finset.erase_right_comm]
        field_simp [hne j hjs hjk]
        rw [hP, ← this]
        ring
      · intro m hm hmk
        exact Finset.prod_eq_zero (i := k) (Finset.mem_erase.mpr ⟨Ne.symm hmk, hks⟩) (sub_self _)
      · intro h; exact absurd hks h
    -- the term j = k
    have h2 : (∑ m ∈ s.erase k, ∏ l ∈ (s.erase k).erase m, (x k - x l)) =
        P * ∑ m ∈ s.erase k, 1 / (x k - x m) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun m hm => ?_)
      have := Finset.mul_prod_erase (s.erase k) (fun l => x k - x l) hm
      field_simp [hne m (Finset.mem_of_mem_erase hm) (Finset.ne_of_mem_erase hm)]
      rw [hP, ← this]
      ring
    -- the right side
    have h3 : (∑ i ∈ Finset.range n, ∏ i' ∈ (Finset.range n).erase i, (x k - y i')) =
        (w k * P) * ∑ i ∈ Finset.range n, 1 / (x k - y i) := by
      rw [hw k hk, Finset.mul_sum]
      refine Finset.sum_congr rfl (fun i hi => ?_)
      have := Finset.mul_prod_erase (Finset.range n) (fun i' => x k - y i') hi
      field_simp [hxy i hi]
      rw [← this]
      ring
    rw [← Finset.add_sum_erase s _ hk, h2, h3] at hd
    have h1' : ∑ j ∈ s.erase k, w j * ∑ m ∈ s.erase j, ∏ l ∈ (s.erase j).erase m, (x k - x l) =
        P * ∑ j ∈ s.erase k, w j / (x k - x j) := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun j hj => ?_)
      rw [h1 j hj]
      ring
    rw [h1'] at hd
    apply mul_left_cancel₀ hP0
    linear_combination hd
  intro Qc hQc n k hk
  have hc : ∀ j, Qc n j = ((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
        ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1) := by
    intro j; rw [hQc]
  have hk1 : k ∈ Finset.range (n + 1) := Finset.mem_range.mpr (by omega)
  have h2 : ∀ m : ℕ, (2 : ℚ) ^ m ≠ 0 := fun m => by positivity
  have hs1 : ∀ b : ℕ, (2 : ℚ) ^ (b + 1) - 1 ≠ 0 := by
    intro b
    have : (2 : ℚ) ≤ 2 ^ (b + 1) := by
      calc (2 : ℚ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ (b + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
    linarith
  have hs1' : ∀ b : ℕ, (1 : ℚ) - 2 ^ (b + 1) ≠ 0 := fun b h => hs1 b (by linarith)
  have hinj : ∀ a b : ℕ, (2 : ℚ) ^ a = 2 ^ b → a = b := by
    intro a b h
    have : (2 : ℕ) ^ a = 2 ^ b := by exact_mod_cast h
    exact Nat.pow_right_injective (le_refl 2) this
  have hx : ∀ a ∈ Finset.range (n + 1), ∀ b ∈ Finset.range (n + 1),
      (fun l : ℕ => (2 : ℚ) ^ l) a = (fun l : ℕ => (2 : ℚ) ^ l) b → a = b :=
    fun a _ b _ h => hinj a b h
  have hxy : ∀ i ∈ Finset.range n,
      (fun l : ℕ => (2 : ℚ) ^ l) k - (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i)) i ≠ 0 := by
    intro i _ h
    have := hinj _ _ (sub_eq_zero.mp h)
    omega
  have hw : ∀ j ∈ Finset.range (n + 1),
      (fun j => Qc n j * (2 : ℚ) ^ j) j *
        ∏ l ∈ (Finset.range (n + 1)).erase j, ((fun l : ℕ => (2 : ℚ) ^ l) j - (fun l : ℕ => (2 : ℚ) ^ l) l) =
      ∏ i ∈ Finset.range n, ((fun l : ℕ => (2 : ℚ) ^ l) j - (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i)) i) := by
    intro j hj
    have hjn : j ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hj)
    simp only []
    let g : ℕ → ℚ := fun l => if l = j then 1 else (2 : ℚ) ^ j - 2 ^ l
    have e1 : ∏ l ∈ (Finset.range (n + 1)).erase j, ((2 : ℚ) ^ j - 2 ^ l) =
        ∏ l ∈ (Finset.range (n + 1)).erase j, g l :=
      Finset.prod_congr rfl (fun l hl => by simp only [g, if_neg (Finset.ne_of_mem_erase hl)])
    have e2 : ∏ l ∈ (Finset.range (n + 1)).erase j, g l = ∏ l ∈ Finset.range (n + 1), g l :=
      Finset.prod_erase _ (if_pos rfl)
    have e3 : ∏ l ∈ Finset.range (n + 1), g l =
        (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) := by
      rw [show n + 1 = (j + 1) + (n - j) by omega, Finset.prod_range_add, Finset.prod_range_succ]
      have ga : ∏ l ∈ Finset.range j, g l = ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) :=
        Finset.prod_congr rfl (fun l hl => by
          have := Finset.mem_range.mp hl
          simp only [g, if_neg (show l ≠ j by omega)])
      have gb : ∏ s ∈ Finset.range (n - j), g (j + 1 + s) =
          ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) :=
        Finset.prod_congr rfl (fun s _ => by simp only [g, if_neg (show j + 1 + s ≠ j by omega)])
      rw [ga, gb, show g j = 1 from if_pos rfl, mul_one]
    rw [e1, e2, e3, ← lag_test n j hjn, hc j]
    ring
  have hpf := pf2_test n k hk1 (fun l : ℕ => (2 : ℚ) ^ l) (fun i : ℕ => (2 : ℚ) ^ (n + 1 + i))
    (fun j => Qc n j * (2 : ℚ) ^ j) hx hxy hw
  beta_reduce at hpf
  have hpk : ∀ j, j < k → (2 : ℚ) ^ (k - j) - 1 ≠ 0 := by
    intro j hj
    rw [show k - j = (k - j - 1) + 1 by omega]
    exact hs1 _
  -- T0: the j = k term of the statement's sum is 0
  have T0 : ∑ j ∈ Finset.range (k + 1), Qc n j / ((2 : ℚ) ^ (k - j) - 1) =
      ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) := by
    rw [Finset.sum_range_succ, Nat.sub_self, pow_zero, sub_self, div_zero, add_zero]
  -- T1: the left side of hpf
  have T1 : ∑ j ∈ (Finset.range (n + 1)).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j) =
      ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) -
        ∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
    let G : ℕ → ℚ := fun j => if j = k then 0 else Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j)
    have e1 : ∑ j ∈ (Finset.range (n + 1)).erase k, Qc n j * (2 : ℚ) ^ j / ((2 : ℚ) ^ k - 2 ^ j) =
        ∑ j ∈ (Finset.range (n + 1)).erase k, G j :=
      Finset.sum_congr rfl (fun j hj => by simp only [G, if_neg (Finset.ne_of_mem_erase hj)])
    rw [e1, Finset.sum_erase _ (show G k = 0 from if_pos rfl),
      show n + 1 = (k + 1) + (n - k) by omega, Finset.sum_range_add, Finset.sum_range_succ]
    have ga : ∑ j ∈ Finset.range k, G j = ∑ j ∈ Finset.range k, Qc n j / ((2 : ℚ) ^ (k - j) - 1) := by
      refine Finset.sum_congr rfl (fun j hj => ?_)
      have hjk := Finset.mem_range.mp hj
      simp only [G, show j ≠ k by omega, if_false]
      rw [show (2 : ℚ) ^ k = 2 ^ j * 2 ^ (k - j) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 j, hpk j hjk]
    have gb : ∑ b ∈ Finset.range (n - k), G (k + 1 + b) =
        -∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
      rw [← Finset.sum_neg_distrib]
      refine Finset.sum_congr rfl (fun b _ => ?_)
      simp only [G]
      rw [if_neg (by omega : k + 1 + b ≠ k), show k + 1 + b = k + b + 1 by omega]
      rw [show (2 : ℚ) ^ (k + b + 1) = 2 ^ k * 2 ^ (b + 1) by
        rw [show k + b + 1 = k + (b + 1) by omega, pow_add]]
      have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = -(2 ^ k * (2 ^ (b + 1) - 1)) := by ring
      rw [this]
      field_simp [h2 k, hs1 b]
    rw [ga, gb, show G k = 0 from if_pos rfl, add_zero]
    ring
  -- T2: the nodes 2^(n+1+i)
  have T2 : Qc n k * (2 : ℚ) ^ k * ∑ i ∈ Finset.range n, 1 / ((2 : ℚ) ^ k - 2 ^ (n + 1 + i)) =
      Qc n k * ∑ i ∈ Finset.range n, 1 / (1 - (2 : ℚ) ^ (n + 1 + i - k)) := by
    rw [mul_assoc, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    have e : n + 1 + i - k = (n - k + i) + 1 := by omega
    rw [show (2 : ℚ) ^ (n + 1 + i) = 2 ^ k * 2 ^ (n + 1 + i - k) by rw [← pow_add]; congr 1; omega, e]
    have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (n - k + i + 1) = 2 ^ k * (1 - 2 ^ (n - k + i + 1)) := by ring
    rw [this]
    field_simp [h2 k, hs1' (n - k + i)] <;> ring
  -- T3: the other nodes 2^l, l ≠ k
  have T3a : ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) +
        ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) := by
    let H : ℕ → ℚ := fun l => if l = k then 0 else 1 / ((2 : ℚ) ^ k - 2 ^ l)
    have e1 : ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
        ∑ l ∈ (Finset.range (n + 1)).erase k, H l :=
      Finset.sum_congr rfl (fun l hl => by simp only [H, if_neg (Finset.ne_of_mem_erase hl)])
    rw [e1, Finset.sum_erase _ (show H k = 0 from if_pos rfl),
      show n + 1 = (k + 1) + (n - k) by omega, Finset.sum_range_add, Finset.sum_range_succ]
    have ha : ∑ l ∈ Finset.range k, H l = ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) :=
      Finset.sum_congr rfl (fun l hl => by
        have := Finset.mem_range.mp hl
        simp only [H, if_neg (show l ≠ k by omega)])
    have hb : ∑ b ∈ Finset.range (n - k), H (k + 1 + b) =
        ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) :=
      Finset.sum_congr rfl (fun b _ => by simp only [H, if_neg (show k + 1 + b ≠ k by omega)])
    rw [ha, hb, show H k = 0 from if_pos rfl, add_zero]
  have T3b : (2 : ℚ) ^ k * ∑ l ∈ Finset.range k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
    rw [Finset.mul_sum]
    have e1 : ∀ l ∈ Finset.range k, (2 : ℚ) ^ k * (1 / ((2 : ℚ) ^ k - 2 ^ l)) =
        (2 : ℚ) ^ (k - l) / ((2 : ℚ) ^ (k - l) - 1) := by
      intro l hl
      have hlk := Finset.mem_range.mp hl
      rw [show (2 : ℚ) ^ k = 2 ^ l * 2 ^ (k - l) by rw [← pow_add]; congr 1; omega]
      field_simp [h2 l, hpk l hlk] <;> ring
    rw [Finset.sum_congr rfl e1, ← Finset.sum_range_reflect]
    refine Finset.sum_congr rfl (fun b hb => ?_)
    have := Finset.mem_range.mp hb
    rw [show k - (k - 1 - b) = b + 1 by omega]
  have T3c : (2 : ℚ) ^ k * ∑ b ∈ Finset.range (n - k), 1 / ((2 : ℚ) ^ k - 2 ^ (k + 1 + b)) =
      ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1)) := by
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun b _ => ?_)
    rw [show (2 : ℚ) ^ (k + 1 + b) = 2 ^ k * 2 ^ (b + 1) by
      rw [show k + 1 + b = k + (b + 1) by omega, pow_add]]
    have : (2 : ℚ) ^ k - 2 ^ k * 2 ^ (b + 1) = 2 ^ k * (1 - 2 ^ (b + 1)) := by ring
    rw [this]
    field_simp [h2 k, hs1' b] <;> ring
  have T3 : Qc n k * (2 : ℚ) ^ k * ∑ l ∈ (Finset.range (n + 1)).erase k, 1 / ((2 : ℚ) ^ k - 2 ^ l) =
      Qc n k * (∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) +
        ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1))) := by
    rw [T3a]
    linear_combination (Qc n k) * T3b + (Qc n k) * T3c
  rw [T0]
  linear_combination hpf - T1 + T2 - T3

What is known

Notes

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (2 versions)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«spec-ffd3137a».Context

/-- erdos-1050, hole `hpint` of the skeleton on erdos-1050--h1-v2--h3 (graph PR #253): a closed form
for the Padé numerator coefficient p_k = ∑_{j<k} Qc n j / (2^(k-j) - 1), k ≤ n (the j = k term is
0 in ℚ). It is the regular part at z = 2^k of the rational function ∑_j Qc n j / (z/2^j - 1), whose
product form is spec-f2b55478's, corrected for the terms j > k that p_k leaves out. Every term on the
right has 2-adic valuation at least k(k-1)/2, which is the 2-adic half of `hpint`. Checked exactly
(Python fractions) for 1 ≤ n ≤ 13 and every k ≤ n, and with 2 replaced by 3 and 5. -/
theorem erdos_1050_pade_numerator_closed_form : ∀ (Qc : ℕ → ℕ → ℚ),
    (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - 1) / 2) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - k - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) →
    ∀ n k : ℕ, k ≤ n →
      ∑ j ∈ Finset.range (k + 1), Qc n j / ((2 : ℚ) ^ (k - j) - 1) =
        Qc n k * (∑ i ∈ Finset.range n, 1 / (1 - (2 : ℚ) ^ (n + 1 + i - k)) -
            ∑ b ∈ Finset.range k, (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) -
            ∑ b ∈ Finset.range (n - k), 1 / (1 - (2 : ℚ) ^ (b + 1))) +
          ∑ b ∈ Finset.range (n - k), Qc n (k + b + 1) * (2 : ℚ) ^ (b + 1) / ((2 : ℚ) ^ (b + 1) - 1) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall k\le n:\quad \sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\;=\;Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}}-\sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1}-\sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr)+\sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1}$

For any $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ fixed by hypothesis as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, and all natural numbers $k\le n$, the identity holds in $\mathbb{Q}$. Exponent subtractions are natural-number subtraction (none of $k-j$, $n+1+i-k$, $n-k$ truncates under $k\le n$) and $k(k-1)/2$ is natural-number division; on the left the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so the left side is in effect $p_k=\sum_{j<k}Q_c(n,j)/(2^{k-j}-1)$, and every denominator on the right is nonzero. The doc comment's 2-adic valuation claim is not part of the statement.

Rendered from gloss/5c92d6bfa27b….md · Improve these words →

History: 2 versions on record

  1. 2026-10-06 · written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4 · not signed · gloss/3d7d70d09521….md · the first version of its chain

    Read this version

    For any $Q_c : \mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ given by $$Q_c(n,k) = (-1)^k\, 2^{\lfloor k(k-1)/2\rfloor} \prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\;\cdot\;\prod_{i=0}^{n-1}\frac{2^{\,2n-k-i}-1}{2^{\,i+1}-1}$$ (the same definition as in the hole erdos-1050--h1-v2--h3), and for all natural numbers $k \le n$, $$\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1} \;=\; Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}} \;-\; \sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1} \;-\; \sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr) \;+\; \sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1},$$ in $\mathbb{Q}$.

    Reading notes. Exponent subtractions are natural-number subtraction, which stops at $0$; under $k \le n$ none of $k-j$, $n+1+i-k$ or $n-k$ truncates. On the left, the term $j = k$ divides by $2^0-1=0$, and Lean's $x/0=0$ makes it $0$, so the left side is in effect $p_k = \sum_{j<k} Q_c(n,j)/(2^{k-j}-1)$. On the right every denominator is nonzero. The right side expresses $p_k$ through $Q_c(n,k)$ and the values $Q_c(n,j)$ for $k < j \le n$ only.

    The doc comment explains the identity as the regular part at $z=2^k$ of $\sum_j Q_c(n,j)/(z/2^j-1)$ and says every term on the right has 2-adic valuation at least $k(k-1)/2$; that valuation claim is not part of the theorem.

    Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3; its doc comment ties it to the hole hpint of a skeleton on that node (graph PR #253) and to the product form of spec-f2b55478. The site shows it as not needed by any merged proof of this problem.

  2. 2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/5c92d6bfa27b….md · diff to its predecessor

    Read this version

    $\displaystyle \forall k\le n:\quad \sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\;=\;Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}}-\sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1}-\sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr)+\sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1}$

    For any $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ fixed by hypothesis as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, and all natural numbers $k\le n$, the identity holds in $\mathbb{Q}$. Exponent subtractions are natural-number subtraction (none of $k-j$, $n+1+i-k$, $n-k$ truncates under $k\le n$) and $k(k-1)/2$ is natural-number division; on the left the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so the left side is in effect $p_k=\sum_{j<k}Q_c(n,j)/(2^{k-j}-1)$, and every denominator on the right is nonzero. The doc comment's 2-adic valuation claim is not part of the statement.

Diff of 5c92d6bfa27b against 3d7d70d09521
@@ -1,11 +1,3 @@
-For any $Q_c : \mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ given by
-$$Q_c(n,k) = (-1)^k\, 2^{\lfloor k(k-1)/2\rfloor} \prod_{i=0}^{k-1}\frac{2^{\,n-i}-1}{2^{\,i+1}-1}\;\cdot\;\prod_{i=0}^{n-1}\frac{2^{\,2n-k-i}-1}{2^{\,i+1}-1}$$
-(the same definition as in the hole erdos-1050--h1-v2--h3), and for all natural numbers $k \le n$,
-$$\sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1} \;=\; Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}} \;-\; \sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1} \;-\; \sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr) \;+\; \sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1},$$
-in $\mathbb{Q}$.
+$$\forall k\le n:\quad \sum_{j=0}^{k}\frac{Q_c(n,j)}{2^{\,k-j}-1}\;=\;Q_c(n,k)\Bigl(\sum_{i=0}^{n-1}\frac{1}{1-2^{\,n+1+i-k}}-\sum_{b=0}^{k-1}\frac{2^{b+1}}{2^{b+1}-1}-\sum_{b=0}^{n-k-1}\frac{1}{1-2^{b+1}}\Bigr)+\sum_{b=0}^{n-k-1}\frac{Q_c(n,k+b+1)\,2^{b+1}}{2^{b+1}-1}$$
 
-Reading notes. Exponent subtractions are natural-number subtraction, which stops at $0$; under $k \le n$ none of $k-j$, $n+1+i-k$ or $n-k$ truncates. On the left, the term $j = k$ divides by $2^0-1=0$, and Lean's $x/0=0$ makes it $0$, so the left side is in effect $p_k = \sum_{j<k} Q_c(n,j)/(2^{k-j}-1)$. On the right every denominator is nonzero. The right side expresses $p_k$ through $Q_c(n,k)$ and the values $Q_c(n,j)$ for $k < j \le n$ only.
-
-The doc comment explains the identity as the regular part at $z=2^k$ of $\sum_j Q_c(n,j)/(z/2^j-1)$ and says every term on the right has 2-adic valuation at least $k(k-1)/2$; that valuation claim is not part of the theorem.
-
-Role on the record: the node is listed as proposed for the hole erdos-1050--h1-v2--h3; its doc comment ties it to the hole `hpint` of a skeleton on that node (graph PR #253) and to the product form of spec-f2b55478. The site shows it as not needed by any merged proof of this problem.
+For any $Q_c:\mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ fixed by hypothesis as $Q_c(n,k)=(-1)^k\,2^{k(k-1)/2}\prod_{i=0}^{k-1}\frac{2^{n-i}-1}{2^{i+1}-1}\prod_{i=0}^{n-1}\frac{2^{2n-k-i}-1}{2^{i+1}-1}$, and all natural numbers $k\le n$, the identity holds in $\mathbb{Q}$. Exponent subtractions are natural-number subtraction (none of $k-j$, $n+1+i-k$, $n-k$ truncates under $k\le n$) and $k(k-1)/2$ is natural-number division; on the left the term $j=k$ divides by $2^0-1=0$, which is $0$ in Lean, so the left side is in effect $p_k=\sum_{j<k}Q_c(n,j)/(2^{k-j}-1)$, and every denominator on the right is nonzero. The doc comment's 2-adic valuation claim is not part of the statement.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

Rendered from targets/erdos-1050/nodes/spec-ffd3137a/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000311.json, merge commit 1e6a4209cd14.

Verdict pass, from attestations/000311.json.

Submitter
t0929-1
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000311.json, merge commit 1e6a4209cd14.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1050/nodes/spec-ffd3137a/Witness.lean, sha256 3ad31bef9c9f.
import Mathlib

theorem witness : ∃ (Qc : ℕ → ℕ → ℚ) (n k : ℕ),
    (Qc = fun (n k : ℕ) =>
      ((-1 : ℚ) ^ k * (2 : ℚ) ^ (k * (k - 1) / 2) *
          ∏ i ∈ Finset.range k, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
        ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - k - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) ∧ k ≤ n :=
  ⟨_, 0, 0, rfl, le_refl 0⟩

In words, unverified — what this witness says; written by t1006-w4, drafted with Claude Opus 5.5 (Anthropic) via Claude Code, tester agent W4, 2026-10-06; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

This file shows that the statement's hypotheses can be met together: there exist a function $Q_c : \mathbb{N}\times\mathbb{N}\to\mathbb{Q}$ and natural numbers $n$, $k$ such that $Q_c$ is equal to the function defined in the statement (the signed product of two Gaussian-binomial-shaped products at $q = 2$, the same definition as in erdos-1050--h1-v2--h3) and $k \le n$. It takes $Q_c$ to be that function itself and $n = k = 0$. It says nothing about the closed form.

Rendered from gloss/b69eba8ee54c….md · Improve these words →

Annexes (1), in full

Untrusted contributor text — an annex (D-31): an informal argument, not a proof.

Untrusted: annex (D-31), by t0929-1, drafted with Claude Opus 5.5 via Claude Code (agents 1050-C, 1050-W3-1); Lean checked by POST /check and POST /precheck; identities in exact rational arithmetic (Python fractions), 2026-09-30T00:25:41Z, licence CC-BY-4.0. Rendered from targets/erdos-1050/nodes/spec-ffd3137a/annex/ecbc3af0554549368356065b98651fad88466968201351662542daeadabec749.md.

spec-ffd3137a (closed form for the Padé numerator coefficient p_k): an elementary proof route

Contributor: t0929-1 (agents 1050-C, 1050-W3-1). Status: all three steps are proved in Lean, as one theorem with the node's own statement: verdict pass from precheck 01M3QTYJZGY0J129XF270Y9PXC (2026-09-30, every step), submitted as graph pull request #311, not merged at the time of writing. The same argument, inlined into a proof of erdos-1050--h1-v2--h3, passed a precheck too. The identities are also checked in exact rational arithmetic (Python fractions). The Lean block at the end is step 1 alone, for reading; the full proof is the node's Proof.lean once merged.

Write q = 2, x_l = q^l, c_j = Qc n j, and E(X) = Π_{i<n} (X − q^(n+1+i)), a polynomial of degree n.

  1. The Padé denominator's coefficients are Lagrange coefficients (numerical: 315 cases, q ∈ {2,3,5}, n ≤ 13, every j ≤ n): c_j · q^j · Π_{l ≤ n, l ≠ j} (q^j − q^l) = E(q^j). Proof sketch: Π_{l<j}(q^j − q^l) = q^(j(j−1)/2) (q;q)_j, Π_{j<l≤n}(q^j − q^l) = (−1)^(n−j) q^(j(n−j)) (q;q)_(n−j), E(q^j) = (−1)^n q^(jn) Π_{t=n+1−j}^{2n−j} (q^t − 1), and c_j = (−1)^j q^(j(j−1)/2) [n j]_q [2n−j n]_q with [n j]_q (q;q)_j (q;q)_(n−j) = (q;q)_n and (q;q)_n [2n−j n]_q = Π_{t=n+1−j}^{2n−j} (q^t − 1). The powers of q add up to jn on both sides.
  2. Hence, by Lagrange interpolation (n + 1 nodes, deg E = n), Σ_{j ≤ n} c_j / (z/q^j − 1) = Σ_j c_j q^j / (z − q^j) = E(z) / Π_{l ≤ n} (z − q^l). At z = q^m, m > n, this is spec-f2b55478 (proved on the record), which this route re-derives without using it.
  3. The regular part at z = q^k (k ≤ n) of the left side is Σ_{j ≠ k} c_j q^j/(q^k − q^j); of the right side it is G'(q^k) with G(z) = E(z)/Π_{l ≠ k}(z − q^l), and G'(q^k) = G(q^k) · [Σ_i 1/(q^k − q^(n+1+i)) − Σ_{l ≠ k} 1/(q^k − q^l)] with G(q^k) = c_k q^k. Rewriting each fraction with powers of q and moving the terms j > k (which p_k leaves out) to the right gives exactly the statement of spec-ffd3137a.

A Lean route: prove 1 as a product identity (Finset.prod_range_succ, prod_range_reflect for the reindexing t = n+1−j..2n−j); get 2 from Mathlib's Lagrange interpolation or by clearing denominators and comparing two degree-n polynomials at the n+1 nodes; get 3 from Polynomial.derivative of a product at a node. Consequences for the hole hpint of erdos-1050--h1-v2--h3's skeleton are in annex 7c650db6… on that node.

import Mathlib

theorem lag_test (n j : ℕ) (hj : j ≤ n) :
    (((-1 : ℚ) ^ j * (2 : ℚ) ^ (j * (j - 1) / 2) *
        ∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) *
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) / ((2 : ℚ) ^ (i + 1) - 1)) * 2 ^ j *
      (∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l)) *
      ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
    ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) := by
  have hpos : ∀ s : ℕ, (2 : ℚ) ^ (s + 1) - 1 ≠ 0 := by
    intro s
    have : (2 : ℚ) ≤ 2 ^ (s + 1) := by
      calc (2 : ℚ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ (s + 1) := pow_le_pow_right₀ (by norm_num) (by omega)
    linarith
  -- (b) the nodes below j
  have hb : ∏ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) =
      (2 : ℚ) ^ (j * (j - 1) / 2) * ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) := by
    have h1 : ∀ l ∈ Finset.range j, ((2 : ℚ) ^ j - 2 ^ l) = 2 ^ l * ((2 : ℚ) ^ (j - l) - 1) := by
      intro l hl
      have hl' := Finset.mem_range.mp hl
      have : (2 : ℚ) ^ j = 2 ^ l * 2 ^ (j - l) := by rw [← pow_add]; congr 1; omega
      rw [this]; ring
    rw [Finset.prod_congr rfl h1, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum,
      Finset.sum_range_id]
    congr 1
    rw [← Finset.prod_range_reflect]
    refine Finset.prod_congr rfl (fun s hs => ?_)
    have hs' := Finset.mem_range.mp hs
    congr 2
    omega
  -- (c) the nodes above j
  have hc : ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s)) =
      (-(2 : ℚ) ^ j) ^ (n - j) * ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) := by
    calc ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ j - 2 ^ (j + 1 + s))
        = ∏ s ∈ Finset.range (n - j), ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (s + 1) - 1)) := by
          refine Finset.prod_congr rfl (fun s _ => ?_)
          rw [show j + 1 + s = j + (s + 1) by omega, pow_add]
          ring
      _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
  -- (d) the right side
  have hd : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i)) =
      (-(2 : ℚ) ^ j) ^ n * ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
    calc ∏ i ∈ Finset.range n, ((2 : ℚ) ^ j - 2 ^ (n + 1 + i))
        = ∏ i ∈ Finset.range n, ((-(2 : ℚ) ^ j) * ((2 : ℚ) ^ (n + 1 + i - j) - 1)) := by
          refine Finset.prod_congr rfl (fun i _ => ?_)
          rw [show n + 1 + i = j + (n + 1 + i - j) by omega, pow_add, Nat.add_sub_cancel_left]
          ring
      _ = _ := by rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
  -- (e) the q-factorial splits at j
  have he : (∏ i ∈ Finset.range j, ((2 : ℚ) ^ (n - i) - 1)) *
      ∏ s ∈ Finset.range (n - j), ((2 : ℚ) ^ (s + 1) - 1) =
      ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) := by
    have hn : n = (n - j) + j := by omega
    conv_rhs => rw [hn]
    rw [Finset.prod_range_add, mul_comm]
    congr 1
    rw [← Finset.prod_range_reflect]
    refine Finset.prod_congr rfl (fun t ht => ?_)
    have ht' := Finset.mem_range.mp ht
    congr 2
    omega
  -- (f) reflect the second Gaussian binomial's numerator
  have hf : ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (2 * n - j - i) - 1) =
      ∏ i ∈ Finset.range n, ((2 : ℚ) ^ (n + 1 + i - j) - 1) := by
    rw [← Finset.prod_range_reflect]
    refine Finset.prod_congr rfl (fun i hi => ?_)
    have hi' := Finset.mem_range.mp hi
    congr 2
    omega
  have hF : ∏ s ∈ Finset.range n, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
    Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
  have hB : ∏ s ∈ Finset.range j, ((2 : ℚ) ^ (s + 1) - 1) ≠ 0 :=
    Finset.prod_ne_zero_iff.mpr (fun s _ => hpos s)
  have hjj : j * j = j * (j - 1) / 2 + j * (j - 1) / 2 + j := by
    have h2 := Nat.two_mul_div_two_of_even (Nat.even_mul_pred_self j)
    rcases j with _ | j
    · simp
    · simp only [Nat.add_sub_cancel] at h2 ⊢
      nlinarith
  have hpow : (-(2 : ℚ) ^ j) ^ n = (-1) ^ j * 2 ^ (j * (j - 1) / 2) * 2 ^ (j * (j - 1) / 2) * 2 ^ j *
      (-(2 : ℚ) ^ j) ^ (n - j) := by
    rw [show n = j + (n - j) by omega, pow_add, Nat.add_sub_cancel_left, neg_pow, ← pow_mul, hjj,
      pow_add, pow_add]
    ring
  rw [Finset.prod_div_distrib, Finset.prod_div_distrib, hb, hc, hd, hf, hpow]
  field_simp
  rw [← he]
  ring
Acknowledged findings (15)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at (2 ^ (2 * n - k - i) - 1) / (2 ^ (i + 1) - 1)

The divisor 2^(i+1) - 1 is at least 1; the quotient is a factor of the Gaussian binomial in Qc, copied verbatim from erdos-1050--h1-v2--h3.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at (2 ^ (n - i) - 1) / (2 ^ (i + 1) - 1)

The divisor 2^(i+1) - 1 is at least 1; Qc is copied verbatim from erdos-1050--h1-v2--h3.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (1 - 2 ^ (b + 1))

2^(b+1) is at least 2, so the divisor is at most -1 and never zero.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (1 - 2 ^ (n + 1 + i - k))

Under k ≤ n the exponent is at least 1, so the divisor is at most -1 and never zero.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 2 ^ (b + 1) / (2 ^ (b + 1) - 1)

The divisor 2^(b+1) - 1 is at least 1.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at Qc n (k + b + 1) * 2 ^ (b + 1) / (2 ^ (b + 1) - 1)

The divisor 2^(b+1) - 1 is at least 1.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at Qc n j / (2 ^ (k - j) - 1)

Intended: the divisor is zero exactly at j = k, and that term is 0 in Lean, which is how the hole hpint and the definition of Aq in erdos-1050--h1-v2--h3 sum only over j < k.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at 2 * n - k

Every Qc n j used here has j ≤ n, so 2n - j does not truncate; Qc is copied verbatim from erdos-1050--h1-v2--h3.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at 2 * n - k - i

Here j ≤ n and i < n, so 2n - j - i ≥ 1 and does not truncate; Qc is copied verbatim from erdos-1050--h1-v2--h3.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at k - 1

At k = 0 it truncates to 0 and gives 0 * 0 / 2 = 0 = C(0,2), which is intended.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at k - j

j ranges over Finset.range (k + 1), so j ≤ k and k - j does not truncate.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at n + 1 + i - k

Under the hypothesis k ≤ n this is at least 1 + i and does not truncate.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at n - i

In Qc's first product i < j ≤ n for every Qc n j used here, so n - i ≥ 1 and does not truncate.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at n - k

Under the hypothesis k ≤ n this is the exact count of indices j = k+1, ..., n.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a off-by-one-range finding at Finset.range (k + 1)

Intended: j runs over 0..k inclusive as in hole hpint; the j = k term is 0.

How to read this page

How to read a statement’s page →