-- Mathlib/NumberTheory/LucasLehmer.lean
theorem lucas_lehmer_sufficiency (p : ℕ) (w : 1 < p) : LucasLehmerTest p → (mersenne p).Prime

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
contrapose

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)
h : 2 ^ (p' + 2) < mersenne (p' + 2)
⊢ False

Tactic:
exact not_lt_of_ge (Nat.sub_le _ _) h

Result:
no goals

Proof state:
p : ℕ
w : 1 < p
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
let p' := p - 2

Result:
p : ℕ
w : 1 < p
p' : ℕ := p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne p) → ¬LucasLehmerTest p

Tactic:
intro a t

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne p)
t : LucasLehmerTest p
⊢ False

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
⊢ False

Tactic:
have h₂ := Nat.minFac_sq_le_self (mersenne_pos.2 (Nat.lt_of_succ_lt w)) a

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)
⊢ False

Proof state:
p : ℕ
w : 1 < p
p' : ℕ := p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
have z : p = p' + 2 := (tsub_eq_iff_eq_add_of_le w.nat_succ_le).mp rfl

Result:
p : ℕ
w : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest p
⊢ False

Tactic:
rw [z] at t

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ False

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)
⊢ False

Tactic:
have h := lt_of_lt_of_le h₁ h₂

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
h₂ : (mersenne (p' + 2)).minFac ^ 2 ≤ mersenne (p' + 2)
h : 2 ^ (p' + 2) < mersenne (p' + 2)
⊢ False

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne p)
t : LucasLehmerTest p
⊢ False

Tactic:
rw [z] at a

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest p
⊢ False

Proof state:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ False

Tactic:
have h₁ := order_ineq p' t

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : 2 ^ (p' + 2) < ↑(q (p' + 2)) ^ 2
⊢ False

Proof state:
p : ℕ
w : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl

Result:
p : ℕ
w✝ : 1 < p
p' : ℕ := p - 2
z : p = p' + 2
w : 1 < p' + 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)