Compfiles/Imo1997P5.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Imo1997P5.ineq₁ line 34 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HPow.hPow, HSub.hSub

   Proof uses: Nat.le_induction, Eq.mpr, id, Eq, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natSub, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 77 more

   111 instances, coercions and auxiliary constants left out.

   Tactic trace: 6 steps

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

2. lemma Imo1997P5.ineq₂ line 39 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, HPow.hPow

   Proof uses: Eq.mpr, HAdd.hAdd, HSub.hSub, id, Eq, congrArg, Nat.pow_add, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 66 more

   111 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

3. lemma Imo1997P5.ineq₃ line 44 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HPow.hPow

   Proof uses: Nat.le_induction, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 79 more

   110 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

4. lemma Imo1997P5.ineq₄ line 47 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, HPow.hPow

   Proof uses: Nat.recAux, of_eq_true, Eq.trans, Eq, True, congr, congrArg, MulZeroClass.mul_zero, congrFun', pow_zero, one_pow, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 33 more

   55 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

5. lemma Imo1997P5.aux₁ line 52 source

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

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

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

6. lemma Imo1997P5.aux₂ line 54 source

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

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

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

7. lemma Imo1997P5.aux₃ line 56 source

   standard axioms: Quot.sound, propext what this means

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

   Proof uses: Iff.mp, Nat.pow_dvd_pow_iff, Dvd.intro, Eq.symm

   19 instances, coercions and auxiliary constants left out.

8. determine Imo1997P5.solution_set line 61 source

   no axioms what this means

   Statement uses: Set, Prod, Nat

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

   3 instances, coercions and auxiliary constants left out.

9. problem Imo1997P5.imo1997_p5 line 63 source

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

   Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Eq, HPow.hPow, Membership.mem, Prod, Set, Imo1997P5.solution_set, Prod.mk

   Proof uses: Eq.mpr, Or, And, id, congrArg, Eq.trans, Insert.insert, Singleton.singleton, congr, Prod.mk.injEq, Iff.intro, dite, LE.le, HMul.hMul, HSub.hSub, Eq.symm, pow_mul, HAdd.hAdd, pow_add, HPow and 108 more

   159 instances, coercions and auxiliary constants left out.

   Tactic trace: 56 steps

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