Compfiles/Usa2015P1.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2015, Problem 1

Solve in integers the equation x² + xy + y² = ((x + y) / 3 + 1)³.

Imports (2)
Imported by 1 file
  1. lemma Usa2015P1.iff_comm line 27 source

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

    Statement uses: Iff

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Usa2015P1.abc line 30 source

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

    Statement uses: Int, Ne, OfNat.ofNat, Eq, HPow.hPow, Nat, HMul.hMul, Exists

    Proof uses: Dvd.dvd, of_eq_true, Eq.trans, True, congrArg, Iff.mp, Int.pow_dvd_pow_iff, ne_of_gt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Exists.intro, Eq.symm, Eq.mp, propext, mul_right_inj', lt_of_le_of_ne', Even.pow_nonneg and 3 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  3. determine Usa2015P1.SolutionSet line 41 source

    standard axioms: propext what this means

    Statement uses: Set, Prod, Int

    Proof uses: Union.union, Set.ofPred, Usa2015P1.SolutionSet.match_1, Exists, And, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Neg.neg

    14 instances, coercions and auxiliary constants left out.

  4. problem Usa2015P1.usa2015_p1 line 45 source

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

    Statement uses: Int, Iff, Membership.mem, Prod, Set, Usa2015P1.SolutionSet, Prod.mk, Eq, Rat, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, HDiv.hDiv

    Proof uses: id, Usa2015P1.iff_comm, Union.union, Set.ofPred, Usa2015P1.SolutionSet.match_1, Exists, And, HSub.hSub, Neg.neg, Eq.mpr, Or, implies_congr, Prod.fst, Prod.snd, Eq.refl, congrArg, funext, congr, Eq.trans, Nat.rawCast and 178 more

    205 instances, coercions and auxiliary constants left out.

    Tactic trace: 117 steps

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