MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  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/S03_Infinitely_Many_Primes.lean:8 (same declaration text).

    Tactic trace: 8 steps

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

  2. theorem C05S03.exists_prime_factor line 15 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/S03_Infinitely_Many_Primes.lean:27 (same declaration text).

    Tactic trace: 19 steps

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

  3. theorem C05S03.primes_infinite line 33 source

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

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

    Proof uses: LE.le, OfNat.ofNat, HAdd.hAdd, Nat.factorial, Nat.succ_le_succ, Nat.succ_le_of_lt, Nat.factorial_pos, Dvd.dvd, C05S03.exists_prime_factor, Exists.intro, And.intro, id, Decidable.byContradiction, Not, Nat.dvd_factorial, Nat.Prime.pos, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int and 65 more

    95 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 31 steps

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

  4. example C05S03.(example at line 59) line 59 source
  5. example C05S03.(example at line 64) line 64 source
  6. example C05S03.(example at line 69) line 69 source
  7. example C05S03.(example at line 74) line 74 source
  8. theorem C05S03._root_.Nat.Prime.eq_of_dvd_of_prime line 81 source

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

  9. theorem C05S03.mem_of_dvd_prod_primes line 88 source

    standard axioms: Classical.choice, Quot.sound, propext 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 58 more

    82 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 13 steps

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

  10. theorem C05S03.primes_infinite' line 102 source

    standard axioms: Classical.choice, Quot.sound, propext 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 68 more

    100 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 25 steps

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

  11. theorem C05S03.bounded_of_ex_finset line 129 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/S03_Infinitely_Many_Primes.lean:137 (same declaration text).

    Tactic trace: 6 steps

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

  12. theorem C05S03.ex_finset_of_bounded line 138 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/S03_Infinitely_Many_Primes.lean:146 (same declaration text).

    Tactic trace: 4 steps

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

  13. theorem C05S03.mod_4_eq_3_or_mod_4_eq_3 line 145 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/S03_Infinitely_Many_Primes.lean:158 (same declaration text).

    Tactic trace: 10 steps

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

  14. theorem C05S03.two_le_of_mod_4_eq_3 line 153 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/S03_Infinitely_Many_Primes.lean:166 (same declaration text).

    Tactic trace: 5 steps

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

  15. theorem C05S03.aux line 159 source

    standard axioms: propext what this means

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

    Proof uses: And.intro, Nat.div_dvd_of_dvd, Nat.div_lt_self, lt_of_le_of_lt, zero_le

    18 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 4 steps

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

  16. theorem C05S03.exists_prime_factor_mod_4_eq_3 line 164 source

    standard axioms: Classical.choice, Quot.sound, propext 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 62 more

    88 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 31 steps

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

  17. theorem C05S03.primes_mod_4_eq_3_infinite line 194 source

    standard axioms: Classical.choice, Quot.sound, propext 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 44 more

    57 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 39 steps

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