Compfiles/Usa2017P1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2017, Problem 1

Prove that there are infinitely many distinct pairs $(a,b)$ of relatively prime positive integers $a>1$ and $b>1$ such that $a^b+b^a$ is divisible by $a+b$.

Imports (7)
Imported by 1 file
  1. def Usa2017P1.condition line 32 source

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: And, Eq, Nat.gcd, OfNat.ofNat, GT.gt, Dvd.dvd, HAdd.hAdd, HPow.hPow

    9 instances, coercions and auxiliary constants left out.

  2. def Usa2017P1.solution_set line 37 source

    standard axioms: propext what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Set.ofPred, Usa2017P1.condition, Prod.fst, Prod.snd

  3. lemma Usa2017P1.divisibility_helper line 39 source

    standard axioms: propext what this means

    Statement uses: Nat, Or, Eq, OfNat.ofNat, Nat.ModEq, HAdd.hAdd, HMul.hMul, HPow.hPow

    Proof uses: Or.inl, Eq.mpr, id, congrArg, congrFun', congr, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, 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_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 31 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  4. lemma Usa2017P1.build_condition_divisibility line 55 source

    standard axioms: propext what this means

    Statement uses: Nat, Dvd.dvd, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow

    Proof uses: Iff.mp, Nat.ModEq, Nat.modEq_zero_iff_dvd, Eq, of_eq_true, Eq.trans, True, congr, congrArg, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm and 40 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  5. lemma Usa2017P1.build_condition line 101 source

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

    Statement uses: Nat, Usa2017P1.condition, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    Proof uses: Eq, rfl, Nat.gcd, Iff.mp, Nat.Coprime, Nat.coprime_iff_gcd_eq_one, Eq.mpr, id, congrArg, add_comm, Iff.mpr, Nat.coprime_add_self_right, Odd, Nat.coprime_two_right, Exists.intro, Nat.Simproc.add_eq_add_ge, of_decide_eq_true, LE.le, Eq.refl, Bool and 15 more

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  6. def Usa2017P1.build line 117 source

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

    Statement uses: Nat, Prod, Usa2017P1.solution_set

    Proof uses: Subtype.mk, Membership.mem, Set, Prod.mk, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2017P1.build_condition

    7 instances, coercions and auxiliary constants left out.

  7. problem Usa2017P1.usa2016_p1 line 122 source

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

    Statement uses: Infinite, Prod, Nat, Set.ofPred, Usa2017P1.usa2016_p1.match_1, Usa2017P1.condition

    Proof uses: Infinite.of_injective, Usa2017P1.build, Eq

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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