Compfiles/Imo2012P6.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

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2012, Problem 6

Find all positive integers n for which there exist non-negative integers a₁, a₂, ..., aₙ such that 1/2^a₁ + 1/2^a₂ + ··· + 1/2^aₙ = 1/3^a₁ + 2/3^a₂ + ··· + n/3^aₙ = 1

Imports (2)
Imported by 1 file
  1. determine Imo2012P6.solution_set line 28 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, Or, Eq, HMod.hMod, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. def Imo2012P6.IsSolution line 30 source

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

    Statement uses: Nat

    Proof uses: Exists, And, LT.lt, OfNat.ofNat, Eq, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow

    12 instances, coercions and auxiliary constants left out.

  3. lemma Imo2012P6.sum_id line 36 source

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

    Statement uses: Nat, Eq, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HMul.hMul, HAdd.hAdd

    Proof uses: Finset, Finset.erase, Finset.range, Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, Not, LE.le, True, congr, congrArg, congrFun', Nat.succ, LT.lt, Ne, iff_self, Eq.mpr and 7 more

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  4. lemma Imo2012P6.solution_5 line 42 source

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

    Statement uses: Imo2012P6.IsSolution, OfNat.ofNat, Nat

    Proof uses: Exists.intro, And, LT.lt, Eq, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow, ite, Membership.mem, Finset, Finset.Ico, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl and 57 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  5. lemma Imo2012P6.solution_9 line 48 source

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

    Statement uses: Imo2012P6.IsSolution, OfNat.ofNat, Nat

    Proof uses: Exists.intro, And, LT.lt, Eq, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow, ite, Membership.mem, Finset, Finset.Ico, of_decide_eq_true, Lean.Sym.decide_isTrue_congr, NatCast.natCast, Rat.mk', Int.ofNat, Nat.divExact, HMul.hMul and 219 more

    105 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. lemma Imo2012P6.ind_4k1_to_4k2 If n=4k+1 is a solution then n=4k+2 is also a solution line 53 source

    Source comment

    If n=4k+1 is a solution then n=4k+2 is also a solution.

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

    Statement uses: Nat, Imo2012P6.IsSolution, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    Proof uses: And, LT.lt, Eq, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow, Finset, ite, Membership.mem, Exists.intro, And.intro, Eq.mpr, id, congrArg, Finset.sum_Icc_succ_top, Finset.erase, Finset.sum_congr, rfl

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

    lemma ind_4k1_to_4k2 : ∀ k, IsSolution (4 * k + 1) → IsSolution (4 * k + 2) := by
…

    Mentions: Imo2012P6.IsSolution

  7. lemma Imo2012P6.ind_4k1_to_4k13 If n=4k+1 is a solution then n=4k+13 is also a solution line 73 source

    Source comment

    If n=4k+1 is a solution then n=4k+13 is also a solution.

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

    Statement uses: Nat, Imo2012P6.IsSolution, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    Proof uses: And, LT.lt, Eq, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow, ite, LE.le, Finset, Membership.mem, Exists.intro, And.intro, Eq.mpr, id, congrArg, Finset.sum_Icc_succ_top, Finset.erase, Finset.sum_congr and 1 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

    lemma ind_4k1_to_4k13 : ∀ k, IsSolution (4 * k + 1) → IsSolution (4 * k + 13) := by
…

    Mentions: Imo2012P6.IsSolution

  8. problem Imo2012P6.imo2012_p6 line 106 source

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

    Statement uses: Eq, Set, Nat, Set.ofPred, Imo2012P6.IsSolution, Imo2012P6.solution_set

    Proof uses: Set.ext, Iff.intro, Membership.mem, And, LT.lt, OfNat.ofNat, Rat, Finset.sum, Finset.Icc, HDiv.hDiv, HPow.hPow, Finset, Finset.sup, HMul.hMul, HSub.hSub, Trans.trans, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr and 137 more

    159 instances, coercions and auxiliary constants left out.

    Tactic trace: 78 steps

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