awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
h₁ : Eq (α := ZMod q) (↑(↑n : ℤ) : X q).1 (↑n : X q).1
h₂ : Eq (α := ZMod q) (↑(↑n : ℤ) : X q).2 (↑n : X q).2
⊢ Eq (α := X q) (↑(↑n : ℤ) : X q) (↑n : X q)

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
⊢ Eq (α := ZMod q) (↑(↑n : ℤ) : X q).1 (↑n : X q).1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
⊢ Eq (α := ZMod q) (↑(↑n : ℤ) : X q).2 (↑n : X q).2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
dsimp : HMul.hMul (α := X q) (2, 1) (2, -1) = 1
⊢ HMul.hMul (α := X q) ω ωb = 1

Tactic:
dsimp [ω, ωb]

Premises used: LucasLehmer.X.ωb, LucasLehmer.X.ω
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : (HMul.hMul (α := X q) (2, 1) (2, -1)).1 = 1.1
h₂ : (HMul.hMul (α := X q) (2, 1) (2, -1)).2 = 1.2
⊢ HMul.hMul (α := X q) (2, 1) (2, -1) = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : HMul.hMul (α := ZMod q) 2 2 + -3 = 1
⊢ (HMul.hMul (α := X q) (2, 1) (2, -1)).1 = 1.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ (HMul.hMul (α := X q) (2, 1) (2, -1)).2 = 1.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ HMul.hMul (α := ZMod q) 2 2 + -3 = 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
rw : HMul.hMul (α := X q) ω ωb = 1
rw₁ rw₂ : Eq (α := X q) 1 1
⊢ HMul.hMul (α := X q) ωb ω = 1

Tactic:
rw [mul_comm, ω_mul_ωb]

Premises used: LucasLehmer.X.ω_mul_ωb, mul_comm
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
zero : (↑4 : X q).1 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).1
zero₁ : (↑4 : X q).2 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).2
⊢ (↑4 : X q) = HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ (↑4 : X q).1 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ (↑4 : X q).2 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ Eq (α := X q) (↑(s (i + 1)) : X q) (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : X q)

Tactic:
rfl

Premises used: LucasLehmer.s, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
push_cast : HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2 = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2
⊢ (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : X q) = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2 = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw rw₁ :
  HPow.hPow (β := ℕ)
        (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
      2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
      2
⊢ HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
      2

Tactic:
rw [ih]
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (β := ℕ)
        (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HPow.hPow (α := X q) 1 (HPow.hPow (α := ℕ) 2 i) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        HMul.hMul (α := X q) 2 1 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₄ rw₅ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2

Tactic:
rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]

Premises used: one_pow, LucasLehmer.X.ωb_mul_ω, LucasLehmer.X.ωb, add_sub_cancel_right, LucasLehmer.X.ω, mul_one, mul_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
rw₁ :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2) =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
rw₂ rw₃ :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2) =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))

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

Premises used: pow_succ, pow_mul
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
ih :
  (↑(s i) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)
X :
  (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2
X₁ :
  HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
          HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
        2 -
      2
X₂ :
  HPow.hPow (β := ℕ)
        (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
          HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
        2 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 *
          (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i) *
            HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2
X₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 *
          (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i) *
            HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
X₄ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
⊢ (↑(s (i + 1)) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))

Tactic:
calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Premises used: Int.cast, HMul.hMul, HSub.hSub, HPow.hPow, HAdd.hAdd, LucasLehmer.X.ωb, LucasLehmer.X.ω, OfNat.ofNat, LucasLehmer.s, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
zero :
  (↑(s 0) : X q) =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) (β := ℕ) 2 0) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) (β := ℕ) 2 0)
succ :
  ∀ (i : ℕ)
    (ih :
      (↑(s i) : X q) =
        HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)),
    (↑(s (i + 1)) : X q) =
      HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
⊢ (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)

Tactic:
induction i with
  | zero =>
    dsimp [s, ω, ωb]
    ext <;> norm_num
  | succ i ih =>
    calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Premises used: Int.cast, HMul.hMul, HSub.hSub, HPow.hPow, HAdd.hAdd, LucasLehmer.X.ωb, Nat.zero, LucasLehmer.X.ω, OfNat.ofNat, Nat.succ, LucasLehmer.s, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : (HPow.hPow (α := X q) (β := ℕ) α 2).1 = 3.1
h₂ : (HPow.hPow (α := X q) (β := ℕ) α 2).2 = 3.2
⊢ HPow.hPow (α := X q) (β := ℕ) α 2 = 3

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ (HPow.hPow (α := X q) (β := ℕ) α 2).1 = 3.1

Tactic:
simp [α, sq]

Premises used: sq, LucasLehmer.X.α
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ (HPow.hPow (α := X q) (β := ℕ) α 2).2 = 3.2

Tactic:
simp [α, sq]

Premises used: sq, LucasLehmer.X.α
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : (HPow.hPow (β := ℕ) (HAdd.hAdd (α := X q) 1 α) 2).1 = (HMul.hMul (α := X q) 2 ω).1
h₂ : (HPow.hPow (β := ℕ) (HAdd.hAdd (α := X q) 1 α) 2).2 = (HMul.hMul (α := X q) 2 ω).2
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := X q) 1 α) 2 = HMul.hMul (α := X q) 2 ω

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : HAdd.hAdd (α := ZMod q) 1 3 = HMul.hMul (α := ZMod q) 2 2
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := X q) 1 α) 2).1 = (HMul.hMul (α := X q) 2 ω).1

Tactic:
simp [α, ω, sq]

Premises used: sq, LucasLehmer.X.α, LucasLehmer.X.ω
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₂ : HAdd.hAdd (α := ZMod q) 1 1 = 2
⊢ (HPow.hPow (β := ℕ) (HAdd.hAdd (α := X q) 1 α) 2).2 = (HMul.hMul (α := X q) 2 ω).2

Tactic:
simp [α, ω, sq]

Premises used: sq, LucasLehmer.X.α, LucasLehmer.X.ω
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ HAdd.hAdd (α := ZMod q) 1 3 = HMul.hMul (α := ZMod q) 2 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ HAdd.hAdd (α := ZMod q) 1 1 = 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
rw : HPow.hPow (α := X q) α (2 * i) * α = HPow.hPow (α := X q) 3 i * α
rw₁ : HPow.hPow (α := X q) (β := ℕ) α 2 ^ i * α = HPow.hPow (α := X q) 3 i * α
rw₂ rw₃ : HPow.hPow (α := X q) 3 i * α = HPow.hPow (α := X q) 3 i * α
⊢ HPow.hPow (α := X q) α (2 * i + 1) = HPow.hPow (α := X q) 3 i * α

Tactic:
rw [pow_succ, pow_mul, α_sq]

Premises used: pow_succ, pow_mul, LucasLehmer.X.α_sq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
⊢ Eq (α := ZMod q) (↑x : ZMod q) 0 ↔ q ∣ x

Tactic:
ZMod.natCast_eq_zero_iff _ _

Premises used: ZMod.natCast_eq_zero_iff
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
h : Eq (α := X q) (↑x : X q) 0 ↔ Eq (α := ZMod q) (↑x : ZMod q) 0
⊢ Eq (α := X q) (↑x : X q) 0 ↔ q ∣ x

Tactic:
convert! ZMod.natCast_eq_zero_iff _ _

Premises used: ZMod.natCast_eq_zero_iff
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
hx : Eq (α := ZMod q) (↑x : ZMod q) 0
⊢ Eq (α := ZMod q) (↑x : X q).2 0.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
⊢ Eq (α := X q) (↑x : X q) 0 ↔ Eq (α := ZMod q) (↑x : ZMod q) 0

Tactic:
exact ⟨congr_arg Prod.fst, fun hx ↦ ext hx (by simp)⟩
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
obtain :
  ∀ (k : ℕ) [inst : Fact (Nat.Prime (2 * k + 1))] (leg3 : legendreSym (2 * k + 1) 3 = -1),
    HAdd.hAdd (α := X (2 * k + 1)) 1 α ^ (2 * k + 1) = HSub.hSub (α := X (2 * k + 1)) 1 α
⊢ HAdd.hAdd (α := X q) 1 α ^ q = HSub.hSub (α := X q) 1 α

Tactic:
obtain ⟨k, rfl⟩ := odd

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
inst : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
⊢ HPow.hPow (α := ZMod q) 3 k = -1

Tactic:
simpa [leg3, mul_add_div, eq_comm] using legendreSym.eq_pow (2 * k + 1) 3

Premises used: HMul.hMul, Nat.mul_add_div, eq_comm, HAdd.hAdd, legendreSym.eq_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
inst : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
⊢ HPow.hPow (α := ZMod q) 3 k = -1

Tactic:
have : (3 ^ k : ZMod q) = -1 := by
    simpa [leg3, mul_add_div, eq_comm] using legendreSym.eq_pow (2 * k + 1) 3
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
inst : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : HPow.hPow (α := ZMod q) 3 k = -1
rw rw₁ : Eq (α := X q) 3 3
⊢ Eq (α := X q) 3 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 3)

Tactic:
rw [map_ofNat]

Premises used: map_ofNat
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
inst : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : HPow.hPow (α := ZMod q) 3 k = -1
rw :
  HPow.hPow (α := X (2 * k + 1)) 1 (2 * k + 1) +
      HMul.hMul (α := X (2 * k + 1)) (-(ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 1) α =
    HSub.hSub (α := X (2 * k + 1)) 1 α
⊢ HAdd.hAdd (α := X (2 * k + 1)) 1 α ^ (2 * k + 1) = HSub.hSub (α := X (2 * k + 1)) 1 α

Tactic:
rw [add_pow_expChar, α_pow, show (3 : X q) = (3 : ZMod q) by rw [map_ofNat], ← map_pow, this,
    map_neg]

Premises used: LucasLehmer.X.α_pow, map_neg, map_pow, add_pow_expChar
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
inst : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : HPow.hPow (α := ZMod q) 3 k = -1
⊢ HPow.hPow (α := X (2 * k + 1)) 1 (2 * k + 1) +
      HMul.hMul (α := X (2 * k + 1)) (-(ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 1) α =
    HSub.hSub (α := X (2 * k + 1)) 1 α

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
rw : HPow.hPow (α := X q) (β := ℕ) 1 2 - 3 = -2
⊢ HAdd.hAdd (α := X q) 1 α ^ (q + 1) = -2

Tactic:
rw [pow_succ, one_add_α_pow_q odd leg3, mul_comm, ← _root_.sq_sub_sq, α_sq]

Premises used: pow_succ, LucasLehmer.X.α_sq, LucasLehmer.X.one_add_α_pow_q, mul_comm, sq_sub_sq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ HPow.hPow (α := X q) (β := ℕ) 1 2 - 3 = -2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
rw : HAdd.hAdd (α := X q) 1 α ^ (2 * ((q + 1) / 2)) = -2
⊢ HMul.hMul (α := X q) 2 ω ^ ((q + 1) / 2) = -2

Tactic:
rw [← one_add_α_sq, ← pow_mul]

Premises used: LucasLehmer.X.one_add_α_sq, pow_mul
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
H : 2 ∣ q + 1
⊢ 2 * ((q + 1) / 2) = q + 1

Tactic:
apply Nat.mul_div_cancel'

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
H : Even (q + 1)
⊢ 2 ∣ q + 1

Tactic:
rw [← even_iff_two_dvd]

Premises used: even_iff_two_dvd
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ Even (q + 1)

Tactic:
Odd.add_one odd

Premises used: Odd.add_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ Even (q + 1)

Tactic:
exact Odd.add_one odd

Premises used: Odd.add_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ 2 * ((q + 1) / 2) = q + 1

Tactic:
have : 2 * ((q + 1) / 2) = q + 1 := by
    apply Nat.mul_div_cancel'
    rw [← even_iff_two_dvd]
    exact Odd.add_one odd
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
this : 2 * ((q + 1) / 2) = q + 1
rw : HAdd.hAdd (α := X q) 1 α ^ (q + 1) = -2
rw₁ rw₂ : Eq (α := X q) (-2) (-2)
⊢ HAdd.hAdd (α := X q) 1 α ^ (2 * ((q + 1) / 2)) = -2

Tactic:
rw [this, one_add_α_pow_q_succ odd leg3]

Premises used: LucasLehmer.X.one_add_α_pow_q_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
obtain : ∀ (w : ℕ), q = 2 * w + 1 → HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2
⊢ HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2

Tactic:
obtain ⟨_, _⟩ := odd
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
⊢ (q + 1) / 2 = q / 2 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
rw : HPow.hPow (α := ZMod q) 2 (q / 2) * 2 = 2
⊢ HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2

Tactic:
rw [(by lia : (q + 1) / 2 = q / 2 + 1), pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
⊢ (↑(legendreSym q 2) : ZMod q) = HPow.hPow (α := ZMod q) (↑2 : ZMod q) (q / 2)

Tactic:
have leg := legendreSym.eq_pow q 2
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
leg : (↑(legendreSym q 2) : ZMod q) = HPow.hPow (α := ZMod q) (↑2 : ZMod q) (q / 2)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod q) 2 2
⊢ Eq (α := ZMod q) 2 (↑2 : ZMod q)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
leg : (↑(legendreSym q 2) : ZMod q) = HPow.hPow (α := ZMod q) (↑2 : ZMod q) (q / 2)
⊢ Eq (α := ZMod q) 2 (↑2 : ZMod q)

Tactic:
have : (2 : ZMod q) = ((2 : ℤ) : ZMod q) := by norm_cast
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
leg : (↑(legendreSym q 2) : ZMod q) = HPow.hPow (α := ZMod q) (↑2 : ZMod q) (q / 2)
this : Eq (α := ZMod q) 2 (↑2 : ZMod q)
rw : HMul.hMul (α := ZMod q) (↑1 : ZMod q) (↑2 : ZMod q) = (↑2 : ZMod q)
⊢ HPow.hPow (α := ZMod q) 2 (q / 2) * 2 = 2

Tactic:
rw [this, ← leg, leg2]
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w : ℕ
h : q = 2 * w + 1
leg : (↑(legendreSym q 2) : ZMod q) = HPow.hPow (α := ZMod q) (↑2 : ZMod q) (q / 2)
this : Eq (α := ZMod q) 2 (↑2 : ZMod q)
⊢ HMul.hMul (α := ZMod q) (↑1 : ZMod q) (↑2 : ZMod q) = (↑2 : ZMod q)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
⊢ HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2

Tactic:
have pow2 : (2 : ZMod q) ^ ((q + 1) / 2) = 2 := by
    obtain ⟨_, _⟩ := odd
    rw [(by lia : (q + 1) / 2 = q / 2 + 1), pow_succ]
    have leg := legendreSym.eq_pow q 2
    have : (2 : ZMod q) = ((2 : ℤ) : ZMod q) := by norm_cast
    rw [this, ← leg, leg2]
    ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2
⊢ HMul.hMul (α := X q) 2 ω ^ ((q + 1) / 2) = -2

Tactic:
have := two_mul_ω_pow odd leg3
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2
this : HMul.hMul (α := X q) 2 ω ^ ((q + 1) / 2) = -2
⊢ HPow.hPow (α := X q) 2 ((q + 1) / 2) * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2

Tactic:
rw [mul_pow] at this

Premises used: mul_pow