Compfiles/Imo2009P3.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2009, Problem 3

Suppose that $s_1, s_2, s_3, \ldots$ is a strictly increasing sequence of positive integers such that the subsequences $$s_{s_1}, s_{s_2}, s_{s_3}, \ldots \quad\text{and}\quad s_{s_1+1}, s_{s_2+1}, s_{s_3+1}, \ldots$$ are both arithmetic progressions. Prove that the sequence $s_1, s_2, s_3, \ldots$ is itself an arithmetic progression.

Imports (2)
Imported by 1 file
  1. def Imo2009P3.IsArithProg A sequence f : ℕ → ℕ is an arithmetic progression line 30 source

    Source documentation

    A sequence f : ℕ → ℕ is an arithmetic progression.

    no axioms what this means

    Statement uses: Nat

    Proof uses: Exists, Eq, HAdd.hAdd, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

    def IsArithProg (f : ℕ → ℕ) : Prop := ∃ d : ℕ, ∀ n, f (n + 1) = f n + d
…

    Mentions: f

  2. lemma Imo2009P3.IsArithProg_iff line 37 source

    standard axioms: propext what this means

    Statement uses: Nat, Iff, Imo2009P3.IsArithProg, Exists, Eq, HAdd.hAdd, HMul.hMul

    Proof uses: Iff.intro, OfNat.ofNat, Exists.intro, Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', MulZeroClass.mul_zero, zero_add, eq_self, Eq.mpr, id, congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 24 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  3. lemma Imo2009P3.strictMono_add_right_le line 43 source

    standard axioms: propext what this means

    Statement uses: Nat, StrictMono, LE.le, HAdd.hAdd

    Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, add_zero, Eq.mpr, id, Eq, LT.lt, propext, Nat.add_one_le_iff, LE.le.trans_lt, lt_add_one

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  4. problem Imo2009P3.imo2009_p3 line 53 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, StrictMono, LT.lt, OfNat.ofNat, Imo2009P3.IsArithProg, HAdd.hAdd

    Proof uses: Eq.mpr, Exists, Eq, HMul.hMul, id, congrArg, propext, Imo2009P3.IsArithProg_iff, Eq.mp, lt_add_one, LE.le, StrictMono.monotone, Iff.mpr, Order.add_one_le_iff, LT.lt.trans_le, congr, Eq.trans, congrFun', MulZeroClass.mul_zero, zero_add and 143 more

    182 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

    Open to load the checked before-and-after goal states.