Compfiles/Imo1998P6.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1998, Problem 6

Determine the least possible value of f(1998), where f : ℕ+ → ℕ+ satisfies f(n^2 * f(m)) = m * f(n)^2 for all m, n ∈ ℕ+.

Imports (2)
Imported by 1 file
  1. lemma Imo1998P6.f_f_eq line 33 source

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

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

    Proof uses: Eq.mp, congrFun', congrArg, Eq.trans, one_pow, one_mul

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma Imo1998P6.f_injective line 37 source

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

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

    Proof uses: Imo1998P6.f_f_eq, cast, Eq.symm, Eq.trans, Eq.mp, congrArg, propext, PNat.coe_inj, Nat.mul_left_inj, ne_of_gt, pow_pos, PNat.pos

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  3. lemma Imo1998P6.f_sq_d line 46 source

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

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

    Proof uses: Eq.mp, congrArg, one_mul

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma Imo1998P6.f_prod_eq line 49 source

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

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

    Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrArg, congrFun', one_mul, eq_self, congr, mul_assoc, mul_pow, mul_comm, mul_left_comm, Imo1998P6.f_f_eq, forall_congr and 10 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  5. lemma Imo1998P6.f_d_mul line 57 source

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

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

    Proof uses: Imo1998P6.f_prod_eq, Eq.mp, congrArg, congrFun', mul_one

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. lemma Imo1998P6.f_mul_rel line 61 source

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

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

    Proof uses: Eq.mpr, id, congrArg, Imo1998P6.f_prod_eq, Imo1998P6.f_d_mul, mul_assoc, Eq.refl

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma Imo1998P6.f1_dvd line 64 source

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

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

    Proof uses: GT.gt, HSub.hSub, Nat.le.rec, Nat.succ, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, pow_succ, congrFun', pow_zero, mul_comm, mul_one, tsub_self, eq_self, Nat.le, Eq.mpr, id and 121 more

    187 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  8. def Imo1998P6.gf line 92 source

    standard axioms: propext what this means

    Statement uses: PNat, Nat

    Proof uses: HDiv.hDiv, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

  9. lemma Imo1998P6.gf_spec line 94 source

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

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

    Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, Imo1998P6.gf.eq_1, Nat.mul_div_cancel', Imo1998P6.f1_dvd, Eq.refl

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  10. lemma Imo1998P6.gf_pos line 97 source

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

    Statement uses: PNat, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, LT.lt, Imo1998P6.gf

    Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, Imo1998P6.gf.eq_1, Nat.div_pos, Nat.le_of_dvd, PNat.pos, Imo1998P6.f1_dvd

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  11. lemma Imo1998P6.gf_one line 102 source

    standard axioms: propext what this means

    Statement uses: PNat, Eq, Nat, Imo1998P6.gf, OfNat.ofNat

    Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, Imo1998P6.gf.eq_1, Nat.div_self, PNat.pos, Eq.refl

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  12. lemma Imo1998P6.gf_mul line 105 source

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

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

    Proof uses: id, Eq.mpr, HDiv.hDiv, congrArg, Nat.div_mul_div_comm, Imo1998P6.f1_dvd, Eq.symm, PNat.mul_coe, Imo1998P6.f_mul_rel, of_eq_true, Eq.trans, True, Nat.mul_div_mul_left, LT.lt, eq_true, True.intro, eq_self

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  13. lemma Imo1998P6.gf_invol line 113 source

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

    Statement uses: PNat, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Imo1998P6.gf, Subtype.mk, LT.lt, Imo1998P6.gf_pos

    Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, id, congrArg, Eq.trans, congrFun', one_pow, mul_comm, mul_one, PNat.eq, Imo1998P6.gf_spec, Mathlib.Tactic.Ring.of_lift, Mathlib.Tactic.Ring.CSLift.lift, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast and 79 more

    129 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  14. lemma Imo1998P6.gf_prime line 126 source

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

    Statement uses: PNat, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Nat.Prime, Imo1998P6.gf

    Proof uses: Iff.mpr, And, LE.le, LT.lt, Not, Dvd.dvd, Nat.prime_def_lt', And.intro, Decidable.byContradiction, dite, False, Subtype.mk, Imo1998P6.gf_pos, Imo1998P6.gf_invol, absurd, NeZero.mk, LT.lt.ne', Eq.mp, congrFun', congrArg and 96 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  15. lemma Imo1998P6.f_1998_eq line 148 source

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

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

    Proof uses: Eq.mpr, id, congrArg, Imo1998P6.gf_spec, Eq.refl, congrFun', Eq.trans, Imo1998P6.gf_mul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 16 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  16. theorem Imo1998P6.f_1998_ge line 155 source

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

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

    Proof uses: Nat.Prime, And, Ne, GE.ge, dite, Nat.casesAuxOn, False.elim, Eq.mp, False, eq_false_of_decide, Eq.refl, Bool, Bool.false, HAdd.hAdd, eq_false, Eq.trans, True, congr, congrArg, congrFun' and 122 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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

  17. def Imo1998P6.primeSwap line 179 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: Imo1998P6.primeSwap.match_1, Unit, OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  18. def Imo1998P6.g line 182 source

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

    Statement uses: Nat

    Proof uses: List.prod, List.map, Imo1998P6.primeSwap, Nat.primeFactorsList

    2 instances, coercions and auxiliary constants left out.

  19. lemma Imo1998P6.primeSwap_invol line 184 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, Imo1998P6.primeSwap

    Proof uses: dite, OfNat.ofNat, Eq.refl, Eq.symm, Not, of_eq_true, Eq.trans, True, congrFun', congrArg, Imo1998P6.primeSwap.match_1, Unit, eq_self

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  20. lemma Imo1998P6.primeSwap_prime line 189 source

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

    Statement uses: Nat, Nat.Prime, Imo1998P6.primeSwap

    Proof uses: dite, Or, Eq, OfNat.ofNat, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, Not, of_eq_true, Eq.trans, True, congrArg, Unit, False, implies_congr, eq_false and 4 more

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  21. lemma Imo1998P6.g_mul line 194 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1998P6.g, HMul.hMul

    Proof uses: id, List.Perm, List.map, Imo1998P6.primeSwap, Nat.primeFactorsList, HAppend.hAppend, List, List.Perm.map, Nat.perm_primeFactorsList_mul, Eq.mpr, List.prod, congrArg, List.Perm.prod_eq, Eq.mp, List.map_append, List.prod_append, Eq.refl

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  22. lemma Imo1998P6.g_prime line 200 source

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

    Statement uses: Nat, Nat.Prime, Eq, Imo1998P6.g, Imo1998P6.primeSwap

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.prod, List.map, Nat.primeFactorsList, List.cons, List.nil, List, Nat.primeFactorsList_prime, List.map_cons, List.map_nil, mul_one, eq_self

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  23. lemma Imo1998P6.g_ne_zero line 203 source

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

    Statement uses: Nat, Ne, Imo1998P6.g, OfNat.ofNat

    Proof uses: id, List.prod_ne_zero, List.map, Imo1998P6.primeSwap, Nat.primeFactorsList, Eq.mpr, Not, Membership.mem, List, Exists, And, Eq, congrArg, propext, List.mem_map, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, Nat.Prime.ne_zero and 2 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  24. lemma Imo1998P6.g_pos line 208 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1998P6.g

    Proof uses: Nat.pos_of_ne_zero, Imo1998P6.g_ne_zero

    2 instances, coercions and auxiliary constants left out.

  25. lemma Imo1998P6.g_invol line 210 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1998P6.g

    Proof uses: Nat.strongRecOn, LT.lt, dite, of_eq_true, Eq.trans, True, congrFun', congrArg, List, List.map, Imo1998P6.primeSwap, Nat.primeFactorsList, List.nil, List.prod, Nat.primeFactorsList_one, List.map_nil, eq_self, Eq.symm, Not, And and 91 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  26. lemma Imo1998P6.g_func_eq line 224 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1998P6.g, HMul.hMul, HPow.hPow

    Proof uses: Eq.mpr, id, congrArg, Imo1998P6.g_mul, pow_ne_zero, Imo1998P6.g_ne_zero, sq, Imo1998P6.g_invol, mul_comm, Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  27. lemma Imo1998P6.g_1998 line 227 source

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

    Statement uses: Eq, Nat, Imo1998P6.g, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  28. def Imo1998P6.gPNat line 229 source

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

    Statement uses: PNat

    Proof uses: Subtype.mk, Nat, LT.lt, OfNat.ofNat, Imo1998P6.g

    4 instances, coercions and auxiliary constants left out.

  29. lemma Imo1998P6.gPNat_func_eq line 231 source

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

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

    Proof uses: PNat.eq, id, Eq.mpr, Imo1998P6.g, congrArg, PNat.mul_coe, PNat.pow_coe, Imo1998P6.g_func_eq, PNat.ne_zero

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  30. lemma Imo1998P6.gPNat_1998 line 239 source

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

    Statement uses: Eq, PNat, Imo1998P6.gPNat, OfNat.ofNat, Nat

    Proof uses: PNat.eq, of_eq_true, Eq.trans, True, congrFun', congrArg, NeZero.mk, LT.lt.ne', Imo1998P6.g, LT.lt, Imo1998P6.g_1998, Subtype.mk.congr_simp, eq_self

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  31. theorem Imo1998P6.imo1998_p6_mem line 245 source

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

    Statement uses: Membership.mem, PNat, Set, Set.ofPred, Exists, And, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Exists.intro, Imo1998P6.gPNat, And.intro, Imo1998P6.gPNat_func_eq, Imo1998P6.gPNat_1998

    21 instances, coercions and auxiliary constants left out.

  32. theorem Imo1998P6.imo1998_p6_lb line 249 source

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

    Statement uses: PNat, Membership.mem, Set, Set.ofPred, Exists, And, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, LE.le

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Imo1998P6.f_1998_ge

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  33. determine Imo1998P6.answer line 258 source

    standard axioms: propext what this means

    Statement uses: PNat

    Proof uses: OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  34. problem Imo1998P6.imo1998_p6 line 260 source

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

    Statement uses: IsLeast, PNat, Set.ofPred, Exists, And, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Imo1998P6.answer

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Imo1998P6.imo1998_p6_mem, Imo1998P6.imo1998_p6_lb

    35 instances, coercions and auxiliary constants left out.