-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sModNat_eq_sMod (p k : ℕ) (hp : 2 ≤ p) : (sModNat (2 ^ p - 1) k : ℤ) = sMod p k

Proof state:
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) 0) = sMod p 0

Tactic:
rw [sModNat, sMod, Int.ofNat_emod]

Result:
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑4 % ↑(2 ^ p - 1) = 4 % (2 ^ p - 1)

Proof state:
p k : ℕ
hp : 2 ≤ p
⊢ ↑(sModNat (2 ^ p - 1) k) = sMod p k

Tactic:
have h1 := calc
  4 = 2 ^ 2 := by norm_num
  _ ≤ 2 ^ p := Nat.pow_le_pow_of_le_right (by norm_num) hp

Result:
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) k) = sMod p k

Proof state:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ (↑(sModNat (2 ^ p - 1) k) ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Tactic:
rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc,
  Int.add_emod_self, ← sub_eq_add_neg]

Result:
no goals

Proof state:
p : ℕ
hp : 2 ≤ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h1 : 4 ≤ 2 ^ p
⊢ 4 - 1 ≤ 2 ^ p - 1

Tactic:
exact Int.sub_le_sub_right h1 _

Result:
no goals

Proof state:
case zero
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑4 % ↑(2 ^ p - 1) = 4 % (2 ^ p - 1)

Tactic:
simp [h2]

Result:
no goals

Proof state:
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) k) = sMod p k

Tactic:
induction k with
| zero =>
  rw [sModNat, sMod, Int.ofNat_emod]
  simp [h2]
| succ k ih =>
  rw [sModNat, sMod, ← ih]
  have h3 : 2 ≤ 2 ^ p - 1 := by
    zify [h2]
    calc
      (2 : Int) ≤ 4 - 1 := by norm_num
      _         ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _
  zify [h2, h3]
  rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc,
    Int.add_emod_self, ← sub_eq_add_neg]

Result:
no goals

Proof state:
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ 2 ≤ 4 - 1

Tactic:
norm_num

Result:
no goals

Proof state:
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
⊢ 1 ≤ 2 ^ p

Tactic:
omega

Result:
no goals

Proof state:
p k : ℕ
hp : 2 ≤ p
⊢ 2 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ ↑((sModNat (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Tactic:
zify [h2, h3]

Result:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ (↑(sModNat (2 ^ p - 1) k) ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Proof state:
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ 4 - 1 ≤ 2 ^ p - 1

Tactic:
zify at h1

Result:
p : ℕ
hp : 2 ≤ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h1 : 4 ≤ 2 ^ p
⊢ 4 - 1 ≤ 2 ^ p - 1

Proof state:
p k : ℕ
hp : 2 ≤ p
⊢ 4 = 2 ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ ↑(sModNat (2 ^ p - 1) (k + 1)) = sMod p (k + 1)

Tactic:
rw [sModNat, sMod, ← ih]

Result:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ ↑((sModNat (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Proof state:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ ↑((sModNat (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Tactic:
have h3 : 2 ≤ 2 ^ p - 1 := by
  zify [h2]
  calc
    (2 : Int) ≤ 4 - 1 := by norm_num
    _         ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _

Result:
case succ
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
h3 : 2 ≤ 2 ^ p - 1
⊢ ↑((sModNat (2 ^ p - 1) k ^ 2 + (2 ^ p - 1 - 2)) % (2 ^ p - 1)) = (↑(sModNat (2 ^ p - 1) k) ^ 2 - 2) % (2 ^ p - 1)

Proof state:
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) k) = sMod p k

Tactic:
have h2 : 1 ≤ 2 ^ p := by omega

Result:
p k : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) k) = sMod p k

Proof state:
p : ℕ
hp : 2 ≤ p
h1 : 4 ≤ 2 ^ p
h2 : 1 ≤ 2 ^ p
k : ℕ
ih : ↑(sModNat (2 ^ p - 1) k) = sMod p k
⊢ 2 ≤ 2 ^ p - 1

Tactic:
calc
  (2 : Int) ≤ 4 - 1 := by norm_num
  _         ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _

Result:
no goals