Compfiles/Usa2019P1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2019, Problem 1

Let ℕ+ be the set of positive integers. A function f: ℕ+ → ℕ+ satisfies the equation

fᶠ⁽ⁿ⁾(n)⬝f²(n) = n^2

for all positive integers n, where fᵏ(m) means f iterated k times on m. Given this information, determine all possible values of f(1000).

Imports (3)
Imported by 1 file
  1. lemma Usa2019P1.f_injective line 35 source

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

    Statement uses: PNat, Eq, HMul.hMul, Nat.iterate, HPow.hPow, Nat, OfNat.ofNat, Function.Injective

    Proof uses: eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, LT.lt, Nat.casesAuxOn, Subtype.mk, id, False.elim, Eq.mp, False, HAdd.hAdd, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self, Eq.mpr and 7 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  2. lemma Usa2019P1.lemma_1 line 68 source

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

    Statement uses: PNat, Eq, HMul.hMul, Nat.iterate, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Function.iterate_fixed, Trans.trans, Eq.symm, Function.Injective.iterate, Usa2019P1.f_injective

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma Usa2019P1.lemma_2 line 85 source

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

    Statement uses: PNat, Eq, HMul.hMul, Nat.iterate, HPow.hPow, Nat, OfNat.ofNat, Odd

    Proof uses: id, Eq.mpr, congrArg, Eq.refl, Eq.mp, propext, mul_left_inj, sq, Nat.recAux, of_eq_true, Eq.trans, True, congrFun', MulZeroClass.mul_zero, eq_self, HAdd.hAdd, Nat.succ, Nat.mul_succ, Function.comp, Function.iterate_add and 3 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

  4. lemma Usa2019P1.pnat_odd_mul line 131 source

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

    Statement uses: PNat, Eq, HMul.hMul, Odd, Nat, And

    Proof uses: LT.lt, OfNat.ofNat, Subtype.mk, id, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Odd.mul, Eq.mp, congrArg, PNat.mk_coe, Iff.mp, Nat.odd_mul

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  5. lemma Usa2019P1.lemma_3 line 144 source

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

    Statement uses: PNat, Eq, HMul.hMul, Nat.iterate, HPow.hPow, Nat, OfNat.ofNat, Odd

    Proof uses: PNat.strongInductionOn, LT.lt, dite, And.right, Usa2019P1.pnat_odd_mul, Eq.mp, congrArg, sq, Eq.mpr, id, Usa2019P1.lemma_1, rfl, Not, And.left, And, Decidable.byContradiction, Or, False, propext, not_and_or and 7 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  6. determine Usa2019P1.solution_set line 191 source

    no axioms what this means

    Statement uses: Set, PNat

    Proof uses: Set.ofPred, Even, Nat

    2 instances, coercions and auxiliary constants left out.

  7. problem Usa2019P1.usa2019_p1 line 193 source

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

    Statement uses: PNat, Iff, Membership.mem, Set, Usa2019P1.solution_set, Exists, And, Eq, HMul.hMul, Nat.iterate, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Iff.intro, ite, exists_eq, Eq.mpr, id, congrArg, Eq.trans, congrFun', ite_congr, Eq.refl, Not, True, eq_self, ite_true, Iff.mpr, right_eq_ite_iff, Eq.symm, of_eq_true, ite_eq_left_of_eq_true, Function.comp and 29 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 56 steps

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