`Compfiles/Imo2016P5.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

17 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2016, Problem 5

The equation

(x - 1)(x - 2) ... (x - 2016) = (x - 1)(x - 2) ... (x - 2016)

is written on the board. What is the least possible value of k for which it is possible to erase exactly k of these 4032 factors such that at least one factor remains on each side and the resulting equation has no real solutions?

Imports (5)

Imported by 1 file

Compfiles.lean

lemma Imo2016P5.lemma1 line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, DecidablePred, Eq, Nat, HAdd.hAdd, Finset.card, SDiff.sdiff, Finset.filter
Proof uses: Finset.card_sdiff_add_card_eq_card, Finset.filter_subset
3 instances, coercions and auxiliary constants left out.
lemma Imo2016P5.u_neg_iff line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Iff, LT.lt, HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat, And
Proof uses: Eq.mpr, Or, id, Eq, congrArg, propext, mul_neg_iff, Iff.intro, And.intro, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, HPow.hPow and 57 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.v_neg_iff line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Iff, LT.lt, HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat, And
Proof uses: Eq.mpr, Or, id, Eq, congrArg, propext, mul_neg_iff, Iff.intro, And.intro, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, HPow.hPow and 52 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_P_fst line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: rfl, Eq.mpr, id, congrArg, Finset.prod_range_succ', of_eq_true, Eq.trans, True, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_natCast, Nat.cast_one, eq_self, eq_true, True.intro and 40 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_P_snd line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: rfl, Eq.mpr, id, congrArg, Finset.prod_range_succ, HMul, Eq.rec, Eq.refl, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_natCast, eq_self, eq_true and 1 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_Q_fst line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: rfl, Eq.mpr, id, congrArg, Finset.prod_range_succ', of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_natCast, eq_self, eq_true, True.intro, Finset.prod_congr and 40 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_Q_snd line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: rfl, Eq.mpr, id, congrArg, Finset.prod_range_succ, HMul, Eq.rec, Eq.refl, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_natCast, eq_self, eq_true and 1 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_repair_P Re-pairing of the left-hand product: isolate 1 and 2016, and group the remaining factors into pairs (4j+4, 4j+5) line 106 source
Source documentation
Re-pairing of the left-hand product: isolate 1 and 2016, and group the remaining factors into pairs (4j+4, 4j+5).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HMul.hMul, HSub.hSub, HAdd.hAdd
Proof uses: Finset.prod_mul_distrib, Eq.mpr, id, congrArg, Imo2016P5.prod_P_fst, Imo2016P5.prod_P_snd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 34 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma prod_repair_P (x : ℝ) :
    (∏ k ∈ Finset.range 504, ((x - (4 * (k : ℝ) + 1)) * (x - (4 * (k : ℝ) + 4))))
      = (x - 1) * (x - 2016)
        * ∏ j ∈ Finset.range 503, ((x - (4 * (j : ℝ) + 4)) * (x - (4 * (j : ℝ) + 5))) := by
…
```
lemma Imo2016P5.prod_repair_Q Re-pairing of the right-hand product: isolate 2 and 2015, and group the remaining factors into pairs (4j+3, 4j+6) line 119 source
Source documentation
Re-pairing of the right-hand product: isolate 2 and 2015, and group the remaining factors into pairs (4j+3, 4j+6).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Finset.prod, Nat, Finset.range, OfNat.ofNat, HMul.hMul, HSub.hSub, HAdd.hAdd
Proof uses: Finset.prod_mul_distrib, Eq.mpr, id, congrArg, Imo2016P5.prod_Q_fst, Imo2016P5.prod_Q_snd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 33 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma prod_repair_Q (x : ℝ) :
    (∏ k ∈ Finset.range 504, ((x - (4 * (k : ℝ) + 2)) * (x - (4 * (k : ℝ) + 3))))
      = (x - 2) * (x - 2015)
        * ∏ j ∈ Finset.range 503, ((x - (4 * (j : ℝ) + 3)) * (x - (4 * (j : ℝ) + 6))) := by
…
```
lemma Imo2016P5.key The two products remaining on the board never take the same real value: the left one is always strictly smaller than the right one line 132 source
Source documentation
The two products remaining on the board never take the same real value: the left one is always strictly smaller than the right one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Ne, Finset.prod, Nat, Finset.range, OfNat.ofNat, HMul.hMul, HSub.hSub, HAdd.hAdd
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, HPow.hPow, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos and 121 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 277 steps (first 200 of 277)
Open to load the checked before-and-after goal states.
```
lemma key (x : ℝ) :
    (∏ k ∈ Finset.range 504, ((x - (4 * (k : ℝ) + 1)) * (x - (4 * (k : ℝ) + 4)))) ≠
    (∏ k ∈ Finset.range 504, ((x - (4 * (k : ℝ) + 2)) * (x - (4 * (k : ℝ) + 3)))) := by
…
```
lemma Imo2016P5.setL line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, SDiff.sdiff, Finset.Icc, OfNat.ofNat, Finset.filter, Or, HMod.hMod, Union.union, Finset.image, HAdd.hAdd, HMul.hMul, Finset.range
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Not, Exists, LT.lt, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, Or.inr, Exists.intro, HSub.hSub, HDiv.hDiv and 2 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.setR line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Nat, SDiff.sdiff, Finset.Icc, OfNat.ofNat, Finset.filter, Or, HMod.hMod, Union.union, Finset.image, HAdd.hAdd, HMul.hMul, Finset.range
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Not, Exists, LT.lt, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, Or.inl, Exists.intro, HDiv.hDiv, Or.inr and 1 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.disjL line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Disjoint, Finset, Nat, Finset.image, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.range
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, LT.lt, Exists, False, Eq.mp, Eq.trans, funext, congrFun'
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.disjR line 393 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Disjoint, Finset, Nat, Finset.image, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.range
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, LT.lt, Exists, False, Eq.mp, Eq.trans, funext, congrFun'
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2016P5.prod_erase_aux After erasing the factors indexed by n % 4 = 2, 3 on the left and by n % 4 = 0, 1 on the right, the resulting equation has no real solution line 404 source
Source documentation
After erasing the factors indexed by n % 4 = 2, 3 on the left and by n % 4 = 0, 1 on the right, the resulting equation has no real solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Ne, Finset.prod, Nat, SDiff.sdiff, Finset, Finset.Icc, OfNat.ofNat, Finset.filter, Or, Eq, HMod.hMod, HSub.hSub
Proof uses: Finset.range, HMul.hMul, HAdd.hAdd, Eq.mpr, Union.union, Finset.image, id, congrArg, Imo2016P5.setL, Finset.prod_union, Imo2016P5.disjL, Finset.prod_image, Membership.mem, Set, Eq.symm, Finset.prod_mul_distrib, Finset.prod_congr, rfl, congrFun', congr and 54 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma prod_erase_aux (x : ℝ) :
    (∏ i ∈ Finset.Icc (1 : ℕ) 2016 \ ((Finset.Icc (1 : ℕ) 2016).filter (fun n ↦ n % 4 = 2 ∨ n % 4 = 3)),
        (x - (i : ℝ))) ≠
    (∏ i ∈ Finset.Icc (1 : ℕ) 2016 \ ((Finset.Icc (1 : ℕ) 2016).filter (fun n ↦ n % 4 = 0 ∨ n % 4 = 1)),
        (x - (i : ℝ))) := by
…
```
determine Imo2016P5.solution_value line 430 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo2016P5.imo2016_p5 line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, And, LT.lt, Finset.Icc, OfNat.ofNat, Eq, HAdd.hAdd, Finset.card, Not, Real, Finset.prod, SDiff.sdiff, HSub.hSub, Imo2016P5.solution_value
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Eq.mpr, id, congrArg, Set.mem_ofPred_eq, Exists.intro, Finset.filter, Or, HMod.hMod, LE.le, LE.ofSetLike, Finset.filter_subset, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 54 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.