-- Mathlib/NumberTheory/LucasLehmer.lean
theorem order_ω (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
    orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2)

Proof state:
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False

Tactic:
apply ZMod.neg_one_ne_one h.symm

Result:
no goals

Proof state:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
apply orderOf_dvd_iff_pow_eq_one.2

Result:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ωUnit (p' + 2) ^ 2 ^ (p' + 1) = 1
⊢ False

Tactic:
replace ω_pow :=
  congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) ω_pow

Result:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : (Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = (Units.coeHom (X (q (p' + 2)))) 1
⊢ False

Proof state:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2)

Tactic:
apply Nat.eq_prime_pow_of_dvd_least_prime_pow

Result:
case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2

case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Proof state:
case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2

Tactic:
exact Nat.prime_two

Result:
no goals

Proof state:
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
⊢ False

Tactic:
haveI : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩

Result:
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False

Tactic:
have ω_pow := orderOf_dvd_iff_pow_eq_one.1 o

Result:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ωUnit (p' + 2) ^ 2 ^ (p' + 1) = 1
⊢ False

Proof state:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1

Tactic:
apply Units.ext

Result:
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

Tactic:
intro o

Result:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False

Tactic:
have h : (1 : ZMod (q (p' + 2))) = -1 :=
  congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))

Result:
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
⊢ False

Proof state:
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1

Tactic:
exact ω_pow_eq_one p' h

Result:
no goals

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : (Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = (Units.coeHom (X (q (p' + 2)))) 1
⊢ False

Tactic:
simp? at ω_pow says
  simp only [Units.coeHom_apply, Units.val_pow_eq_pow_val, ωUnit_coe, Units.val_one] at ω_pow

Result:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False

Proof state:
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1

Tactic:
push_cast

Result:
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1

Proof state:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : (Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = (Units.coeHom (X (q (p' + 2)))) 1
⊢ False

Tactic:
simp only [Units.coeHom_apply, Units.val_pow_eq_pow_val, ωUnit_coe, Units.val_one] at ω_pow

Result:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False