Compfiles/Imo2007P5.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2007, Problem 5

Let a and b be positive integers. Show that if 4ab - 1 divides (4a² - 1)² then a = b.

Imports (3)
Imported by 1 file
  1. lemma Imo2007P5.bad_symm line 33 source

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

    Statement uses: Int, Nat, Dvd.dvd, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow

    Proof uses: Eq.mpr, id, Eq, congrArg, mul_right_comm, HAdd.hAdd, sub_sq', add_comm, Eq.symm, dvd_mul_of_dvd_left, Int.ModEq, propext, Int.modEq_zero_iff_dvd, Int.ModEq.trans, Int.ModEq.pow, Int.ModEq.sub_right, one_pow, Int.ModEq.symm, Int.modEq_sub, Eq.mp and 5 more

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  2. lemma Imo2007P5.bad_exists_descent line 44 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Nat, And, Exists, Dvd.dvd, HSub.hSub, HMul.hMul, HPow.hPow

    Proof uses: Eq, Int.ModEq, Eq.mpr, id, congrArg, Eq.mp, Eq.symm, mul_assoc, sq, Int.ModEq.refl, Neg.neg, Int.ModEq.symm, propext, Int.modEq_iff_dvd, HAdd.hAdd, sub_neg_eq_add, sub_add_cancel, Exists.intro, rfl, Int.ModEq.trans and 38 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

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

  3. lemma Imo2007P5.nat_pred_descent line 96 source

    no axioms what this means

    Statement uses: Nat, DecidablePred, Exists, And, LT.lt, Not

    Proof uses: forall_not_of_not_exists, Exists.elim, Nat.find, False, Nat.find_spec, Nat.find_min, And.left, And.right

    2 instances, coercions and auxiliary constants left out.

  4. theorem Imo2007P5.generalized_imo2007_p5 line 101 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Nat, Dvd.dvd, HSub.hSub, HMul.hMul, HPow.hPow, Eq

    Proof uses: And, Exists, Exists.elim, Imo2007P5.bad_exists_descent, Exists.intro, And.intro, And.left, And.right, Not, Imo2007P5.nat_pred_descent, Classical.propDecidable, Decidable.byContradiction, Or.elim, False, lt_or_gt_of_ne, Imo2007P5.bad_symm

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  5. problem Imo2007P5.imo2007_p5 line 116 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Dvd.dvd, HSub.hSub, HMul.hMul, HPow.hPow, Nat, Eq

    Proof uses: Exists, CanLift.prf, LE.le, le_of_lt, Iff.mp, Int.natCast_pos, Imo2007P5.generalized_imo2007_p5, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, congrArg

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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