-- Mathlib/NumberTheory/Fermat.lean
/-- Prime factors of `a ^ (2 ^ n) + 1` are of form `k * 2 ^ (n + 1) + 1`. -/
lemma pow_pow_add_primeFactors_one_lt {a n p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
    (hpdvd : p ∣ a ^ (2 ^ n) + 1) :
    ∃ k, p = k * 2 ^ (n + 1) + 1

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
⊢ ↑a ≠ 0

Tactic:
intro h

Result:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
h : ↑a = 0
⊢ False

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ orderOf ↑a = 2 ^ (n + 1)

Tactic:
apply orderOf_eq_prime_pow

Result:
case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬↑a ^ 2 ^ n = 1

case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ↑a ^ 2 ^ (n + 1) = 1

Proof state:
case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬↑a ^ 2 ^ n = 1

Tactic:
rw [ha1]

Result:
case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬-1 = 1

Proof state:
case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬-1 = 1

Tactic:
exact neg_one_ne_one

Result:
no goals

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

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

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

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ↑a ^ 2 ^ n + 1 = 0

Tactic:
exact_mod_cast (natCast_zmod_eq_zero_iff_dvd (a ^ (2 ^ n) + 1) p).mpr hpdvd

Result:
no goals

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
ha : orderOf ↑a = 2 ^ (n + 1)
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
simpa [ha, dvd_def, Nat.sub_eq_iff_eq_add hp.one_le, mul_comm] using orderOf_dvd_card_sub_one ha0

Result:
no goals

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : 1 = 0
h : ↑a = 0
⊢ False

Tactic:
exact one_ne_zero ha1

Result:
no goals

Proof state:
case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ↑a ^ 2 ^ (n + 1) = 1

Tactic:
rw [pow_succ, pow_mul, ha1, neg_one_sq]

Result:
no goals

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ↑a ^ 2 ^ n = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Result:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ↑a ^ 2 ^ n + 1 = 0

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
h : ↑a = 0
⊢ False

Tactic:
rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1

Result:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : 1 = 0
h : ↑a = 0
⊢ False

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

Tactic:
have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
  rw [eq_neg_iff_add_eq_zero]
  exact_mod_cast (natCast_zmod_eq_zero_iff_dvd (a ^ (2 ^ n) + 1) p).mpr hpdvd

Result:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
have : Fact (2 < p) := Fact.mk (lt_of_le_of_ne hp.two_le hp2.symm)

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

Proof state:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
have ha0 : (a : ZMod p) ≠ 0 := by
  intro h
  rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
  exact one_ne_zero ha1

Result:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1