`Compfiles/Usa2017P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

56 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2017, Problem 2

Let $m_1, m_2, \ldots, m_n$ be a collection of $n$ positive integers, not necessarily distinct. For any sequence of integers $A = (a_1, \ldots, a_n)$ and any permutation $w = w_1 w_2 \cdots w_n$ of $m_1, \ldots, m_n$, define an $A$-inversion of $w$ to be a pair of entries $w_i, w_j$ with $i < j$ for which one of the following conditions holds:

$a_i \ge w_i > w_j$,
$w_j > a_i \ge w_i$, or
$w_i > w_j > a_i$.

Show that, for any two sequences of integers $A = (a_1, \ldots, a_n)$ and $B = (b_1, \ldots, b_n)$, and for any positive integer $k$, the number of permutations of $m_1, \ldots, m_n$ having exactly $k$ A-inversions is equal to the number of permutations of $m_1, \ldots, m_n$ having exactly $k$ B-inversions.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa2017P2.invPair The A-inversion relation on a pair of entries: x is the left entry (at position i, with threshold c = a_i) and y is the right entry line 55 source
Source documentation
The A-inversion relation on a pair of entries: x is the left entry (at position i, with threshold c = a_i) and y is the right entry.

no axioms what this means
Statement uses: Int
Proof uses: Or, And, LE.le, LT.lt
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def invPair (c x y : ℤ) : Prop := (x ≤ c ∧ y < x) ∨ (c < y ∧ x ≤ c) ∨ (y < x ∧ c < y)
```
instance Usa2017P2.(instance at line 57) line 57 source
def Usa2017P2.ainvCount The number of A-inversions of the permutation σ line 61 source
Source documentation
The number of A-inversions of the permutation σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Equiv.Perm
Proof uses: Finset.sum, Finset.univ, ite, And, LT.lt, Usa2017P2.invPair, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
def ainvCount {n : ℕ} (m : Fin n → ℤ) (A : Fin n → ℤ) (σ : Perm (Fin n)) : ℕ :=
…
```
def Usa2017P2.genFun The generating function ∑ σ, X ^ (ainvCount m A σ) of the A-inversion statistic line 65 source
Source documentation
The generating function ∑ σ, X ^ (ainvCount m A σ) of the A-inversion statistic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Polynomial
Proof uses: Finset.sum, Equiv.Perm, Finset.univ, HPow.hPow, Polynomial.X, Usa2017P2.ainvCount
11 instances, coercions and auxiliary constants left out.
```
noncomputable def genFun {n : ℕ} (m : Fin n → ℤ) (A : Fin n → ℤ) : ℤ[X] :=
…
```
def Usa2017P2.qq The geometric sum 1 + X + ⋯ + X^(t-1) line 69 source
Source documentation
The geometric sum 1 + X + ⋯ + X^(t-1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int
Proof uses: Finset.sum, Finset.range, HPow.hPow, Polynomial.X
8 instances, coercions and auxiliary constants left out.
```
noncomputable def qq (t : ℕ) : ℤ[X] := ∑ s ∈ range t, X ^ s
```
def Usa2017P2.valMul The multiset of values of the entries line 72 source
Source documentation
The multiset of values of the entries.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Multiset
Proof uses: Multiset.map, Finset.val, Finset.univ
1 instances, coercions and auxiliary constants left out.
```
def valMul {n : ℕ} (m : Fin n → ℤ) : Multiset ℤ := Finset.univ.val.map m
```
def Usa2017P2.eCnt The multiplicity of the value v among the entries line 75 source
Source documentation
The multiplicity of the value v among the entries.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int
Proof uses: Multiset.count, Usa2017P2.valMul
1 instances, coercions and auxiliary constants left out.
```
def eCnt {n : ℕ} (m : Fin n → ℤ) (v : ℤ) : ℕ := (valMul m).count v
```
Mentions: Usa2017P2.valMul
def Usa2017P2.cntP The number of entries satisfying p line 78 source
Source documentation
The number of entries satisfying p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, DecidablePred
Proof uses: Multiset.countP, Usa2017P2.valMul
```
def cntP {n : ℕ} (m : Fin n → ℤ) (p : ℤ → Prop) [DecidablePred p] : ℕ :=
…
```
def Usa2017P2.frontContrib The number of inversions contributed by the first position when it has entry x and threshold c, over the remaining entries w line 83 source
Source documentation
The number of inversions contributed by the first position when it has entry x and threshold c, over the remaining entries w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Fin
Proof uses: Finset.sum, Finset.univ, ite, Usa2017P2.invPair, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def frontContrib {t : ℕ} (c x : ℤ) (w : Fin t → ℤ) : ℕ :=
…
```
def Usa2017P2.skipEmb The embedding Fin n ↪ Fin (n+1) whose range is everything except p, as used in Equiv.Perm.decomposeFin line 88 source
Source documentation
The embedding Fin n ↪ Fin (n+1) whose range is everything except p, as used in Equiv.Perm.decomposeFin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Function.Embedding
Proof uses: Function.Embedding.mk, Equiv.Perm, Equiv.swap, Fin.succ
13 instances, coercions and auxiliary constants left out.
```
def skipEmb {n : ℕ} (p : Fin (n + 1)) : Fin n ↪ Fin (n + 1) where
…
```
lemma Usa2017P2.invPair_iff Compact characterization of invPair: the pair is an inversion iff the truth values "c lies in the half-open interval between the entries" and "x > y" differ line 94 source
Source documentation
Compact characterization of invPair: the pair is an inversion iff the truth values "c lies in the half-open interval between the entries" and "x > y" differ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Iff, Usa2017P2.invPair, Or, And, LT.lt, LE.le
Proof uses: id
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma invPair_iff (c x y : ℤ) :
    invPair c x y ↔ (y < x ∧ (x ≤ c ∨ c < y)) ∨ (x ≤ y ∧ x ≤ c ∧ c < y) := by
…
```
Mentions: Usa2017P2.invPair
lemma Usa2017P2.frontContrib_le line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Fin, LE.le, Eq, Usa2017P2.frontContrib, HAdd.hAdd, Finset.sum, Finset.univ, ite, LT.lt, OfNat.ofNat
Proof uses: id, Eq.mpr, Usa2017P2.invPair, congrArg, Eq.symm, Finset.sum_add_distrib, Finset.sum_congr, rfl, Finset, Membership.mem, Iff, Or, And, propext, Usa2017P2.invPair_iff, dite, False.elim, Not, ite_eq_left, Iff.mpr and 7 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.frontContrib_gt line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Fin, LT.lt, Eq, Usa2017P2.frontContrib, Finset.sum, Finset.univ, ite, And, OfNat.ofNat
Proof uses: id, Finset.sum_congr, Usa2017P2.invPair, rfl, Finset, Membership.mem, Iff, Eq.mpr, Or, LE.le, congrArg, propext, Usa2017P2.invPair_iff, if_congr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.skipEmb_ne line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Equiv.Perm, Equiv.swap, Fin.succ, Eq, Fin.succ_ne_zero, Equiv.injective, Eq.mp, congrArg, Equiv.swap_apply_left
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.sum_univ_add_skipEmb Splitting a sum over Fin (n+1) into the term at p and the rest line 128 source
Source documentation
Splitting a sum over Fin (n+1) into the term at p and the rest.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, AddCommMonoid, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Finset.sum, Finset.univ, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Finset, Finset.image, Finset.erase, Finset.ext, Iff.intro, Membership.mem, And, Exists, Iff.mp, Finset.mem_image, Iff.mpr, Ne, Finset.mem_erase, And.intro, Usa2017P2.skipEmb_ne, Finset.mem_univ, Equiv.Perm, Equiv.swap, Equiv.injective, Eq.trans and 15 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma sum_univ_add_skipEmb {n : ℕ} {M : Type*} [AddCommMonoid M] (p : Fin (n + 1))
    (g : Fin (n + 1) → M) : ∑ i, g i = g p + ∑ i : Fin n, g (skipEmb p i) := by
…
```
Mentions: Usa2017P2.skipEmb
lemma Usa2017P2.ainvCount_comp Relabeling the entries by a permutation does not change the number of A-inversions (thresholds are positional) line 151 source
Source documentation
Relabeling the entries by a permutation does not change the number of A-inversions (thresholds are positional).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Int, Eq, Usa2017P2.ainvCount, Function.comp, HMul.hMul
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
```
lemma ainvCount_comp {n : ℕ} (e : Perm (Fin n)) (m : Fin n → ℤ) (A : Fin n → ℤ)
    (σ : Perm (Fin n)) : ainvCount (m ∘ e) A σ = ainvCount m A (e * σ) := rfl
```
Mentions: Usa2017P2.ainvCount
lemma Usa2017P2.genFun_comp line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Int, Eq, Polynomial, Usa2017P2.genFun, Function.comp
Proof uses: id, Finset.sum, Finset.univ, HPow.hPow, Polynomial.X, Usa2017P2.ainvCount, Equiv.sum_comp, Equiv.mulLeft
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.ainvCount_decompose Documented declaration: ainvCount_decompose line 163 source
Source documentation
The first-position decomposition of the inversion count: under Equiv.Perm.decomposeFin, the A-inversions split into the pairs involving the first position (frontContrib) and the inversions of the remaining permutation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Equiv.Perm, Eq, Usa2017P2.ainvCount, Equiv, Prod, Nat.succ, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Usa2017P2.frontContrib, Function.comp, Function.Embedding, Usa2017P2.skipEmb, Fin.succ
Proof uses: Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ, id, Finset.sum, Finset.univ, ite, And, LT.lt, Usa2017P2.invPair, Eq.mpr, congrArg, Fin.sum_univ_succ, HAdd, Eq.rec, Eq.refl, ite_eq_right, lt_irrefl, And.left, zero_add, Eq.symm and 19 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma ainvCount_decompose {n : ℕ} (m : Fin (n + 1) → ℤ) (A : Fin (n + 1) → ℤ)
    (p : Fin (n + 1)) (π : Perm (Fin n)) :
    ainvCount m A (Equiv.Perm.decomposeFin.symm (p, π)) =
      frontContrib (A 0) (m p) (m ∘ skipEmb p) + ainvCount (m ∘ skipEmb p) (A ∘ Fin.succ) π := by
…
```
Mentions: Usa2017P2.ainvCount, Usa2017P2.frontContrib, Usa2017P2.skipEmb
lemma Usa2017P2.genFun_rec The first-position recurrence for the generating function line 207 source
Source documentation
The first-position recurrence for the generating function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Polynomial, Usa2017P2.genFun, Finset.sum, Finset.univ, HMul.hMul, HPow.hPow, Polynomial.X, Usa2017P2.frontContrib, Function.comp, Function.Embedding, Usa2017P2.skipEmb, Fin.succ
Proof uses: id, Eq.mpr, Equiv.Perm, Usa2017P2.ainvCount, Prod, Nat.succ, Equiv, Equiv.symm, Equiv.Perm.decomposeFin, congrArg, Eq.symm, Equiv.sum_comp, Prod.mk, Fintype.sum_prod_type, Finset.sum_congr, rfl, Finset, Membership.mem, Finset.mul_sum, Usa2017P2.ainvCount_decompose and 2 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma genFun_rec {n : ℕ} (m : Fin (n + 1) → ℤ) (A : Fin (n + 1) → ℤ) :
    genFun m A = ∑ p : Fin (n + 1),
      X ^ frontContrib (A 0) (m p) (m ∘ skipEmb p) * genFun (m ∘ skipEmb p) (A ∘ Fin.succ) := by
…
```
Mentions: Usa2017P2.genFun, Usa2017P2.frontContrib, Usa2017P2.skipEmb
lemma Usa2017P2.sum_if_eq_count line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Finset.sum, Finset.univ, ite, OfNat.ofNat, Multiset.count, Usa2017P2.valMul
Proof uses: Eq.mpr, Finset.card, Finset.filter, id, congrArg, Eq.symm, Finset.card_filter, Finset, Finset.filter_congr, Membership.mem, eq_comm, Multiset.countP, Multiset.map, Finset.val, Multiset.card, Multiset.filter, Multiset.countP_map, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.sum_if_eq_cntP line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, DecidablePred, Eq, Finset.sum, Finset.univ, ite, OfNat.ofNat, Usa2017P2.cntP
Proof uses: Eq.mpr, Finset.card, Finset.filter, id, congrArg, Eq.symm, Finset.card_filter, Multiset.countP, Multiset.map, Finset.val, Multiset.card, Multiset.filter, Multiset.countP_map, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.eCnt_eq_card_filter line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Usa2017P2.eCnt, Finset.card, Finset.filter, Finset.univ
Proof uses: Eq.mpr, Finset.sum, ite, OfNat.ofNat, id, congrArg, Finset.card_filter, Eq.symm, Multiset.count, Usa2017P2.valMul, Usa2017P2.sum_if_eq_count
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.valMul_comp_skipEmb Deleting one occurrence of a value from the entry multiset line 242 source
Source documentation
Deleting one occurrence of a value from the entry multiset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Multiset, Usa2017P2.valMul, Function.comp, Function.Embedding, Usa2017P2.skipEmb, Multiset.erase
Proof uses: Multiset.count, ite, Finset.sum, Finset.univ, Usa2017P2.sum_univ_add_skipEmb, rfl, Eq.mpr, id, congrArg, Eq.mp, Usa2017P2.sum_if_eq_count, add_comm, Eq.refl, Iff.mpr, Multiset.ext, dite, HSub.hSub, Multiset.count_erase_self, ite_eq_left, Not and 3 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma valMul_comp_skipEmb {n : ℕ} (m : Fin (n + 1) → ℤ) (p : Fin (n + 1)) :
    valMul (m ∘ skipEmb p) = (valMul m).erase (m p) := by
…
```
Mentions: Usa2017P2.valMul, Usa2017P2.skipEmb
lemma Usa2017P2.exists_perm_of_valMul_eq Two entry functions with the same multiset of values differ by a permutation of the indices line 266 source
Source documentation
Two entry functions with the same multiset of values differ by a permutation of the indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Multiset, Usa2017P2.valMul, Exists, Equiv.Perm, Function.comp
Proof uses: Nat.recAux, OfNat.ofNat, Exists.intro, funext, Fin.elim0, HAdd.hAdd, Membership.mem, Eq.mpr, id, congrArg, Iff.mpr, Multiset.map, Finset.val, Finset.univ, And, Multiset.mem_map, And.intro, Finset, Finset.mem_val, Finset.mem_univ and 23 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma exists_perm_of_valMul_eq {n : ℕ} :
    ∀ {m₁ m₂ : Fin n → ℤ}, valMul m₁ = valMul m₂ → ∃ e : Perm (Fin n), m₂ = m₁ ∘ e := by
…
```
Mentions: Usa2017P2.valMul
lemma Usa2017P2.genFun_eq_of_valMul_eq The generating function only depends on the multiset of values line 296 source
Source documentation
The generating function only depends on the multiset of values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Multiset, Usa2017P2.valMul, Polynomial, Usa2017P2.genFun
Proof uses: Equiv.Perm, Function.comp, Exists, Usa2017P2.exists_perm_of_valMul_eq, Eq.symm, Usa2017P2.genFun_comp
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma genFun_eq_of_valMul_eq {n : ℕ} {m₁ m₂ : Fin n → ℤ} (h : valMul m₁ = valMul m₂)
    (A : Fin n → ℤ) : genFun m₁ A = genFun m₂ A := by
…
```
Mentions: h, Usa2017P2.valMul, Usa2017P2.genFun
lemma Usa2017P2.frontContrib_eval Explicit evaluation of frontContrib in terms of the full entry multiset line 302 source
Source documentation
Explicit evaluation of frontContrib in terms of the full entry multiset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Usa2017P2.frontContrib, Function.comp, Function.Embedding, Usa2017P2.skipEmb, ite, LE.le, Usa2017P2.cntP, LT.lt, And
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Finset.sum, Finset.univ, Usa2017P2.frontContrib_le, HAdd, Eq.rec, Eq.refl, Usa2017P2.sum_univ_add_skipEmb, Usa2017P2.sum_if_eq_cntP, congrFun', Finset.sum_congr, Finset, Membership.mem, Eq.symm, Eq.mp, zero_add and 9 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma frontContrib_eval {n : ℕ} (m : Fin (n + 1) → ℤ) (c : ℤ) (p : Fin (n + 1)) :
    frontContrib c (m p) (m ∘ skipEmb p) =
      if m p ≤ c then cntP m (· < m p) + cntP m (c < ·)
      else cntP m (fun y => c < y ∧ y < m p) := by
…
```
Mentions: Usa2017P2.frontContrib, Usa2017P2.skipEmb, Usa2017P2.cntP
def Usa2017P2.gc The contribution of the first position, as a function of its value line 333 source
Source documentation
The contribution of the first position, as a function of its value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int
Proof uses: ite, LE.le, HAdd.hAdd, Usa2017P2.cntP, LT.lt, And
7 instances, coercions and auxiliary constants left out.
```
def gc {n : ℕ} (m : Fin n → ℤ) (c v : ℤ) : ℕ :=
…
```
lemma Usa2017P2.qq_add line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial, Int, Usa2017P2.qq, HAdd.hAdd, HMul.hMul, HPow.hPow, Polynomial.X
Proof uses: id, Eq.mpr, Finset.sum, Finset.range, congrArg, Finset.sum_range_add, Finset.mul_sum, HAdd, Eq.rec, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, pow_add
41 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.block_tele line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, Polynomial, Int, Finset.sum, Finset.range, List.length, HMul.hMul, HPow.hPow, Polynomial.X, List.sum, List.take, Usa2017P2.qq, GetElem?.getElem!, LT.lt
Proof uses: List.rec, of_eq_true, List.nil, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Finset, funext, congr, List.take_nil, pow_zero, getElem!_neg, Not, False, not_false_eq_true, MulZeroClass.mul_zero, Finset.sum_const_zero and 24 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.pureId line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, List.length, Eq, Polynomial, Int, HAdd.hAdd, HMul.hMul, HPow.hPow, Polynomial.X, HSub.hSub, List.sum, List.take, Finset.sum, Finset.range, Usa2017P2.qq, GetElem?.getElem!, LT.lt, Finset.Ico
Proof uses: Eq.mpr, Min.min, id, congrArg, List.length_take, Nat.min_eq_left, Eq.refl, HAppend.hAppend, List.drop, List.take_append_drop, List.sum_append, OfNat.ofNat, Nat.le_add_right, List.take_take, Option.getD, GetElem?.getElem?, Inhabited.default, List.getElem!_eq_getElem?_getD, Option, List.getElem?_take_of_lt and 72 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.multiset_card_filter_finset_sum The cardinality of a filter of a finite sum of multisets line 426 source
Source documentation
The cardinality of a filter of a finite sum of multisets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Multiset, Int, DecidablePred, Eq, Nat, Multiset.card, Multiset.filter, Finset.sum
Proof uses: Finset.induction, of_eq_true, OfNat.ofNat, eq_self, Not, Membership.mem, Eq.mpr, Insert.insert, HAdd.hAdd, id, congrArg, Finset.sum_insert, Multiset.filter_add, Multiset.card_add, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma multiset_card_filter_finset_sum {ι : Type*} [DecidableEq ι] (s : Finset ι)
    (f : ι → Multiset ℤ) (p : ℤ → Prop) [DecidablePred p] :
    Multiset.card (Multiset.filter p (∑ v ∈ s, f v)) =
      ∑ v ∈ s, Multiset.card (Multiset.filter p (f v)) := by
…
```
Mentions: f
lemma Usa2017P2.multiset_filter_replicate Filtering a replicated multiset line 437 source
Source documentation
Filtering a replicated multiset.

standard axioms: Quot.sound, propext what this means
Statement uses: Int, DecidablePred, Nat, Eq, Multiset, Multiset.filter, Multiset.replicate, ite, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, ite_self, eq_self, Eq.mpr, HAdd.hAdd, Multiset.cons, id, Multiset.replicate_succ, Singleton.singleton, Multiset.filter_cons, dite, congr, Decidable, ite_eq_left, Multiset.singleton_add, Eq.refl and 3 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma multiset_filter_replicate (p : ℤ → Prop) [DecidablePred p] (k : ℕ) (v : ℤ) :
    Multiset.filter p (Multiset.replicate k v) = if p v then Multiset.replicate k v else 0 := by
…
```
lemma Usa2017P2.list_map_sum_eq_sum_range Reindexing the sum of a mapped list as a sum over range line 450 source
Source documentation
Reindexing the sum of a mapped list as a sum over range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, AddCommMonoid, List, Eq, List.sum, List.map, Finset.sum, Nat, Finset.range, List.length, GetElem?.getElem!, LT.lt
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, EmptyCollection.emptyCollection, Finset, HSMul.hSMul, Finset.card, Inhabited.default, funext, getElem!_neg, Not, False, not_false_eq_true, Finset.sum_const and 17 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma list_map_sum_eq_sum_range {α : Type*} {β : Type*} [Inhabited α] [AddCommMonoid β]
    (l : List α) (f : α → β) :
    (l.map f).sum = ∑ t ∈ Finset.range l.length, f l[t]! := by
…
```
Mentions: f
lemma Usa2017P2.list_sum_eq_sum_range The sum of a list of naturals as a sum over range line 467 source
Source documentation
The sum of a list of naturals as a sum over range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Eq, List.sum, Finset.sum, Finset.range, List.length, GetElem?.getElem!, LT.lt
Proof uses: List.map, id, Usa2017P2.list_map_sum_eq_sum_range, Eq.mp, congrArg, List.map_id
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma list_sum_eq_sum_range (l : List ℕ) :
    l.sum = ∑ t ∈ Finset.range l.length, l[t]! := by
…
```
lemma Usa2017P2.list_sum_take_eq_sum_range The sum of an initial segment of a list of naturals line 474 source
Source documentation
The sum of an initial segment of a list of naturals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, List.length, Eq, List.sum, List.take, Finset.sum, Finset.range, GetElem?.getElem!, LT.lt
Proof uses: Eq.mpr, id, congrArg, Usa2017P2.list_sum_eq_sum_range, Min.min, List.length_take, Nat.min_eq_left, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.mp, propext, Finset.mem_range, GetElem.getElem, getElem!_pos, Nat.lt_of_lt_of_le, List.length_take_le', List.getElem_take, Eq.refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma list_sum_take_eq_sum_range (l : List ℕ) {j : ℕ} (hj : j ≤ l.length) :
    (l.take j).sum = ∑ t ∈ Finset.range j, l[t]! := by
…
```
lemma Usa2017P2.sorted_filter_eq_take In a sorted list of integers, the elements ≤ c form an initial segment line 487 source
Source documentation
In a sorted list of integers, the elements ≤ c form an initial segment.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Int, List.Pairwise, LE.le, Eq, List.filter, Decidable.decide, List.take, List.length
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, True, congrArg, List.take_nil, OfNat.ofNat, Nat, eq_self, List.cons, Membership.mem, And, Eq.mp, propext, List.pairwise_cons, dite, Eq.mpr, id, List.filter_cons_of_pos and 19 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma sorted_filter_eq_take (l : List ℤ) (c : ℤ) (hp : l.Pairwise (· ≤ ·)) :
    l.filter (· ≤ c) = l.take (l.filter (· ≤ c)).length := by
…
```
lemma Usa2017P2.sorted_get_lt_iff A sorted list of distinct integers is strictly increasing line 510 source
Source documentation
A sorted list of distinct integers is strictly increasing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Int, List.Pairwise, LE.le, List.Nodup, Fin, List.length, Iff, LT.lt, List.get
Proof uses: Iff.intro, Decidable.byContradiction, Not, Eq, Or, False, eq_or_lt_of_le, Eq.mp, congrArg, propext, not_lt, absurd, lt_irrefl, Iff.mpr, List.Pairwise.rel_get_of_lt, Ne, Iff.mp, List.Nodup.get_inj_iff, ne_of_lt, lt_of_le_of_ne
18 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma sorted_get_lt_iff {l : List ℤ} (hp : l.Pairwise (· ≤ ·)) (hn : l.Nodup)
    (s t : Fin l.length) : l.get s < l.get t ↔ s < t := by
…
```
lemma Usa2017P2.sorted_getElem!_lt_iff getElem! version of sorted_get_lt_iff line 526 source
Source documentation
getElem! version of sorted_get_lt_iff.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Int, List.Pairwise, LE.le, List.Nodup, Nat, LT.lt, List.length, Iff, GetElem?.getElem!
Proof uses: Eq, List.get, Fin.mk, Eq.mpr, Option.getD, GetElem?.getElem?, Inhabited.default, id, congrArg, List.getElem!_eq_getElem?_getD, Option.some, GetElem.getElem, Option, List.getElem?_eq_getElem, Option.getD_some, Fin.isLt, List.get_eq_getElem, Eq.refl, Fin, propext and 2 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma sorted_getElem!_lt_iff {l : List ℤ} (hp : l.Pairwise (· ≤ ·)) (hn : l.Nodup)
    {s t : ℕ} (hs : s < l.length) (ht : t < l.length) :
    l[s]! < l[t]! ↔ s < t := by
…
```
lemma Usa2017P2.sorted_getElem!_le_iff In a sorted list of distinct integers, the elements at positions < k are exactly those ≤ c, where k is the number of elements ≤ c line 537 source
Source documentation
In a sorted list of distinct integers, the elements at positions < k are exactly those ≤ c, where k is the number of elements ≤ c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Int, List.Pairwise, LE.le, List.Nodup, Nat, LT.lt, List.length, Iff, GetElem?.getElem!, List.filter, Decidable.decide
Proof uses: Eq, List.get, Fin.mk, Eq.mpr, Option.getD, GetElem?.getElem?, Inhabited.default, id, congrArg, List.getElem!_eq_getElem?_getD, Option.some, GetElem.getElem, Option, List.getElem?_eq_getElem, Option.getD_some, Fin.isLt, List.get_eq_getElem, Eq.refl, List.take, Usa2017P2.sorted_filter_eq_take and 26 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma sorted_getElem!_le_iff {l : List ℤ} (hp : l.Pairwise (· ≤ ·)) (hn : l.Nodup)
    (c : ℤ) {t : ℕ} (ht : t < l.length) :
    l[t]! ≤ c ↔ t < (l.filter (· ≤ c)).length := by
…
```
lemma Usa2017P2.sum_image_eq_sort_map_sum A sum over the image finset reindexed as a list sum over the sorted distinct values line 572 source
Source documentation
A sum over the image finset reindexed as a list sum over the sorted distinct values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, AddCommMonoid, Fin, Int, Eq, Finset.sum, Finset.image, Finset.univ, List.sum, List.map, Finset.sort, LE.le
Proof uses: Multiset, Finset.val, Finset.sort_eq, id, Eq.mpr, Multiset.sum, Multiset.map, congrArg, Eq.symm, Multiset.map_coe, Multiset.sum_coe, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma sum_image_eq_sort_map_sum {n : ℕ} {β : Type*} [AddCommMonoid β]
    (m : Fin n → ℤ) (G : ℤ → β) :
    ∑ v ∈ univ.image m, G v = (((univ.image m).sort (· ≤ ·)).map G).sum := by
…
```
lemma Usa2017P2.valMul_eq_sum_eCnt line 582 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Multiset, Usa2017P2.valMul, Finset.sum, Finset.image, Finset.univ, HSMul.hSMul, Usa2017P2.eCnt, Singleton.singleton
Proof uses: Iff, Membership.mem, Finset, of_eq_true, Eq.trans, Exists, True, congr, congrArg, List, List.ofFn, congrFun', Fin.univ_val_map, And, funext, true_and, iff_self, Iff.mpr, Multiset.count, Multiset.ext and 24 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.cntP_eq_sum_eCnt line 606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, DecidablePred, Eq, Usa2017P2.cntP, Finset.sum, Finset.image, Finset.univ, ite, Usa2017P2.eCnt, OfNat.ofNat
Proof uses: id, Eq.mpr, Multiset.countP, Usa2017P2.valMul, Multiset.card, Multiset.filter, congrArg, Multiset.countP_eq_card_filter, Multiset, HSMul.hSMul, Singleton.singleton, Usa2017P2.valMul_eq_sum_eCnt, Usa2017P2.multiset_card_filter_finset_sum, Finset.sum_congr, rfl, Finset, Membership.mem, Multiset.replicate, Multiset.nsmul_singleton, Usa2017P2.multiset_filter_replicate and 11 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.pureId_value The pure polynomial identity in value form: the key combinatorial input behind both the ratio identity and the main induction line 622 source
Source documentation
The pure polynomial identity in value form: the key combinatorial input behind both the ratio identity and the main induction. Proven by writing the value multiset as a sorted list of distinct values vs with multiplicity list es and split point k = #(values ≤ c), evaluating the counts via cntP_eq_sum_eCnt, and telescoping with pureId.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Polynomial, Finset.sum, Finset.image, Finset.univ, HMul.hMul, HPow.hPow, Polynomial.X, Usa2017P2.gc, Usa2017P2.qq, Usa2017P2.eCnt
Proof uses: List, Finset.sort, LE.le, rfl, List.map, List.length, List.filter, Decidable.decide, List.Pairwise, Finset.pairwise_sort, List.Nodup, Finset.sort_nodup, of_eq_true, Eq.trans, True, congrFun', congrArg, List.length_map, eq_self, List.length_filter_le and 86 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 161 steps
Open to load the checked before-and-after goal states.
```
lemma pureId_value {n : ℕ} (m : Fin (n + 1) → ℤ) (c : ℤ) :
    ∑ v ∈ univ.image m, X ^ gc m c v * qq (eCnt m v) = qq (n + 1) := by
…
```
Mentions: Usa2017P2.gc, Usa2017P2.qq, Usa2017P2.eCnt
lemma Usa2017P2.sum_eq_sum_image_card Grouping a sum over positions by the value of the entry line 781 source
Source documentation
Grouping a sum over positions by the value of the entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Polynomial, Eq, Finset.sum, Finset.univ, Finset.image, HMul.hMul, Usa2017P2.eCnt
Proof uses: Finset.filter, Eq.symm, Finset.sum_image', congrFun, Membership.mem, Finset, rfl, Eq.mpr, id, congrArg, Finset.sum_congr, And.right, Iff.mp, And, Finset.mem_filter, Eq.refl, HSMul.hSMul, Finset.card, Finset.sum_const, Usa2017P2.eCnt_eq_card_filter and 1 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sum_eq_sum_image_card {n : ℕ} (m : Fin (n + 1) → ℤ) (H : Fin (n + 1) → ℤ[X])
    (K : ℤ → ℤ[X]) (hHK : ∀ q, H q = K (m q)) :
    ∑ q, H q = ∑ v ∈ univ.image m, (eCnt m v : ℤ[X]) * K v := by
…
```
Mentions: Usa2017P2.eCnt
lemma Usa2017P2.genFun_zero line 791 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Int, Eq, Polynomial, Usa2017P2.genFun
Proof uses: id, Equiv.Perm, Usa2017P2.ainvCount, Finset.sum_eq_zero, Finset.univ, Finset.sum, ite, And, LT.lt, Usa2017P2.invPair, Membership.mem, Finset, Fin.elim0, Eq.mpr, HPow.hPow, Polynomial.X, congrArg, Finset.sum_congr, rfl, pow_zero and 13 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.genFun_one line 799 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Int, Eq, Polynomial, Usa2017P2.genFun
Proof uses: id, Equiv.Perm, Usa2017P2.ainvCount, Finset.sum_eq_zero, Finset.univ, Finset.sum, ite, And, LT.lt, Usa2017P2.invPair, Membership.mem, Finset, Subsingleton.elim, ite_eq_right, lt_irrefl, Eq.rec, And.left, Eq.mpr, HPow.hPow, Polynomial.X and 17 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.image_skipEmb The image of skipEmb p is everything except p line 811 source
Source documentation
The image of skipEmb p is everything except p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Finset, Finset.image, Function.Embedding, Usa2017P2.skipEmb, Finset.univ, Finset.erase
Proof uses: Finset.ext, Iff.intro, Membership.mem, And, Exists, Iff.mp, Finset.mem_image, Iff.mpr, Ne, Finset.mem_erase, And.intro, Usa2017P2.skipEmb_ne, Finset.mem_univ, Equiv.Perm, Equiv.swap, Equiv.injective, Eq.trans, Equiv, Eq.symm, Equiv.swap_apply_right and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma image_skipEmb {n : ℕ} (p : Fin (n + 1)) : univ.image (skipEmb p) = univ.erase p := by
…
```
Mentions: Usa2017P2.skipEmb
lemma Usa2017P2.exists_skipEmb_eq line 827 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Exists, Eq, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Membership.mem, Finset, Finset.image, Finset.univ, Eq.mpr, Finset.erase, id, congrArg, Usa2017P2.image_skipEmb, Iff.mpr, And, Finset.mem_erase, And.intro, Finset.mem_univ, Iff.mp, Finset.mem_image, Exists.intro
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Usa2017P2.repr A chosen representative index for a value line 836 source
Source documentation
A chosen representative index for a value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int
Proof uses: dite, Exists, Eq, Classical.choose, Not
10 instances, coercions and auxiliary constants left out.
```
noncomputable def repr {n : ℕ} (m : Fin (n + 1) → ℤ) (v : ℤ) : Fin (n + 1) :=
…
```
lemma Usa2017P2.repr_spec line 839 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Exists, Eq, Usa2017P2.repr
Proof uses: id, Eq.mpr, dite, Classical.choose, Not, congrArg, dite_eq_left, Classical.choose_spec
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P2.eCnt_comp_skipEmb_of_ne Deleting an index whose value w does not match does not change the count of w line 846 source
Source documentation
Deleting an index whose value w does not match does not change the count of w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Ne, Eq, Usa2017P2.eCnt, Function.comp, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Finset.sum, Finset.univ, ite, Usa2017P2.sum_univ_add_skipEmb, rfl, Eq.symm, Multiset.count, Usa2017P2.valMul, Eq.mp, congrArg, zero_add, ite_eq_right, Usa2017P2.sum_if_eq_count
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma eCnt_comp_skipEmb_of_ne {n : ℕ} (m : Fin (n + 1) → ℤ) (q : Fin (n + 1)) {w : ℤ}
    (h : m q ≠ w) : eCnt (m ∘ skipEmb q) w = eCnt m w := by
…
```
Mentions: h, Usa2017P2.eCnt, Usa2017P2.skipEmb
lemma Usa2017P2.genFun_skipEmb_congr Deleting two different indices with the same value gives the same generating function line 858 source
Source documentation
Deleting two different indices with the same value gives the same generating function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Polynomial, Usa2017P2.genFun, Function.comp, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Usa2017P2.genFun_eq_of_valMul_eq, Eq.mpr, Multiset, Usa2017P2.valMul, Multiset.erase, id, congrArg, Usa2017P2.valMul_comp_skipEmb, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma genFun_skipEmb_congr {n : ℕ} (m : Fin (n + 1) → ℤ) {q r : Fin (n + 1)}
    (h : m q = m r) (A : Fin n → ℤ) :
    genFun (m ∘ skipEmb q) A = genFun (m ∘ skipEmb r) A := by
…
```
Mentions: h, Usa2017P2.genFun, Usa2017P2.skipEmb
lemma Usa2017P2.QL The ratio identity, by induction on n line 884 source
Source documentation
The ratio identity, by induction on n.
Proof plan (algebra verified on paper): induction on n.
- Base n = 0: m : Fin 1 → ℤ; eCnt m (m p) = 1 (via eCnt_eq_card_filter, filter is everything by Subsingleton), genFun_one, genFun_zero, qq 1 = 1.
- Step: m : Fin (n+2) → ℤ, θ := m p, e := eCnt m θ. Expand genFun m 0 by genFun_rec (with A = 0; note (0 : Fin _ → ℤ) 0 = 0 and 0 ∘ Fin.succ = 0), rewrite each frontContrib 0 (m q) (m ∘ skipEmb q) as gc m 0 (m q) (frontContrib_eval + gc def), then group by value with sum_eq_sum_image_card using K v := X ^ gc m 0 v * genFun (m ∘ skipEmb (repr v)) 0 where repr v is a chosen index with value v (Classical.choose; the genFun term is independent of the choice by genFun_eq_of_valMul_eq + valMul_comp_skipEmb). Multiply by qq e, split off the v = θ term (Finset.add_sum_erase), and for v ≠ θ apply the IH twice (once to m ∘ skipEmb (repr v) at the index mapping to p — exists because univ.image (skipEmb q) = univ.erase q, cf. the proof of sum_univ_add_skipEmb; once to m ∘ skipEmb p at the index mapping to repr v), using eCnt (m ∘ skipEmb q) w = eCnt m w when m q ≠ w (prove via sum_univ_add_skipEmb + sum_if_eq_count) and Multiset.erase_comm + genFun_eq_of_valMul_eq to identify the double deletions. Everything becomes e * genFun (m ∘ skipEmb p) 0 times ∑ v, X ^ gc m 0 v * qq (eCnt m v) = qq (n+2) (pureId_value).
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Int, Eq, Polynomial, HMul.hMul, Usa2017P2.qq, Usa2017P2.eCnt, Usa2017P2.genFun, Function.comp, Function.Embedding, Usa2017P2.skipEmb
Proof uses: Nat.recAux, Fin.fin_one_eq_zero, Eq.mpr, Finset.card, Finset.filter, Finset.univ, id, congrArg, Usa2017P2.eCnt_eq_card_filter, Finset, Finset.filter_true_of_mem, Membership.mem, congr_arg, of_eq_true, Eq.trans, True, congrFun', Singleton.singleton, Finset.univ_unique, Finset.card_singleton and 82 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
lemma QL {n : ℕ} : ∀ (m : Fin (n + 1) → ℤ) (p : Fin (n + 1)),
    qq (eCnt m (m p)) * genFun m 0 =
      qq (n + 1) * (eCnt m (m p) : ℤ[X]) * genFun (m ∘ skipEmb p) 0 := by
…
```
Mentions: Usa2017P2.qq, Usa2017P2.eCnt, Usa2017P2.genFun, Usa2017P2.skipEmb
lemma Usa2017P2.PL The main induction: the A-inversion generating function does not depend on A line 1013 source
Source documentation
The main induction: the A-inversion generating function does not depend on A.
Proof plan: induction on n. Base n = 0: both sides 1 (genFun_zero). Step n+1: expand genFun m A by genFun_rec + frontContrib_eval (as gc m (A 0)), rewrite each genFun (m ∘ skipEmb p) (A ∘ Fin.succ) to genFun (m ∘ skipEmb p) 0 by IH, group by value (sum_eq_sum_image_card with the repr-kernel as in QL), then: multiply by qq (n+1); use QL at each representative to rewrite qq (n+1) * eCnt m v * genFun (m ∘ skipEmb (repr v)) 0 = qq (eCnt m v) * genFun m 0; the sum becomes genFun m 0 * ∑ v, X ^ gc m (A 0) v * qq (eCnt m v) = genFun m 0 * qq (n+1) by pureId_value; cancel qq (n+1) ≠ 0 (mul_left_cancel₀; qq (n+1) ≠ 0 since its constant coefficient is 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Polynomial, Usa2017P2.genFun, OfNat.ofNat
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Usa2017P2.genFun_zero, Eq.refl, HAdd.hAdd, Finset.sum, Finset.image, Finset.univ, HMul.hMul, Usa2017P2.eCnt, HPow.hPow, Polynomial.X, Usa2017P2.gc, Function.comp, Function.Embedding, Usa2017P2.skipEmb, Usa2017P2.repr, Usa2017P2.frontContrib and 69 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma PL {n : ℕ} : ∀ (m : Fin n → ℤ) (A : Fin n → ℤ), genFun m A = genFun m 0 := by
…
```
Mentions: Usa2017P2.genFun
lemma Usa2017P2.coeff_genFun The coefficient of X^k in the generating function counts permutations with exactly k A-inversions line 1074 source
Source documentation
The coefficient of X^k in the generating function counts permutations with exactly k A-inversions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, Finsupp, Polynomial.coeff, Usa2017P2.genFun, Finset.card, Equiv.Perm, Finset.filter, Usa2017P2.ainvCount, Finset.univ
Proof uses: id, Finset, Finset.sum, Polynomial, HPow.hPow, Polynomial.X, map_sum, LinearMap, RingHom.id, RingHom, Polynomial.lcoeff, Eq.mpr, congrArg, ite, OfNat.ofNat, congrFun', Finset.sum_congr, Eq.refl, Membership.mem, Polynomial.coeff_X_pow and 3 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma coeff_genFun {n : ℕ} (m : Fin n → ℤ) (A : Fin n → ℤ) (k : ℕ) :
    (genFun m A).coeff k =
      ((univ.filter (fun σ : Perm (Fin n) => ainvCount m A σ = k)).card : ℤ) := by
…
```
Mentions: Usa2017P2.genFun, Usa2017P2.ainvCount
problem Usa2017P2.usa2017_p2 USA Mathematical Olympiad 2017, Problem 2 line 1098 source
Source documentation
USA Mathematical Olympiad 2017, Problem 2. The number of permutations of m₁, …, mₙ with exactly k A-inversions equals the number with exactly k B-inversions. Permutations are counted with multiplicity (as positional permutations σ : Equiv.Perm (Fin n)), which is equivalent to the count over distinct arrangements: each distinct arrangement corresponds to the same positive number ∏ (multiplicity)! of positional permutations, independently of A, B and k. Note: the positivity hypothesis hm is actually not needed for the conclusion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LT.lt, OfNat.ofNat, Int, Eq, Finset.card, Equiv.Perm, Finset.filter, Usa2017P2.ainvCount, Finset.univ
Proof uses: Polynomial, Usa2017P2.genFun, Usa2017P2.PL, Finsupp, Polynomial.coeff, Usa2017P2.coeff_genFun, Iff.mp, Int.ofNat_inj, Eq.trans, Eq.symm, Eq.mp, congrArg
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
problem usa2017_p2 {n : ℕ} (m : Fin n → ℕ) (_hm : ∀ i, 0 < m i) (A B : Fin n → ℤ) (k : ℕ) :
    (univ.filter (fun σ : Perm (Fin n) => ainvCount (fun i => (m i : ℤ)) A σ = k)).card =
    (univ.filter (fun σ : Perm (Fin n) => ainvCount (fun i => (m i : ℤ)) B σ = k)).card := by
…
```
Mentions: Usa2017P2.ainvCount