MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

GitHub source file

27 declarations, 9 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. theorem C05S03.two_le line 8 source

    standard axioms: propext what this means

    Statement uses: Nat, Ne, OfNat.ofNat, LE.le

    Proof uses: Nat.casesAuxOn, Eq, absurd, Eq.refl, Eq.symm, HAdd.hAdd, Nat.succ_le_succ, zero_le

    11 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:8 (same declaration text).

    Tactic trace: 17 steps

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

  2. example C05S03.(example at line 15) line 15 source
  3. example C05S03.(example at line 20) line 20 source
  4. theorem C05S03.exists_prime_factor line 27 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, Nat.Prime, Dvd.dvd

    Proof uses: dite, Exists.intro, And.intro, dvd_refl, Not, Nat.strong_induction_on, LT.lt, Ne, Eq.mp, Eq, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, propext, Nat.prime_def_lt, False.elim and 62 more

    85 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:15 (same declaration text).

    Tactic trace: 19 steps

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

  5. theorem C05S03.primes_infinite sorry line 45 source

    depends on sorry what this means

    Statement uses: Nat, Exists, And, GT.gt, Nat.Prime

    Proof uses: LE.le, OfNat.ofNat, HAdd.hAdd, Nat.factorial, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Dvd.dvd, C05S03.exists_prime_factor, Exists.intro, And.intro, id, Decidable.byContradiction, Not, False

    10 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:33 (same statement text; different proof or body). Qualify references as C05S03.primes_infinite@path.

    Tactic trace: 29 steps

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

  6. example C05S03.(example at line 65) line 65 source
  7. example C05S03.(example at line 71) line 71 source
  8. example C05S03.(example at line 76) line 76 source
  9. example C05S03.(example at line 81) line 81 source
  10. example C05S03.(example at line 91) sorry line 91 source
  11. example C05S03.(example at line 93) sorry line 93 source
  12. example C05S03.(example at line 98) line 98 source
  13. theorem C05S03._root_.Nat.Prime.eq_of_dvd_of_prime sorry line 101 source

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:81 (same statement text; different proof or body). Qualify references as C05S03._root_.Nat.Prime.eq_of_dvd_of_prime@path.

  14. theorem C05S03.mem_of_dvd_prod_primes sorry line 106 source

    depends on sorry what this means

    Statement uses: Finset, Nat, Nat.Prime, Membership.mem, Dvd.dvd, Finset.prod

    Proof uses: Finset.induction_on, EmptyCollection.emptyCollection, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, OfNat.ofNat, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow and 53 more

    74 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:88 (same statement text; different proof or body). Qualify references as C05S03.mem_of_dvd_prod_primes@path.

    Tactic trace: 8 steps

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

  15. example C05S03.(example at line 115) line 115 source
  16. theorem C05S03.primes_infinite' sorry line 118 source

    depends on sorry what this means

    Statement uses: Finset, Nat, Exists, And, Nat.Prime, Not, Membership.mem

    Proof uses: Classical.byContradiction, Finset.filter, Eq, rfl, Iff, Eq.mpr, id, Eq.trans, congrFun', congrArg, Eq.mp, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, LE.le, OfNat.ofNat, HAdd.hAdd, Finset.prod and 20 more

    37 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:102 (same statement text; different proof or body). Qualify references as C05S03.primes_infinite'@path.

    Tactic trace: 18 steps

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

  17. theorem C05S03.bounded_of_ex_finset line 137 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Exists, Finset, Membership.mem, LT.lt

    Proof uses: Exists.intro, HAdd.hAdd, Finset.sup, id, OfNat.ofNat, Nat.lt_succ_of_le, LE.le, Finset.le_sup

    14 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:129 (same declaration text).

    Tactic trace: 6 steps

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

  18. theorem C05S03.ex_finset_of_bounded line 146 source

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

    Statement uses: Nat, DecidablePred, Exists, LE.le, Finset, Iff, Membership.mem

    Proof uses: Exists.intro, Finset.filter, Finset.range, HAdd.hAdd, OfNat.ofNat, Eq.mpr, id, Eq, Eq.trans, And, congrArg, congrFun', LT.lt

    25 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:138 (same declaration text).

    Tactic trace: 6 steps

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

  19. example C05S03.(example at line 153) line 153 source
  20. example C05S03.(example at line 155) line 155 source
  21. theorem C05S03.mod_4_eq_3_or_mod_4_eq_3 line 158 source

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

    Statement uses: Nat, Eq, HMod.hMod, HMul.hMul, OfNat.ofNat, Or

    Proof uses: Eq.mpr, id, congrArg, Nat.mul_mod, LT.lt, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, dite, LE.le, of_eq_true, Eq.trans, True, implies_congr, congrFun', eq_self, true_or and 19 more

    45 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:145 (same declaration text).

    Tactic trace: 10 steps

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

  22. theorem C05S03.two_le_of_mod_4_eq_3 line 166 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, LE.le

    Proof uses: C05S03.two_le, False.elim, False, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, congrArg

    9 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:153 (same declaration text).

    Tactic trace: 5 steps

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

  23. theorem C05S03.aux sorry line 172 source

    depends on sorry what this means

    Statement uses: Nat, Dvd.dvd, LE.le, OfNat.ofNat, LT.lt, And, HDiv.hDiv

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    12 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:159 (same statement text; different proof or body). Qualify references as C05S03.aux@path.

    Tactic trace: 1 steps

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

  24. theorem C05S03.exists_prime_factor_mod_4_eq_3 sorry line 174 source

    depends on sorry what this means

    Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, Exists, And, Nat.Prime, Dvd.dvd

    Proof uses: dite, Exists.intro, And.intro, dvd_refl, Not, Nat.strong_induction_on, LT.lt, Ne, Eq.mp, LE.le, Eq.trans, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, propext, Nat.prime_def_lt, C05S03.two_le_of_mod_4_eq_3 and 66 more

    87 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:164 (same statement text; different proof or body). Qualify references as C05S03.exists_prime_factor_mod_4_eq_3@path.

    Tactic trace: 24 steps

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

  25. example C05S03.(example at line 194) line 194 source
  26. example C05S03.(example at line 197) line 197 source
  27. theorem C05S03.primes_mod_4_eq_3_infinite sorry line 201 source

    depends on sorry what this means

    Statement uses: Nat, Exists, And, GT.gt, Nat.Prime, Eq, HMod.hMod, OfNat.ofNat

    Proof uses: Classical.byContradiction, Not, Ne, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Finset, Iff, Membership.mem, C05S03.ex_finset_of_bounded, Exists.intro, LE.le and 18 more

    30 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:194 (same statement text; different proof or body). Qualify references as C05S03.primes_mod_4_eq_3_infinite@path.

    Tactic trace: 24 steps

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