Compfiles/Usa1976P3.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. determine Usa1976P3.solution_set line 28 source

   no axioms what this means

   Statement uses: Set, Prod, Int

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

   2 instances, coercions and auxiliary constants left out.

2. lemma Usa1976P3.sq_emod_four line 32 source

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

   Statement uses: Int, Or, Eq, HMod.hMod, HPow.hPow, Nat, OfNat.ofNat

   Proof uses: Even, Odd, Int.even_or_odd, HAdd.hAdd, Or.inl, Eq.symm, HMul.hMul, Or.inr

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 6 steps

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

3. lemma Usa1976P3.even_of_sum_sq_emod_four_eq_zero line 37 source

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

   Statement uses: Int, Eq, HMod.hMod, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, And, Even

   Proof uses: Odd, Or, Int.even_or_odd, Exists.intro, rfl, Eq.symm, HMul.hMul, Eq.mpr, id, congrFun', congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, 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 and 43 more

   60 instances, coercions and auxiliary constants left out.

   Tactic trace: 23 steps

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

4. lemma Usa1976P3.even_of_sum_sq_eq_sq_mul_sq line 55 source

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

   Statement uses: Int, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, And, Even

   Proof uses: HMod.hMod, Odd, Or, Int.even_or_odd, Exists.intro, rfl, Eq.symm, absurd, Eq.mp, congrArg, Eq.mpr, id, congrFun', Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 45 more

   59 instances, coercions and auxiliary constants left out.

   Tactic trace: 23 steps

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

5. lemma Usa1976P3.descent_step line 72 source

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

   Statement uses: Int, Nat, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul, Exists, And

   Proof uses: Even, Nat.casesAuxOn, Usa1976P3.even_of_sum_sq_eq_sq_mul_sq, Eq.mp, congrArg, congrFun', Eq.trans, pow_zero, one_mul, Eq.symm, Usa1976P3.even_of_sum_sq_emod_four_eq_zero, Eq.mpr, HMod.hMod, id, pow_succ, mul_assoc, Eq.refl, And.left, And.right

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 12 steps

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

6. lemma Usa1976P3.eq_zero_of_forall_two_pow_dvd line 90 source

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

   Statement uses: Int, Nat, Dvd.dvd, HPow.hPow, OfNat.ofNat, Eq

   Proof uses: Decidable.byContradiction, Not, LT.lt, Int.natAbs, Iff.mpr, Ne, Int.natAbs_pos, Nat.lt_pow_self, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Int.natAbs_dvd_natAbs, Eq.mp, congrArg, Int.natAbs_pow, LE.le, Nat.le_of_dvd and 61 more

   79 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

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

7. lemma Usa1976P3.eq_zero_of_solution_aux line 102 source

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

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

   Proof uses: Usa1976P3.eq_zero_of_forall_two_pow_dvd, Nat.recAux, Dvd.dvd, one_dvd, Exists, And, Usa1976P3.descent_step, Eq.mpr, id, congrArg, pow_succ', Int.mul_dvd_mul_left

   27 instances, coercions and auxiliary constants left out.

   Tactic trace: 12 steps

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

8. problem Usa1976P3.usa1976_p3 line 121 source

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

   Statement uses: Int, Iff, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Membership.mem, Prod, Set, Usa1976P3.solution_set, Prod.mk

   Proof uses: Iff.intro, Eq.mpr, Singleton.singleton, id, congrArg, Usa1976P3.solution_set.eq_1, propext, Set.mem_singleton_iff, And, Prod.mk.injEq, Usa1976P3.eq_zero_of_solution_aux, congrFun', Eq.trans, pow_zero, one_mul, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 89 more

   112 instances, coercions and auxiliary constants left out.

   Tactic trace: 19 steps

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