Compfiles/Imo1992P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1992, Problem 1

Find all integers 1 < a < b < c such that (a - 1)(b - 1)(c - 1) divides abc - 1.

Imports (2)
Imported by 1 file
  1. determine Imo1992P1.solution_set line 30 source

    no axioms what this means

    Statement uses: Set, Prod, Int

    Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton

    3 instances, coercions and auxiliary constants left out.

  2. problem Imo1992P1.imo1992_p1 line 32 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Iff, Membership.mem, Prod, Set, Imo1992P1.solution_set, Prod.mk, Dvd.dvd, HMul.hMul, HSub.hSub

    Proof uses: Iff.intro, And, Eq, Or, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congr, congrArg, Prod.mk.injEq, Mathlib.Meta.NormNum.isInt_dvd_true, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Mathlib.Meta.NormNum.isNat_ofNat, Nat and 88 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 119 steps

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