-- Mathlib/NumberTheory/Fermat.lean
lemma fermat_primeFactors_one_lt (n p : ℕ) (hn : 1 < n) (hp : p.Prime)
    (hpdvd : p ∣ fermatNumber n) :
    ∃ k, p = k * 2 ^ (n + 2) + 1

Proof state:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
suffices h : p ∣ a.val ^ (2 ^ (n + 1)) + 1 by
  exact pow_pow_add_primeFactors_one_lt hp hp2 h

Result:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Proof state:
case intro
n : ℕ
hn : 1 < n
k : ℕ
hp : Prime (k * 2 ^ (n + 1) + 1)
hpdvd : k * 2 ^ (n + 1) + 1 ∣ n.fermatNumber
this : Fact (Prime (k * 2 ^ (n + 1) + 1))
hp2 : k * 2 ^ (n + 1) + 1 ≠ 2
⊢ (k * 2 ^ (n + 1) + 1) % 8 = 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn

Result:
case intro.intro
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ (n + succ 1 + 1) + 1) % 8 = 1

Proof state:
case intro.intro
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n % 8 * (2 ^ (succ 1 + 1) % 8) % 8 + 1) % 8 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
have hp8 : p % 8 = 1 := by
  obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
  rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]
  norm_num

Result:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
h : p ∣ a.val ^ 2 ^ (n + 1) + 1
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
exact pow_pow_add_primeFactors_one_lt hp hp2 h

Result:
no goals

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ p ≠ 2

Tactic:
exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd

Result:
no goals

Proof state:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ↑a.val ^ 2 ^ (n + 1) + 1 = 0

Tactic:
rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]

Result:
no goals

Proof state:
case intro.intro
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ (n + succ 1 + 1) + 1) % 8 = 1

Tactic:
rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]

Result:
case intro.intro
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n % 8 * (2 ^ (succ 1 + 1) % 8) % 8 + 1) % 8 = 1

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
have hp2 : p ≠ 2 := by
  exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd

Result:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Proof state:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ 2 ^ 2 ^ n + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Tactic:
rw [← natCast_zmod_eq_zero_iff_dvd, Nat.cast_add _ 1, Nat.cast_one, Nat.cast_pow] at hpdvd ⊢

Result:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ↑a.val ^ 2 ^ (n + 1) + 1 = 0

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ p % 8 = 1

Tactic:
obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd

Result:
case intro
n : ℕ
hn : 1 < n
k : ℕ
hp : Prime (k * 2 ^ (n + 1) + 1)
hpdvd : k * 2 ^ (n + 1) + 1 ∣ n.fermatNumber
this : Fact (Prime (k * 2 ^ (n + 1) + 1))
hp2 : k * 2 ^ (n + 1) + 1 ≠ 2
⊢ (k * 2 ^ (n + 1) + 1) % 8 = 1

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
obtain ⟨a, ha⟩ := (exists_sq_eq_two_iff hp2).mpr (Or.inl hp8)

Result:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Proof state:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Tactic:
rw [fermatNumber] at hpdvd

Result:
case intro
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ 2 ^ 2 ^ n + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Proof state:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
have : Fact p.Prime := Fact.mk hp

Result:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1