Compfiles/Imo1996P4.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1996, Problem 4

The positive integers a and b are such that the numbers 15a + 16b and 16a − 15b are both squares of positive integers. What is the least possible value that can be taken on by the smaller of these two squares?

Imports (2)
Imported by 1 file
  1. determine Imo1996P4.solution line 28 source

    no axioms what this means

    Statement uses: Int

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  2. def Imo1996P4.S line 30 source

    standard axioms: propext what this means

    Statement uses: Set, Int

    Proof uses: Set.ofPred, Exists, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, HSub.hSub, Min.min

    14 instances, coercions and auxiliary constants left out.

  3. lemma Imo1996P4.coprime line 38 source

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

    Statement uses: Int, Nat, Nat.Prime, Not, Dvd.dvd, IsCoprime

    Proof uses: Eq.mpr, Nat.Coprime, Int.natAbs, id, Eq, congrArg, propext, Int.isCoprime_iff_nat_coprime, Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Mathlib.Tactic.Contrapose.contrapose₄, Int.ofNat_dvd_left

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  4. lemma Imo1996P4.false_of_zero_eqMod_pos line 45 source

    standard axioms: propext what this means

    Statement uses: Nat, Int.ModEq, Int, OfNat.ofNat, LT.lt, False

    Proof uses: Dvd.dvd, Iff.mp, Int.modEq_zero_iff_dvd, Int.ModEq.symm, LE.le, Nat.le_of_dvd, Int.ofNat_dvd, Nat.not_le_of_lt

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. problem Imo1996P4.imo1996_p4 line 52 source

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

    Statement uses: And, Membership.mem, Int, Set, Imo1996P4.S, Imo1996P4.solution, LE.le

    Proof uses: LT.lt, OfNat.ofNat, Exists, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, HSub.hSub, Min.min, Eq.mp, Set.ofPred, congrFun', congrArg, funext, Eq.trans, of_eq_true, True, congr, and_self and 126 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 104 steps

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