awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ))
          (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1
⊢ 1 ≤ HPow.hPow (α := ℕ) 2 (p' + 2)

Tactic:
have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ))
          (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1
this : 1 ≤ HPow.hPow (α := ℕ) 2 (p' + 2)
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ)) (↑(mersenne (p' + 2)) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1

Tactic:
mod_cast h

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, Nat.cast_sub._simp_1, HSub.hSub, cast, Nat.cast, mersenne, Int.cast_mul._simp_1, HPow.hPow, HAdd.hAdd, congr, congrFun', LucasLehmer.X.ω, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ))
          (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1
this : 1 ≤ HPow.hPow (α := ℕ) 2 (p' + 2)
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ)) (↑(mersenne (p' + 2)) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1

Tactic:
exact mod_cast h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
h₁ : Eq (α := ZMod (↑(q p) : ℕ)) (↑(mersenne p) : X (↑(q p) : ℕ)).1 0.1
h₂ : Eq (α := ZMod (↑(q p) : ℕ)) (↑(mersenne p) : X (↑(q p) : ℕ)).2 0.2
⊢ Eq (α := X (↑(q p) : ℕ)) (↑(mersenne p) : X (↑(q p) : ℕ)) 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
h₁ : (HPow.hPow (α := ℕ) 2 p - 1).minFac ∣ HPow.hPow (α := ℕ) 2 p - 1
⊢ Eq (α := ZMod (↑(q p) : ℕ)) (↑(mersenne p) : X (↑(q p) : ℕ)).1 0.1

Tactic:
simp [mersenne, q, ZMod.natCast_eq_zero_iff, -pow_pos]

Premises used: pow_pos, ZMod.natCast_eq_zero_iff, mersenne, LucasLehmer.q
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ Eq (α := ZMod (↑(q p) : ℕ)) (↑(mersenne p) : X (↑(q p) : ℕ)).2 0.2

Tactic:
simp [mersenne, q, ZMod.natCast_eq_zero_iff, -pow_pos]

Premises used: pow_pos, ZMod.natCast_eq_zero_iff, mersenne, LucasLehmer.q
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ (HPow.hPow (α := ℕ) 2 p - 1).minFac ∣ HPow.hPow (α := ℕ) 2 p - 1

Tactic:
apply Nat.minFac_dvd

Premises used: Nat.minFac_dvd
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
obtain :
  ∀ (k : ℤ)
    (w :
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
        HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ))
              (↑(mersenne (p' + 2)) : X (↑(q (p' + 2)) : ℕ)) *
            HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
          1),
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) = -1
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) = -1

Tactic:
obtain ⟨k, w⟩ := ω_pow_formula p' h

Premises used: LucasLehmer.ω_pow_formula
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
k : ℤ
w :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ)) (↑(mersenne (p' + 2)) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ)) 0 *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1

Tactic:
rw [mersenne_coe_X] at w

Premises used: LucasLehmer.mersenne_coe_X
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
k : ℤ
w :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑k : X (↑(q (p' + 2)) : ℕ)) 0 *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) = -1

Tactic:
simpa using w
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
rw :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 2)) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1) * 2)
rw₁ rw₂ :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 2)) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1).succ)
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 2)) =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1))) 2

Tactic:
rw [← pow_mul, ← Nat.pow_succ]

Premises used: Nat.pow_succ, pow_mul
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
rw rw₁ : HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (β := ℕ) (-1) 2 = HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (β := ℕ) (-1) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1))) 2 =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (β := ℕ) (-1) 2

Tactic:
rw [ω_pow_eq_neg_one p' h]

Premises used: LucasLehmer.ω_pow_eq_neg_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (β := ℕ) (-1) 2 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ (↑(ωUnit p) : X (↑(q p) : ℕ)) = ω

Tactic:
rfl

Premises used: LucasLehmer.X.ω, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
pp : Nat.Prime 2
h₁ : ¬orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1)
h₂ : orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1 + 1)
⊢ orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) = HPow.hPow (α := ℕ) 2 (p' + 2)

Tactic:
apply Nat.eq_prime_pow_of_dvd_least_prime_pow

Premises used: Nat.eq_prime_pow_of_dvd_least_prime_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ Nat.Prime 2

Tactic:
Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ Nat.Prime 2

Tactic:
exact Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
o : orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1)
⊢ Eq (α := X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ))
        (HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1))) :
      X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ)) 1 :
      X (↑(q (p' + 2)) : ℕ))

Tactic:
have ω_pow :=
      congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) <|
        orderOf_dvd_iff_pow_eq_one.1 o
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
o : orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1)
ω_pow :
  Eq (α := X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ))
        (HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1))) :
      X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ)) 1 :
      X (↑(q (p' + 2)) : ℕ))
⊢ Eq (α := ZMod (↑(q (p' + 2)) : ℕ)) 1 (-1)

Tactic:
have h : (1 : ZMod (q (p' + 2))) = -1 :=
      congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h_1 : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
o : orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1)
ω_pow :
  Eq (α := X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ))
        (HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1))) :
      X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ)) 1 :
      X (↑(q (p' + 2)) : ℕ))
h : Eq (α := ZMod (↑(q (p' + 2)) : ℕ)) 1 (-1)
⊢ Fact (2 < (↑(q (p' + 2)) : ℕ))

Tactic:
haveI : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h_1 : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
o : orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1)
ω_pow :
  Eq (α := X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ))
        (HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1))) :
      X (↑(q (p' + 2)) : ℕ))
    ((Units.coeHom (X (↑(q (p' + 2)) : ℕ)) : (a : (X (↑(q (p' + 2)) : ℕ))ˣ) → X (↑(q (p' + 2)) : ℕ)) 1 :
      X (↑(q (p' + 2)) : ℕ))
h : Eq (α := ZMod (↑(q (p' + 2)) : ℕ)) 1 (-1)
this : Fact (2 < (↑(q (p' + 2)) : ℕ))
⊢ False

Tactic:
apply ZMod.neg_one_ne_one h.symm

Premises used: ZMod.neg_one_ne_one, Eq.symm
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
h₂ : HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1 + 1)) = 1
⊢ orderOf (G := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) ∣ HPow.hPow (α := ℕ) 2 (p' + 1 + 1)

Tactic:
apply orderOf_dvd_iff_pow_eq_one.2

Premises used: Iff.mpr, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
h₂ :
  (↑(HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1 + 1))) :
      X (↑(q (p' + 2)) : ℕ)) =
    (↑1 : X (↑(q (p' + 2)) : ℕ))
⊢ HPow.hPow (α := (X (↑(q (p' + 2)) : ℕ))ˣ) (ωUnit (p' + 2)) (HPow.hPow (α := ℕ) 2 (p' + 1 + 1)) = 1

Tactic:
apply Units.ext

Premises used: Units.ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (↑(ωUnit (p' + 2)) : X (↑(q (p' + 2)) : ℕ))
      (HPow.hPow (α := ℕ) 2 (p' + 1 + 1)) =
    1

Tactic:
ω_pow_eq_one p' h

Premises used: LucasLehmer.ω_pow_eq_one, LucasLehmer.X.ω
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) (↑(ωUnit (p' + 2)) : X (↑(q (p' + 2)) : ℕ))
      (HPow.hPow (α := ℕ) 2 (p' + 1 + 1)) =
    1

Tactic:
exact ω_pow_eq_one p' h

Premises used: LucasLehmer.ω_pow_eq_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (lucasLehmerResidue (p' + 2)) 0
⊢ HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2

Tactic:
calc
    2 ^ (p' + 2) = orderOf (ωUnit (p' + 2)) := (order_ω p' h).symm
    _ ≤ Fintype.card (X (q (p' + 2)))ˣ := orderOf_le_card_univ
    _ < q (p' + 2) ^ 2 := card_units_lt (Nat.lt_of_succ_lt (two_lt_q _))

Premises used: Trans.trans, orderOf_le_card_univ, LucasLehmer.X.card_units_lt, LucasLehmer.two_lt_q, LucasLehmer.order_ω, Nat.lt_of_succ_lt, Eq.symm
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
⊢ let p' := p - 2;
  p' = p - 2

Tactic:
set p' := p - 2 with hp'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
p' : ℕ := p - 2
hp' : p' = p - 2
clear_value : ∀ (p' : ℕ) (hp' : p' = p - 2), LucasLehmerTest p → Nat.Prime (mersenne p)
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
clear_value p'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
p' : ℕ
hp' : p' = p - 2
obtain : ∀ (w : 1 < p' + 2) (hp' : p' = p' + 2 - 2), LucasLehmerTest (p' + 2) → Nat.Prime (mersenne (p' + 2))
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
obtain rfl : p = p' + 2 := by lia

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 1 < p' + 2
hp' : p' = p' + 2 - 2
⊢ 1 < p' + 2

Tactic:
have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
contrapose : ¬Nat.Prime (mersenne (p' + 2)) → ¬LucasLehmerTest (p' + 2)
⊢ LucasLehmerTest (p' + 2) → Nat.Prime (mersenne (p' + 2))

Tactic:
contrapose
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2

Tactic:
have h₁ := order_ineq p' t
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2
⊢ HPow.hPow (β := ℕ) (mersenne (p' + 2)).minFac 2 ≤ mersenne (p' + 2)

Tactic:
have h₂ := Nat.minFac_sq_le_self (mersenne_pos.2 (Nat.lt_of_succ_lt w)) a
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2
h₂ : HPow.hPow (β := ℕ) (mersenne (p' + 2)).minFac 2 ≤ mersenne (p' + 2)
⊢ HPow.hPow (α := ℕ) 2 (p' + 2) < mersenne (p' + 2)

Tactic:
have h := lt_of_lt_of_le h₁ h₂
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2
h₂ : HPow.hPow (β := ℕ) (mersenne (p' + 2)).minFac 2 ≤ mersenne (p' + 2)
h : HPow.hPow (α := ℕ) 2 (p' + 2) < mersenne (p' + 2)
⊢ False

Tactic:
not_lt_of_ge (Nat.sub_le _ _) h

Premises used: Nat.sub_le, not_lt_of_ge
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w_1 : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
h₁ : HPow.hPow (α := ℕ) 2 (p' + 2) < HPow.hPow (β := ℕ) (↑(q (p' + 2)) : ℕ) 2
h₂ : HPow.hPow (β := ℕ) (mersenne (p' + 2)).minFac 2 ≤ mersenne (p' + 2)
h : HPow.hPow (α := ℕ) 2 (p' + 2) < mersenne (p' + 2)
⊢ False

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

Premises used: Nat.sub_le, not_lt_of_ge
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
⊢ Fact (Nat.Prime (mersenne p))

Tactic:
have : Fact (mersenne p).Prime := ⟨‹_›⟩
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
⊢ let p' := p - 2;
  p' = p - 2

Tactic:
set p' := p - 2 with hp'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ := p - 2
hp' : p' = p - 2
clear_value : ∀ (p' : ℕ) (hp' : p' = p - 2), LucasLehmerTest p
⊢ LucasLehmerTest p

Tactic:
clear_value p'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
obtain :
  ∀ (w : 3 ≤ p' + 2) (hp : Nat.Prime (mersenne (p' + 2))) (this : Fact (Nat.Prime (mersenne (p' + 2))))
    (hp' : p' = p' + 2 - 2), LucasLehmerTest (p' + 2)
⊢ LucasLehmerTest p

Tactic:
obtain rfl : p = p' + 2 := by lia

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
rw :
  (HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ωb (HPow.hPow (α := ℕ) 2 p')).1 =
    0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) (p' + 2 - 2)) 0

Tactic:
rw [sZMod_eq_s p', ← X.fst_intCast, X.closed_form, add_tsub_cancel_right]

Premises used: LucasLehmer.X.closed_form, LucasLehmer.sZMod_eq_s, LucasLehmer.X.fst_intCast, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ Odd (mersenne (p' + 2))

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ p' + 2 ≠ 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ 4 ∣ mersenne (p' + 2) + 1

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ HPow.hPow (α := X (mersenne (p' + 2))) X.ω ((mersenne (p' + 2) + 1) / 4) +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb ((mersenne (p' + 2) + 1) / 4) =
    0

Tactic:
have := X.ω_pow_trace (q := mersenne (p' + 2)) (by simp)
    (legendreSym_mersenne_three w <| hp.of_mersenne.odd_of_ne_two (by lia))
    (legendreSym_mersenne_two w) (by simp [pow_add])
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this_1 : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this :
  HPow.hPow (α := X (mersenne (p' + 2))) X.ω (HPow.hPow (α := ℕ) 2 p' * HPow.hPow (α := ℕ) (β := ℕ) 2 2 / 4) +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb (HPow.hPow (α := ℕ) 2 p' * HPow.hPow (α := ℕ) (β := ℕ) 2 2 / 4) =
    0
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 2 = 4

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this_1 : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this :
  HPow.hPow (α := X (mersenne (p' + 2))) X.ω (HPow.hPow (α := ℕ) 2 p' * 4 / 4) +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb (HPow.hPow (α := ℕ) 2 p' * 4 / 4) =
    0
⊢ Ne (α := ℕ) 4 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this_1 : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this :
  HPow.hPow (α := X (mersenne (p' + 2))) X.ω ((mersenne (p' + 2) + 1) / 4) +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb ((mersenne (p' + 2) + 1) / 4) =
    0
⊢ HPow.hPow (α := X (mersenne (p' + 2))) X.ω (HPow.hPow (α := ℕ) 2 p') +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb (HPow.hPow (α := ℕ) 2 p') =
    0

Tactic:
rw [succ_mersenne, pow_add, show 2 ^ 2 = 4 by norm_num, mul_div_cancel_right₀ _ (by norm_num)]
    at this

Premises used: pow_add, succ_mersenne, mul_div_cancel_right₀
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this_1 : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this :
  HPow.hPow (α := X (mersenne (p' + 2))) X.ω (HPow.hPow (α := ℕ) 2 p') +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb (HPow.hPow (α := ℕ) 2 p') =
    0
⊢ (HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ωb (HPow.hPow (α := ℕ) 2 p')).1 =
    0

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 2 ≤ p
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) 0) : ℤ) = sMod p 0

Tactic:
grind [sModNat, sMod]

Premises used: LucasLehmer.norm_num_ext.sModNat, LucasLehmer.sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 2 ≤ p
n : ℕ
h : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n
⊢ GT.gt (α := ℕ) 2 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 2 ≤ p
n : ℕ
h : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (α := ℕ) 2 p

Tactic:
have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 2 ≤ p
n : ℕ
h : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n
this : HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (α := ℕ) 2 p
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) (n + 1)) : ℤ) = sMod p (n + 1)

Tactic:
grind [sModNat, sMod, Int.emod_eq_add_self_emod]

Premises used: LucasLehmer.norm_num_ext.sModNat, LucasLehmer.sMod, Int.emod_eq_add_self_emod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p k : ℕ
hp : 2 ≤ p
zero : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) 0) : ℤ) = sMod p 0
succ :
  ∀ (n : ℕ),
    (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n →
      (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) (n + 1)) : ℤ) = sMod p (n + 1)
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) k) : ℤ) = sMod p k

Tactic:
induction k with
  | zero => grind [sModNat, sMod]
  | succ =>
    have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp
    grind [sModNat, sMod, Int.emod_eq_add_self_emod]

Premises used: LucasLehmer.norm_num_ext.sModNat, LucasLehmer.sMod, Int.emod_eq_add_self_emod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ sModNat_aux (4 % q) q 0 = sModNat q 0

Tactic:
rfl