Compfiles/Usa1987P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1987, Problem 1

Determine all solutions to

(m² + n)(m + n²) = (m - n)³

where m and n are non-zero integers.

Imports (3)
Imported by 1 file
  1. lemma Usa1987P1.lemma2 line 32 source

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

    Statement uses: Int, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Or, IsSquare

    Proof uses: Ne, eq_or_ne, Or.inr, Eq.refl, Eq.symm, Eq.mpr, id, Eq.trans, False, congrArg, eq_false, or_false, Dvd.dvd, Dvd.intro_left, Eq.mp, propext, Int.pow_dvd_pow_iff, two_ne_zero, mul_right_inj', pow_ne_zero and 4 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  2. determine Usa1987P1.solution_set line 47 source

    no axioms what this means

    Statement uses: Set, Prod, Int

    Proof uses: Insert.insert, Prod.mk, Neg.neg, OfNat.ofNat, Singleton.singleton

    4 instances, coercions and auxiliary constants left out.

  3. problem Usa1987P1.usa1987_p1 line 50 source

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

    Statement uses: Int, Iff, Membership.mem, Prod, Set, Usa1987P1.solution_set, Prod.mk, And, Ne, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub

    Proof uses: Iff.intro, id, Neg.neg, Or, Not, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congr, congrArg, Prod.mk.injEq, of_eq_true, True, False, congrFun', not_false_eq_true, Even.neg_pow, Even, one_pow and 154 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 168 steps

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