Compfiles/Usa2014P2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2014, Problem 2

Let ℤ be the set of integers. Find all functions f : ℤ → ℤ such that x * f(2 * f(y) - x) + y ^ 2 * f(2 * x - f(y)) = (f(x) ^ 2) / x + f(y * f(y)) for all x, y ∈ ℤ with x ≠ 0.

Imports (2)
Imported by 1 file
  1. def Usa2014P2.P line 27 source

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

    Statement uses: Int

    Proof uses: Ne, OfNat.ofNat, Eq, Rat, HAdd.hAdd, HMul.hMul, HSub.hSub, HPow.hPow, Nat, HDiv.hDiv

    17 instances, coercions and auxiliary constants left out.

  2. determine Usa2014P2.S line 30 source

    standard axioms: propext what this means

    Statement uses: Set, Int

    Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton, HPow.hPow, Nat

    12 instances, coercions and auxiliary constants left out.

  3. lemma Usa2014P2.mpr line 34 source

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

    Statement uses: Int, Membership.mem, Set, Usa2014P2.S, Usa2014P2.P

    Proof uses: Ne, OfNat.ofNat, Eq, Singleton.singleton, HPow.hPow, Nat, Rat, HAdd.hAdd, HMul.hMul, HSub.hSub, HDiv.hDiv, of_eq_true, Eq.trans, True, congr, congrArg, Int.cast_zero, MulZeroClass.mul_zero, add_zero, congrFun' and 7 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  4. lemma Usa2014P2.exists_prime_and_not_dvd line 40 source

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

    Statement uses: Int, Ne, OfNat.ofNat, Exists, And, Prime, Not, Dvd.dvd

    Proof uses: Nat, LE.le, HAdd.hAdd, Int.natAbs, Nat.Prime, Nat.exists_infinite_primes, Exists.intro, And.intro, Iff.mp, Nat.prime_iff_prime_int, Eq.mp, Nat.succ, LT.lt, congrArg, propext, Nat.succ_le_iff, Nat.le_of_dvd, Iff.mpr, Int.natAbs_pos, Int.ofNat_dvd and 2 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  5. problem Usa2014P2.usa2014_p2 line 51 source

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

    Statement uses: Int, Iff, Usa2014P2.P, Membership.mem, Set, Usa2014P2.S

    Proof uses: Iff.intro, Eq, OfNat.ofNat, Decidable.byContradiction, Not, And, Prime, Dvd.dvd, Exists, False, Usa2014P2.exists_prime_and_not_dvd, Ne, Prime.ne_zero, HPow.hPow, Nat, Exists.intro, HMul.hMul, HSub.hSub, Eq.mpr, Rat and 201 more

    209 instances, coercions and auxiliary constants left out.

    Tactic trace: 167 steps

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