internlm/Lean-Github huggingface dataset:
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ m ∣ 2
Tactic:
have h_m_prod : m ∣ (∏ k in range n, F k) :=
  dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ m ∣ 2
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ m ∣ 2
Tactic:
have h_prod : (∏ k in range n, F k) + 2 = F n := by
  rw [fermat_product, Nat.sub_add_cancel]
  refine' le_of_lt _
  simp [fermat_bounded]
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ 2
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ 2
Tactic:
refine' (Nat.dvd_add_right h_m_prod).mp _
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ ∏ k ∈ range n, F k + 2
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ ∏ k ∈ range n, F k + 2
Tactic:
rw [h_prod]
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ F n
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ F n
Tactic:
exact h_n
Proof state after:
no goals
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ ∏ k ∈ range n, F k + 2 = F n
Tactic:
rw [fermat_product, Nat.sub_add_cancel]
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 ≤ F n
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 ≤ F n
Tactic:
refine' le_of_lt _
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 < F n
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 < F n
Tactic:
simp [fermat_bounded]
Proof state after:
no goals
Theorem: infinity_of_primes₂
Proof state before:
case inl
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_one : m = 1
⊢ (F n).Coprime (F k)
Tactic:
exact h_one
Proof state after:
no goals
Theorem: infinity_of_primes₂
Proof state before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
⊢ (F n).Coprime (F k)
Tactic:
by_contra
Proof state after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Theorem: infinity_of_primes₂
Proof state before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Tactic:
rw [h_two] at h_n
Proof state after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Theorem: infinity_of_primes₂
Proof state before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Tactic:
have h_even : Even (F n) := even_iff_two_dvd.mpr h_n
Proof state after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
⊢ False
Theorem: infinity_of_primes₂
Proof state before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
⊢ False
Tactic:
have h_odd : Odd (F n) := fermat_odd
Proof state after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
h_odd : Odd (F n)
⊢ False
Theorem: infinity_of_primes₂
Proof state before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
h_odd : Odd (F n)
⊢ False
Tactic:
exact (odd_iff_not_even.mp h_odd) h_even
Proof state after:
no goals
Theorem: ZMod.one_ne_zero
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
⊢ 1 ≠ 0
Tactic:
intro h
Proof state after:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
⊢ False
Theorem: ZMod.one_ne_zero
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
⊢ False
Tactic:
have := ZMod.val_one q ▸ (ZMod.val_eq_zero (1 : ZMod q)).mpr h
Proof state after:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
this : 1 = 0
⊢ False
Theorem: ZMod.one_ne_zero
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
h : 1 = 0
this : 1 = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: ZMod.two_ne_one
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
⊢ 2 ≠ 1
Tactic:
intro h1
Proof state after:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ False
Theorem: ZMod.two_ne_one
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ False
Tactic:
have h : (2 - 1 : ZMod q) = 0 := by exact Iff.mpr sub_eq_zero h1
Proof state after:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
h : 2 - 1 = 0
⊢ False
Theorem: ZMod.two_ne_one
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
h : 2 - 1 = 0
⊢ False
Tactic:
norm_num at h
Proof state after:
no goals
Theorem: ZMod.two_ne_one
Proof state before:
q : ℕ
inst✝ : Fact (1 < q)
h1 : 2 = 1
⊢ 2 - 1 = 0
Tactic:
exact Iff.mpr sub_eq_zero h1
Proof state after:
no goals
Theorem: sub_one_le_sub_one
Proof state before:
n m : ℕ
⊢ n ≤ m → n - 1 ≤ m - 1
Tactic:
exact fun h => pred_le_pred h
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof state before:
⊢ ¬∃ p, p.Prime ∧ ∀ (q : ℕ), q.Prime → q ≤ p
Tactic:
simp only [not_exists, not_and, not_forall, not_le, exists_prop]
Proof state after:
⊢ ∀ (x : ℕ), x.Prime → ∃ x_1, x_1.Prime ∧ x < x_1
Theorem: infinity_of_primes₃
Proof state before:
⊢ ∀ (x : ℕ), x.Prime → ∃ x_1, x_1.Prime ∧ x < x_1
Tactic:
intros p hp
Proof state after:
p : ℕ
hp : p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Theorem: infinity_of_primes₃
Proof state before:
p : ℕ
hp : p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
have : Fact (Nat.Prime p) := by exact { out := hp }
Proof state after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Theorem: infinity_of_primes₃
Proof state before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
let m := mersenne p
Proof state after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
⊢ ∃ x, x.Prime ∧ p < x
Theorem: infinity_of_primes₃
Proof state before:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
⊢ ∃ x, x.Prime ∧ p < x
Tactic:
let q := m.minFac
Proof state after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
⊢ ∃ x, x.Prime ∧ p < x
Theorem: infinity_of_primes₃
Proof 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
Proof state after:
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
⊢ ∃ x, x.Prime ∧ p < x
Theorem: infinity_of_primes₃
Proof 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 }
Proof 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
Theorem: infinity_of_primes₃
Proof 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]
Proof 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
Theorem: infinity_of_primes₃
Proof 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]
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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'
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof state before:
p : ℕ
hp : p.Prime
⊢ Fact p.Prime
Tactic:
exact { out := hp }
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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 }
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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)
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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 *
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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]
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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]
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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'
Proof 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
Theorem: infinity_of_primes₃
Proof 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]
Proof 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
Theorem: infinity_of_primes₃
Proof 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)]
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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
Proof state after:
no goals
Theorem: infinity_of_primes₃
Proof 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
Proof 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
Theorem: infinity_of_primes₃
Proof 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
Proof 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