Theorem: infinity_of_primes₃ (FormalBook/Chapter_01.lean)

State before:
⊢ ¬∃ p, p.Prime ∧ ∀ (q : ℕ), q.Prime → q ≤ p
Tactic:
simp only [not_exists, not_and, not_forall, not_le, exists_prop]
State after:
⊢ ∀ (x : ℕ), x.Prime → ∃ x_1, x_1.Prime ∧ x < x_1

State before:
⊢ ∀ (x : ℕ), x.Prime → ∃ x_1, x_1.Prime ∧ x < x_1
Tactic:
intros p hp
State after:
p : ℕ
hp : p.Prime
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have : Fact (Nat.Prime p) := by exact { out := hp }
State after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
let m := mersenne p
State after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
let q := m.minFac
State after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have hq : q.Prime := minFac_prime <| Nat.ne_of_gt <| one_lt_mersenne.mpr <| Prime.one_lt hp
State after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have : Fact (Nat.Prime q) := by exact { out := hq }
State after:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have h_mod_q : 2 ^ p  ≡ 1 [MOD q] := by
  have : (2^p - 1) % q = 0 :=  mod_eq_zero_of_dvd (minFac_dvd m)
  change (2^p - 1) ≡ 0 [MOD q] at this
  rw [modEq_iff_dvd, dvd_iff_exists_eq_mul_left] at *
  obtain ⟨c, hc⟩ := this
  use c
  simp only [CharP.cast_eq_zero, ge_iff_le, gt_iff_lt, pow_pos, cast_pred, cast_pow, cast_ofNat,
      zero_sub, neg_sub] at hc
  simp [cast_one, cast_pow, cast_ofNat, hc.symm]
State after:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have h_mod_q' : (2 : (ZMod q)) ^ p = 1 := by
  have := (ZMod.natCast_eq_natCast_iff _ _ _).mpr h_mod_q
  norm_cast at this
  rw [← this, cast_pow, cast_ofNat]
State after:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have : (2 : (ZMod q)) * (2 ^ (p - 1)) = 1 := by
  convert h_mod_q'
  nth_rw 1 [← pow_one 2]
  rw [← pow_add 2 1 (p - 1)]
  congr
  exact add_sub_of_le <| Prime.pos hp
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
let two := Units.mkOfMulEqOne (2 : (ZMod q)) (2 ^ (p - 1)) this
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have two_desc : ↑two = (2 : (ZMod q)) := by
  convert Units.val_mkOfMulEqOne this
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have h_two : two ^ p = 1 := by
  ext
  push_cast
  rw [two_desc]
  exact h_mod_q'
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have two_ne_one : two ≠ 1 := by
  by_contra h
  rw [Units.ext_iff] at h
  push_cast at h
  rw [two_desc] at h
  exact (ZMod.two_ne_one q) h
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ ∃ x, x.Prime ∧ p < x

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
use q
State after:
case h
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ q.Prime ∧ p < q

State before:
case h
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ q.Prime ∧ p < q
Tactic:
constructor
State after:
case h.left
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ q.Prime

case h.right
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ p < q

State before:
p : ℕ
hp : p.Prime
⊢ Fact p.Prime
Tactic:
exact { out := hp }
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
⊢ Fact q.Prime
Tactic:
exact { out := hq }
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
⊢ q.ModEq (2 ^ p) 1
Tactic:
have : (2^p - 1) % q = 0 :=  mod_eq_zero_of_dvd (minFac_dvd m)
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : (2 ^ p - 1) % q = 0
⊢ q.ModEq (2 ^ p) 1

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : (2 ^ p - 1) % q = 0
⊢ q.ModEq (2 ^ p) 1
Tactic:
change (2^p - 1) ≡ 0 [MOD q] at this
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : q.ModEq (2 ^ p - 1) 0
⊢ q.ModEq (2 ^ p) 1

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : q.ModEq (2 ^ p - 1) 0
⊢ q.ModEq (2 ^ p) 1
Tactic:
rw [modEq_iff_dvd, dvd_iff_exists_eq_mul_left] at *
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : ∃ c, ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ∃ c, ↑1 - ↑(2 ^ p) = c * ↑q

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
this : ∃ c, ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ∃ c, ↑1 - ↑(2 ^ p) = c * ↑q
Tactic:
obtain ⟨c, hc⟩ := this
State after:
case intro
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ∃ c, ↑1 - ↑(2 ^ p) = c * ↑q

State before:
case intro
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ∃ c, ↑1 - ↑(2 ^ p) = c * ↑q
Tactic:
use c
State after:
case h
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q

State before:
case h
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : ↑0 - ↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q
Tactic:
simp only [CharP.cast_eq_zero, ge_iff_le, gt_iff_lt, pow_pos, cast_pred, cast_pow, cast_ofNat,
    zero_sub, neg_sub] at hc
State after:
case h
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : -↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q

State before:
case h
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
c : ℤ
hc : -↑(2 ^ p - 1) = c * ↑q
⊢ ↑1 - ↑(2 ^ p) = c * ↑q
Tactic:
simp [cast_one, cast_pow, cast_ofNat, hc.symm]
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
⊢ 2 ^ p = 1
Tactic:
have := (ZMod.natCast_eq_natCast_iff _ _ _).mpr h_mod_q
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
this : ↑(2 ^ p) = ↑1
⊢ 2 ^ p = 1

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
this : ↑(2 ^ p) = ↑1
⊢ 2 ^ p = 1
Tactic:
norm_cast at this
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
this : ↑(2 ^ p) = 1
⊢ 2 ^ p = 1

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
this : ↑(2 ^ p) = 1
⊢ 2 ^ p = 1
Tactic:
rw [← this, cast_pow, cast_ofNat]
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 * 2 ^ (p - 1) = 1
Tactic:
convert h_mod_q'
State after:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 * 2 ^ (p - 1) = 2 ^ p

State before:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 * 2 ^ (p - 1) = 2 ^ p
Tactic:
nth_rw 1 [← pow_one 2]
State after:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 ^ 1 * 2 ^ (p - 1) = 2 ^ p

State before:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 ^ 1 * 2 ^ (p - 1) = 2 ^ p
Tactic:
rw [← pow_add 2 1 (p - 1)]
State after:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 ^ (1 + (p - 1)) = 2 ^ p

State before:
case h.e'_2
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 2 ^ (1 + (p - 1)) = 2 ^ p
Tactic:
congr
State after:
case h.e'_2.e_a
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 1 + (p - 1) = p

State before:
case h.e'_2.e_a
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ 1 + (p - 1) = p
Tactic:
exact add_sub_of_le <| Prime.pos hp
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
⊢ ↑two = 2
Tactic:
convert Units.val_mkOfMulEqOne this
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ two ^ p = 1
Tactic:
ext
State after:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ↑(two ^ p) = ↑1

State before:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ↑(two ^ p) = ↑1
Tactic:
push_cast
State after:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ↑two ^ p = 1

State before:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ ↑two ^ p = 1
Tactic:
rw [two_desc]
State after:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ 2 ^ p = 1

State before:
case a
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
⊢ 2 ^ p = 1
Tactic:
exact h_mod_q'
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
⊢ two ≠ 1
Tactic:
by_contra h
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : two = 1
⊢ False

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : two = 1
⊢ False
Tactic:
rw [Units.ext_iff] at h
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : ↑two = ↑1
⊢ False

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : ↑two = ↑1
⊢ False
Tactic:
push_cast at h
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : ↑two = 1
⊢ False

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : ↑two = 1
⊢ False
Tactic:
rw [two_desc] at h
State after:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : 2 = 1
⊢ False

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : 2 = 1
⊢ False
Tactic:
exact (ZMod.two_ne_one q) h
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ p ∣ q - 1
Tactic:
convert Subgroup.card_subgroup_dvd_card (Subgroup.zpowers (two))
State after:
case h.e'_3
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ p = Fintype.card ↥(Subgroup.zpowers two)

case h.e'_4
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ q - 1 = Fintype.card (ZMod q)ˣ

State before:
case h.e'_3
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ p = Fintype.card ↥(Subgroup.zpowers two)
Tactic:
rw [← orderOf_eq_prime h_two two_ne_one]
State after:
case h.e'_3
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ orderOf two = Fintype.card ↥(Subgroup.zpowers two)

State before:
case h.e'_3
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ orderOf two = Fintype.card ↥(Subgroup.zpowers two)
Tactic:
exact Fintype.card_zpowers.symm
State after:
no goals

State before:
case h.e'_4
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
⊢ q - 1 = Fintype.card (ZMod q)ˣ
Tactic:
exact ((prime_iff_card_units q).mp hq).symm
State after:
no goals

State before:
case h.left
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ q.Prime
Tactic:
refine' minFac_prime <| Nat.ne_of_gt _
State after:
case h.left
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ 1 < m

State before:
case h.left
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ 1 < m
Tactic:
calc 1 < 2^2 - 1 := by norm_num
    _  ≤ 2^p - 1 := sub_one_le_sub_one <| pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ 1 < 2 ^ 2 - 1
Tactic:
norm_num
State after:
no goals

State before:
case h.right
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ p < q
Tactic:
have h2q : 2 ≤ q := by
  exact Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
      Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1
State after:
case h.right
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
h2q : 2 ≤ q
⊢ p < q

State before:
case h.right
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
h2q : 2 ≤ q
⊢ p < q
Tactic:
exact lt_of_le_of_lt (Nat.le_of_dvd  (Nat.sub_pos_of_lt <| h2q) h_piv_div_q_sub_one)
    <| pred_lt <| Nat.ne_of_gt <| Nat.le_of_lt h2q
State after:
no goals

State before:
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ 2 ≤ q
Tactic:
exact Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
    Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1
State after:
no goals