Compfiles/Imo1990P4.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1990, Problem 4

Let $\mathbb{Q^+}$ be the set of positive rational numbers. Construct a function $f :\mathbb{Q^+}\rightarrow\mathbb{Q^+}$ such that $f(xf(y)) = \frac{f(x)}{y}$ for all $x, y\in\mathbb{Q^+}$.

Imports (6)
Imported by 1 file
  1. abbrev Imo1990P4.PRat line 32 source

    standard axioms: Quot.sound, propext what this means

    Proof uses: Subtype, Rat, LT.lt, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  2. theorem Imo1990P4.Nat.Primes.toPnat_val line 42 source

    standard axioms: propext what this means

    Statement uses: Nat.Primes, Eq, Nat, Nat.Prime

    Proof uses: Eq.refl

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Imo1990P4.Nat.Primes.PNat_mk_val line 46 source

    standard axioms: propext what this means

    Statement uses: Nat.Primes, LT.lt, Nat, OfNat.ofNat, Nat.Prime, Eq, Subtype, Subtype.mk

    Proof uses: Eq.refl

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Imo1990P4.PRat.num_toNat line 50 source

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

    Statement uses: Imo1990P4.PRat, Eq, Int, Int.toNat, Rat.num, Rat, LT.lt, OfNat.ofNat

    Proof uses: Eq.mpr, LE.le, id, Eq.trans, Max.max, congrFun', congrArg, Int.ofNat_toNat, le_of_lt, Subtype.prop

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. theorem Imo1990P4.PRat.cast_num_toNat line 56 source

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

    Statement uses: Imo1990P4.PRat, Eq, Rat, Int.toNat, Rat.num, LT.lt, OfNat.ofNat

    Proof uses: Eq.mpr, Int, id, congrArg, Eq.symm, Iff.mpr, LE.le, Int.natCast_toNat_eq_self, le_of_lt, Subtype.prop, Eq.refl

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  6. theorem Imo1990P4.PRat.num_toNat_div_den line 64 source

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

    Statement uses: Imo1990P4.PRat, Eq, Rat, HDiv.hDiv, Int.toNat, Rat.num, LT.lt, OfNat.ofNat, Rat.den

    Proof uses: Eq.mpr, id, congrFun', congrArg, Imo1990P4.PRat.cast_num_toNat, Rat.num_div_den, Eq.refl

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  7. instance Imo1990P4.coePRatNNRat line 69 source

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

    Statement uses: Coe, Imo1990P4.PRat, NNRat

    Proof uses: Coe.mk, Imo1990P4.coePRatNNRat.match_1, Rat, LT.lt, OfNat.ofNat, Subtype.mk, LE.le

    4 instances, coercions and auxiliary constants left out.

  8. instance Imo1990P4.coePrimesPRat line 73 source

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

    Statement uses: Coe, Nat.Primes, Imo1990P4.PRat

    Proof uses: Coe.mk, Subtype.mk, Rat, LT.lt, OfNat.ofNat, Nat, Nat.Prime

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. theorem Imo1990P4.PRat.prime_induction line 78 source

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

    Statement uses: Imo1990P4.PRat, OfNat.ofNat, Rat, Nat.Primes, HMul.hMul, Subtype, LT.lt, Subtype.mk, Nat, Nat.Prime, HDiv.hDiv

    Proof uses: Prod, Prod.fst, Prod.snd, Eq.mpr, id, Eq, induction_on_primes, of_eq_true, Eq.trans, True, forall_congr, False, Eq.substr, congrArg, congrFun', CharP.cast_eq_zero, zero_div, forall_prop_domain_congr, Subtype.mk.congr_simp, implies_true and 93 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 95 steps

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

  10. theorem Imo1990P4.PRat.mk_mul_mk line 159 source

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

    Statement uses: Rat, LT.lt, OfNat.ofNat, Eq, Subtype, HMul.hMul, Subtype.mk, Rat.mul_pos

    Proof uses: Subtype.coe_eq_of_eq_mk, rfl

    16 instances, coercions and auxiliary constants left out.

  11. theorem Imo1990P4.just_for_fun.f_one_eq_one line 167 source

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

    Statement uses: Imo1990P4.PRat, Eq, HMul.hMul, Rat, HDiv.hDiv, OfNat.ofNat

    Proof uses: Eq.symm, Eq.mp, congrArg, congr, one_mul, div_one, div_self'

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  12. theorem Imo1990P4.just_for_fun.f_mul_hom line 176 source

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

    Statement uses: Imo1990P4.PRat, Eq, HMul.hMul, Rat, HDiv.hDiv

    Proof uses: OfNat.ofNat, id, Eq.mpr, Inv.inv, congrArg, one_div, Eq.symm, propext, div_eq_one, Eq.mp, congr, Eq.trans, congrFun', inv_mul_cancel, Imo1990P4.just_for_fun.f_one_eq_one, of_eq_true, True, div_inv_eq_mul, eq_self

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  13. theorem Imo1990P4.just_for_fun.f_chain line 189 source

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

    Statement uses: Imo1990P4.PRat, Eq, HMul.hMul, Rat, HDiv.hDiv, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, one_mul, eq_self, Imo1990P4.just_for_fun.f_one_eq_one, Eq.refl

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. instance Imo1990P4.PRat.coePNat line 195 source

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

    Statement uses: Coe, PNat, Imo1990P4.PRat

    Proof uses: Coe.mk, Subtype.mk, Rat, LT.lt, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

  15. theorem Imo1990P4.Set.Infinite.exists_union_disjoint_infinite_of_infinite line 199 source

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

    Statement uses: Set, Set.Infinite, Exists, And, Eq, Union.union, Disjoint

    Proof uses: Cardinal, Cardinal.mk, Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite, Exists.intro, Eq.mpr, id, Eq.trans, True, congr, congrArg, congrFun', eq_self, eq_true, true_and, Infinite, Eq.symm, propext, Set.infinite_coe_iff, LE.le, Cardinal.aleph0 and 10 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  16. def Imo1990P4.PNat.mk_mul_hom_fun line 212 source

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

    Statement uses: CommMonoid, Nat, MulHom, PNat

    Proof uses: MulHom.mk, List.prod, List.map, Nat.primeFactorsList

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  17. theorem Imo1990P4.PNat.mk_mul_hom_fun.nonZero line 221 source

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

    Statement uses: CommMonoidWithZero, NoZeroDivisors, Nontrivial, Nat, Nat.Prime, Not, Eq, OfNat.ofNat, PNat, Ne, MulHom, Imo1990P4.PNat.mk_mul_hom_fun

    Proof uses: id, Eq.mpr, MulHom.mk, List.prod, List.map, Nat.primeFactorsList, Dvd.dvd, Eq.trans, And, Exists, congrArg, Membership.mem, List, funext, congrFun', True, False, not_false_eq_true, and_true, forall_congr

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  18. theorem Imo1990P4.PNat.mk_mul_hom_fun.prime line 231 source

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

    Statement uses: CommMonoid, Nat, Nat.Primes, Eq, MulHom, PNat, Imo1990P4.PNat.mk_mul_hom_fun, Nat.Prime

    Proof uses: id, Eq.mpr, MulHom.mk, List.prod, List.map, Nat.primeFactorsList, congrFun', congrArg, List, Imo1990P4.Nat.Primes.toPnat_val, List.cons, List.nil, Nat.primeFactorsList_prime, Subtype.prop, of_eq_true, Eq.trans, True, List.map_cons, List.map_nil, mul_one and 1 more

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  19. theorem Imo1990P4.PNat.mk_mul_hom_fun.one line 241 source

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

    Statement uses: CommMonoid, Nat, Eq, MulHom, PNat, Imo1990P4.PNat.mk_mul_hom_fun, OfNat.ofNat

    Proof uses: id, of_eq_true, MulHom.mk, List.prod, List.map, Nat.primeFactorsList, Eq.trans, True, congrFun', congrArg, List, List.nil, Nat.primeFactorsList_one, List.map_nil, eq_self

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  20. theorem Imo1990P4.PNat.mk_mul_hom_fun.cancel line 246 source

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

    Statement uses: CommMonoid, Nat, Nat.Prime, Eq, HMul.hMul, OfNat.ofNat, PNat, MulHom, Imo1990P4.PNat.mk_mul_hom_fun

    Proof uses: Eq.mpr, id, congrFun', congrArg, congr, map_mul, Trans.trans, mul_mul_mul_comm, MulHom.mk, List.prod, List.map, Nat.primeFactorsList, Eq.symm, List.prod_map_mul, List.prod_eq_one, Membership.mem, List, And, Dvd.dvd, Exists and 12 more

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  21. theorem Imo1990P4.PNat.mk_mul_hom_fun.inv line 261 source

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

    Statement uses: Nat, Imo1990P4.PRat, PNat, Eq, MulHom, Rat, Imo1990P4.PNat.mk_mul_hom_fun, Inv.inv

    Proof uses: Eq.mpr, List.prod, List.map, Nat.primeFactorsList, Function.comp, id, congrArg, Eq.trans, List.prod_inv, List, List.map_map, Eq.refl

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  22. theorem Imo1990P4.PNat.mk_mul_mk line 266 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Subtype, HMul.hMul, Subtype.mk, Nat.mul_pos

    Proof uses: Subtype.coe_eq_of_eq_mk, rfl

    16 instances, coercions and auxiliary constants left out.

  23. theorem Imo1990P4.Nat.toPNat_mul_toPNat line 269 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, PNat, HMul.hMul, Nat.toPNat, Nat.mul_pos

    Proof uses: rfl

    9 instances, coercions and auxiliary constants left out.

  24. theorem Imo1990P4.Nat.toPNat_coe line 273 source

    no axioms what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.toPNat

    Proof uses: rfl

    6 instances, coercions and auxiliary constants left out.

  25. theorem Imo1990P4.Nat.toPNat_one line 276 source

    standard axioms: propext what this means

    Statement uses: LT.lt, Nat, OfNat.ofNat, Eq, PNat, Nat.toPNat

    Proof uses: rfl

    6 instances, coercions and auxiliary constants left out.

  26. theorem Imo1990P4.Nat.Primes.val_toPNat line 279 source

    standard axioms: propext what this means

    Statement uses: Nat.Primes, LT.lt, Nat, OfNat.ofNat, Nat.Prime, Eq, PNat, Nat.toPNat

    Proof uses: rfl

    7 instances, coercions and auxiliary constants left out.

  27. def Imo1990P4.PRat.mk_mul_hom_fun line 281 source

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

    Statement uses: Nat, Imo1990P4.PRat, MonoidHom, Rat

    Proof uses: MonoidHom.mk, OneHom.mk, Subtype.mk, LT.lt, OfNat.ofNat, HMul.hMul, MulHom, PNat, Imo1990P4.PNat.mk_mul_hom_fun, Nat.toPNat, Int.toNat, Rat.num, Inv.inv, Rat.den

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  28. theorem Imo1990P4.PRat.mk_mul_hom_fun.prime line 307 source

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

    Statement uses: Nat, Imo1990P4.PRat, Nat.Primes, Eq, MonoidHom, Rat, Imo1990P4.PRat.mk_mul_hom_fun, Subtype.mk, LT.lt, OfNat.ofNat, Nat.Prime

    Proof uses: id, of_eq_true, MonoidHom.mk, OneHom.mk, HMul.hMul, MulHom, PNat, Imo1990P4.PNat.mk_mul_hom_fun, Nat.toPNat, Int.toNat, Rat.num, Inv.inv, Rat.den, Eq.trans, True, forall_congr, congrFun', congrArg, Subtype, congr and 7 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  29. theorem Imo1990P4.PRat.mk_mul_hom_fun.inv_prime line 312 source

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

    Statement uses: Nat, Imo1990P4.PRat, Nat.Primes, Eq, MonoidHom, Rat, Imo1990P4.PRat.mk_mul_hom_fun, Inv.inv, Subtype.mk, LT.lt, OfNat.ofNat, Nat.Prime

    Proof uses: id, Eq.mpr, MonoidHom.mk, OneHom.mk, HMul.hMul, MulHom, PNat, Imo1990P4.PNat.mk_mul_hom_fun, Nat.toPNat, Int.toNat, Rat.num, Rat.den, Int.sign, Int, congrArg, Eq.trans, Rat.num_inv, Nat.cast_one, mul_one, ite and 23 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  30. theorem Imo1990P4.exists_f line 330 source

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

    Statement uses: Exists, Imo1990P4.PRat, Eq, HMul.hMul, Rat, HDiv.hDiv

    Proof uses: Set, Nat, And, Union.union, Set.ofPred, Nat.Prime, Disjoint, Set.Infinite, Imo1990P4.Set.Infinite.exists_union_disjoint_infinite_of_infinite, Nat.infinite_setOfPred_prime, Equiv, Nonempty.some, Set.Infinite.to_subtype, Decidable, Classical.dec, dite, Membership.mem, Subtype.mk, LT.lt, OfNat.ofNat and 62 more

    127 instances, coercions and auxiliary constants left out.

    Tactic trace: 90 steps

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

  31. determine Imo1990P4.f line 428 source

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

    Statement uses: Imo1990P4.PRat

    Proof uses: Exists.choose, Eq, HMul.hMul, Rat, HDiv.hDiv, Imo1990P4.exists_f

    12 instances, coercions and auxiliary constants left out.

  32. problem Imo1990P4.imo1990_p4 line 430 source

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

    Statement uses: Imo1990P4.PRat, Eq, Imo1990P4.f, HMul.hMul, Rat, HDiv.hDiv

    Proof uses: Exists.choose_spec, Imo1990P4.exists_f

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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