awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k j : ℕ
hmn : 1 ≤ j
h : mersenne (2 * j + 1) % 3 = 1
succ : (2 * (2 * mersenne (2 * j + 1) + 1) + 1) % 3 = 1
⊢ mersenne (2 * (j + 1) + 1) % 3 = 1

Tactic:
rw [mersenne_succ, show 2 * (j + 1) = 2 * j + 1 + 1 by lia, mersenne_succ]

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k j : ℕ
hmn : 1 ≤ j
h : mersenne (2 * j + 1) % 3 = 1
⊢ (2 * (2 * mersenne (2 * j + 1) + 1) + 1) % 3 = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
h : 1 ≤ k
base : mersenne (HMul.hMul (α := ℕ) 2 1 + 1) % 3 = 1
succ : ∀ (j : ℕ), 1 ≤ j → mersenne (2 * j + 1) % 3 = 1 → mersenne (2 * (j + 1) + 1) % 3 = 1
⊢ mersenne (2 * k + 1) % 3 = 1

Tactic:
induction k, h using Nat.le_induction with
  | base => rfl
  | succ j _ _ =>
    rw [mersenne_succ, show 2 * (j + 1) = 2 * j + 1 + 1 by lia, mersenne_succ]
    lia

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
⊢ mersenne 3 % 8 = 7

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n n_1 : ℕ
hmn : 3 ≤ n_1
h : mersenne n_1 % 8 = 7
succ : (2 * mersenne n_1 + 1) % 8 = 7
⊢ mersenne (n_1 + 1) % 8 = 7

Tactic:
rw [mersenne_succ]

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n n_1 : ℕ
hmn : 3 ≤ n_1
h : mersenne n_1 % 8 = 7
⊢ (2 * mersenne n_1 + 1) % 8 = 7

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
h : 3 ≤ n
base : mersenne 3 % 8 = 7
succ : ∀ (n : ℕ), 3 ≤ n → mersenne n % 8 = 7 → mersenne (n + 1) % 8 = 7
⊢ mersenne n % 8 = 7

Tactic:
induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
⊢ mersenne p % 8 = 7

Tactic:
have := mersenne_mod_eight hp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ mersenne p ≠ 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
rw : Eq (α := ℤ) (if mersenne p % 2 = 0 then 0 else if mersenne p % 8 = 1 ∨ mersenne p % 8 = 7 then 1 else -1) 1
⊢ legendreSym (mersenne p) 2 = 1

Tactic:
rw [legendreSym.at_two (by lia), ZMod.χ₈_nat_eq_if_mod_eight]

Premises used: legendreSym.at_two, ZMod.χ₈_nat_eq_if_mod_eight
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ Eq (α := ℤ) (if mersenne p % 2 = 0 then 0 else if mersenne p % 8 = 1 ∨ mersenne p % 8 = 7 then 1 else -1) 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ Eq (α := ℤ) 3 (↑3 : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ HMod.hMod (α := ℕ) 3 4 = 3

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 2 ≤ p

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
rw : -legendreSym 3 (HMod.hMod (α := ℤ) (↑(mersenne p) : ℤ) (↑3 : ℤ)) = -1
⊢ legendreSym (mersenne p) 3 = -1

Tactic:
rw [(by rfl : (3 : ℤ) = (3 : ℕ)), legendreSym.quadratic_reciprocity_three_mod_four (by norm_num)
    (mersenne_mod_four (by lia)),
    legendreSym.mod]

Premises used: legendreSym.mod, legendreSym.quadratic_reciprocity_three_mod_four, mersenne_mod_four
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
rw_mod_cast : -legendreSym 3 (↑1 : ℤ) = Int.negSucc 0
⊢ -legendreSym 3 (HMod.hMod (α := ℤ) (↑(mersenne p) : ℤ) (↑3 : ℤ)) = -1

Tactic:
rw_mod_cast [mersenne_mod_three odd hp]

Premises used: mersenne_mod_three
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 (↑1 : ℤ) = Int.negSucc 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
⊢ 0 < HPow.hPow (α := ℤ) 2 p - 1

Tactic:
sub_pos.2 <| mod_cast Nat.one_lt_two_pow hp

Premises used: Iff.mpr, sub_pos, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, HPow.hPow, LT.lt, congrFun', Nat.one_lt_two_pow, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
⊢ HPow.hPow (α := ℤ) 2 p - 1 ≠ 0

Tactic:
(mersenne_int_pos hp).ne'

Premises used: LT.lt.ne', LucasLehmer.mersenne_int_pos
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
zero : 0 ≤ sMod p 0
succ : ∀ (n : ℕ), 0 ≤ sMod p (n + 1)
⊢ 0 ≤ sMod p i

Tactic:
cases i
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ 4 % (HPow.hPow (α := ℤ) 2 p - 1)

Tactic:
sup_eq_right.mp rfl

Premises used: sup_eq_right, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ 4 % (HPow.hPow (α := ℤ) 2 p - 1)

Tactic:
exact sup_eq_right.mp rfl

Premises used: sup_eq_right, Iff.mp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
n : ℕ
succ : HPow.hPow (α := ℤ) 2 p - 1 ≠ 0
⊢ 0 ≤ (HPow.hPow (β := ℕ) (sMod p n) 2 - 2) % (HPow.hPow (α := ℤ) 2 p - 1)

Tactic:
apply Int.emod_nonneg

Premises used: Int.emod_nonneg
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
n : ℕ
⊢ HPow.hPow (α := ℤ) 2 p - 1 ≠ 0

Tactic:
mersenne_int_ne_zero p hp

Premises used: LucasLehmer.mersenne_int_ne_zero
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
n : ℕ
⊢ HPow.hPow (α := ℤ) 2 p - 1 ≠ 0

Tactic:
exact mersenne_int_ne_zero p hp

Premises used: LucasLehmer.mersenne_int_ne_zero
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p i : ℕ
zero : sMod p 0 % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p 0
succ : ∀ (n : ℕ), sMod p (n + 1) % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p (n + 1)
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p i

Tactic:
cases i
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ sMod p 0 % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p 0

Tactic:
simp [sMod]

Premises used: LucasLehmer.sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p n : ℕ
⊢ sMod p (n + 1) % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p (n + 1)

Tactic:
simp [sMod]

Premises used: LucasLehmer.sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
rw : sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) < HPow.hPow (α := ℤ) 2 p - 1
⊢ sMod p i < HPow.hPow (α := ℤ) 2 p - 1

Tactic:
rw [← sMod_mod]

Premises used: LucasLehmer.sMod_mod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) < HPow.hPow (α := ℤ) 2 p - 1

Tactic:
(Int.emod_lt_abs _ (mersenne_int_ne_zero p hp)).trans_eq ?_

Premises used: Int.emod_lt_abs, LT.lt.trans_eq, LucasLehmer.mersenne_int_ne_zero
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
refine : |HPow.hPow (α := ℤ) 2 p - 1| = HPow.hPow (α := ℤ) 2 p - 1
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) < HPow.hPow (α := ℤ) 2 p - 1

Tactic:
refine (Int.emod_lt_abs _ (mersenne_int_ne_zero p hp)).trans_eq ?_

Premises used: Int.emod_lt_abs, LT.lt.trans_eq, LucasLehmer.mersenne_int_ne_zero
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ |HPow.hPow (α := ℤ) 2 p - 1| = HPow.hPow (α := ℤ) 2 p - 1

Tactic:
abs_of_nonneg (mersenne_int_pos hp).le

Premises used: LT.lt.le, LucasLehmer.mersenne_int_pos, abs_of_nonneg
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ |HPow.hPow (α := ℤ) 2 p - 1| = HPow.hPow (α := ℤ) 2 p - 1

Tactic:
exact abs_of_nonneg (mersenne_int_pos hp).le

Premises used: LT.lt.le, LucasLehmer.mersenne_int_pos, abs_of_nonneg
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) 4 (↑4 : ZMod (2 ^ (p' + 2) - 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' i : ℕ
ih : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))
succ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (β := ℕ) (↑(s i) : ZMod (2 ^ (p' + 2) - 1)) 2 - 2 =
    HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (β := ℕ) (↑(s i) : ZMod (2 ^ (p' + 2) - 1)) 2 - 2
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) (i + 1)) (↑(s (i + 1)) : ZMod (2 ^ (p' + 2) - 1))

Tactic:
push_cast [s, sZMod, ih]

Premises used: LucasLehmer.sZMod, LucasLehmer.s
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' i : ℕ
ih : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (β := ℕ) (↑(s i) : ZMod (2 ^ (p' + 2) - 1)) 2 - 2 =
    HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (β := ℕ) (↑(s i) : ZMod (2 ^ (p' + 2) - 1)) 2 - 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' i : ℕ
zero : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) 0) (↑(s 0) : ZMod (2 ^ (p' + 2) - 1))
succ :
  ∀ (i : ℕ)
    (ih : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))),
    Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) (i + 1)) (↑(s (i + 1)) : ZMod (2 ^ (p' + 2) - 1))
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))

Tactic:
induction i with
  | zero => dsimp [s, sZMod]; simp
  | succ i ih => push_cast [s, sZMod, ih]; rfl

Premises used: LucasLehmer.sZMod, Nat.zero, Nat.succ, LucasLehmer.s
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p i : ℕ
zero : sZMod p 0 = (↑(sMod p 0) : ZMod (2 ^ p - 1))
succ :
  ∀ (n : ℕ), sZMod p n = (↑(sMod p n) : ZMod (2 ^ p - 1)) → sZMod p (n + 1) = (↑(sMod p (n + 1)) : ZMod (2 ^ p - 1))
⊢ sZMod p i = (↑(sMod p i) : ZMod (2 ^ p - 1))

Tactic:
induction i
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
zero : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) 4 4
⊢ sZMod p 0 = (↑(sMod p 0) : ZMod (2 ^ p - 1))

Tactic:
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]

Premises used: LucasLehmer.sZMod, Int.coe_nat_two_pow_pred, LucasLehmer.sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p n : ℕ
h : sZMod p n = (↑(sMod p n) : ZMod (2 ^ p - 1))
succ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (β := ℕ) (↑(sMod p n) : ZMod (2 ^ p - 1)) 2 - 2 =
    HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (β := ℕ) (↑(sMod p n) : ZMod (2 ^ p - 1)) 2 - 2
⊢ sZMod p (n + 1) = (↑(sMod p (n + 1)) : ZMod (2 ^ p - 1))

Tactic:
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]

Premises used: LucasLehmer.sZMod, Int.coe_nat_two_pow_pred, LucasLehmer.sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) 4 4

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p n : ℕ
h : sZMod p n = (↑(sMod p n) : ZMod (2 ^ p - 1))
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (β := ℕ) (↑(sMod p n) : ZMod (2 ^ p - 1)) 2 - 2 =
    HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (β := ℕ) (↑(sMod p n) : ZMod (2 ^ p - 1)) 2 - 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
rw : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 ↔ sMod p (p - 2) = 0
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0

Tactic:
rw [sZMod_eq_sMod p]

Premises used: LucasLehmer.sZMod_eq_sMod
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
mp : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 → sMod p (p - 2) = 0
mpr : sMod p (p - 2) = 0 → Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 ↔ sMod p (p - 2) = 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
⊢ HPow.hPow (α := ℤ) 2 p - 1 ∣ sMod p (p - 2)

Tactic:
simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
apply : 0 ≤ sMod p (p - 2)
apply₁ : sMod p (p - 2) < HPow.hPow (α := ℤ) 2 p - 1
⊢ sMod p (p - 2) = 0

Tactic:
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h)

Premises used: Int.eq_zero_of_dvd_of_nonneg_of_lt
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
⊢ p ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)

Tactic:
exact sMod_nonneg _ (by positivity) _

Premises used: LucasLehmer.sMod_nonneg
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < HPow.hPow (α := ℤ) 2 p - 1

Tactic:
exact sMod_lt _ (by positivity) _

Premises used: LucasLehmer.sMod_lt
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
mpr : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑0 : ZMod (2 ^ p - 1)) 0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑0 : ZMod (2 ^ p - 1)) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y : X q
h₁ : x.1 = y.1
h₂ : x.2 = y.2
mk : ∀ (fst snd : ZMod q) (h₁ : (fst, snd).1 = y.1) (h₂ : (fst, snd).2 = y.2), (fst, snd) = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
y : X q
fst snd : ZMod q
h₁ : (fst, snd).1 = y.1
h₂ : (fst, snd).2 = y.2
mk :
  ∀ (fst_1 snd_1 : ZMod q) (h₁ : (fst, snd).1 = (fst_1, snd_1).1) (h₂ : (fst, snd).2 = (fst_1, snd_1).2),
    (fst, snd) = (fst_1, snd_1)
⊢ (fst, snd) = y

Tactic:
cases y
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
fst snd fst_1 snd_1 : ZMod q
h₁ : (fst, snd).1 = (fst_1, snd_1).1
h₂ : (fst, snd).2 = (fst_1, snd_1).2
⊢ (fst, snd) = (fst_1, snd_1)

Tactic:
congr
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ Eq (α := ZMod q) 0.1 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ Eq (α := ZMod q) 0.2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y : X q
⊢ (x + y).1 = x.1 + y.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y : X q
⊢ (x + y).2 = x.2 + y.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (-x).1 = -x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (-x).2 = -x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y : X q
⊢ (x * y).1 = x.1 * y.1 + 3 * x.2 * y.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y : X q
⊢ (x * y).2 = x.1 * y.2 + x.2 * y.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ Eq (α := ZMod q) 1.1 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
⊢ Eq (α := ZMod q) 1.2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ : (x * y * z).1 = (x * (y * z)).1
h₂ : (x * y * z).2 = (x * (y * z)).2
⊢ x * y * z = x * (y * z)

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ :
  (x.1 * y.1 + 3 * x.2 * y.2) * z.1 + 3 * (x.1 * y.2 + x.2 * y.1) * z.2 =
    x.1 * (y.1 * z.1 + 3 * y.2 * z.2) + 3 * x.2 * (y.1 * z.2 + y.2 * z.1)
⊢ (x * y * z).1 = (x * (y * z)).1

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₂ :
  (x.1 * y.1 + 3 * x.2 * y.2) * z.2 + (x.1 * y.2 + x.2 * y.1) * z.1 =
    x.1 * (y.1 * z.2 + y.2 * z.1) + x.2 * (y.1 * z.1 + 3 * y.2 * z.2)
⊢ (x * y * z).2 = (x * (y * z)).2

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.1 + 3 * (x.1 * y.2 + x.2 * y.1) * z.2 =
    x.1 * (y.1 * z.1 + 3 * y.2 * z.2) + 3 * x.2 * (y.1 * z.2 + y.2 * z.1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.2 + (x.1 * y.2 + x.2 * y.1) * z.1 =
    x.1 * (y.1 * z.2 + y.2 * z.1) + x.2 * (y.1 * z.1 + 3 * y.2 * z.2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
h₁ : (1 * x).1 = x.1
h₂ : (1 * x).2 = x.2
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (1 * x).1 = x.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (1 * x).2 = x.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
h₁ : (x * 1).1 = x.1
h₂ : (x * 1).2 = x.2
⊢ x * 1 = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (x * 1).1 = x.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (x * 1).2 = x.2

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
⊢ Eq (α := ZMod q) (↑n : X q).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ZMod q) (OfNat.ofNat n).1 (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ZMod q) (OfNat.ofNat n).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
h₁ : Eq (α := ZMod q) (↑0).1 0.1
h₂ : Eq (α := ZMod q) (↑0).2 0.2
⊢ Eq (α := X q) (↑0) 0

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

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

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
h₁ : (↑(x + 1)).1 = (HAdd.hAdd (α := X q) (↑x) 1).1
h₂ : (↑(x + 1)).2 = (HAdd.hAdd (α := X q) (↑x) 1).2
⊢ ↑(x + 1) = HAdd.hAdd (α := X q) (↑x) 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
⊢ (↑(x + 1)).1 = (HAdd.hAdd (α := X q) (↑x) 1).1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q x : ℕ
⊢ (↑(x + 1)).2 = (HAdd.hAdd (α := X q) (↑x) 1).2

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

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

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

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
h₁ : Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).1 (-(↑(n + 1) : X q)).1
h₂ : Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).2 (-(↑(n + 1) : X q)).2
⊢ Eq (α := X q) ((↑(Int.negSucc n) : ZMod q), 0) (-(↑(n + 1) : X q))

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
⊢ Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).1 (-(↑(n + 1) : X q)).1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q n : ℕ
⊢ Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).2 (-(↑(n + 1) : X q)).2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ : (x * (y + z)).1 = (x * y + x * z).1
h₂ : (x * (y + z)).2 = (x * y + x * z).2
⊢ x * (y + z) = x * y + x * z

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ : x.1 * (y.1 + z.1) + 3 * x.2 * (y.2 + z.2) = x.1 * y.1 + 3 * x.2 * y.2 + (x.1 * z.1 + 3 * x.2 * z.2)
⊢ (x * (y + z)).1 = (x * y + x * z).1

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₂ : x.1 * (y.2 + z.2) + x.2 * (y.1 + z.1) = x.1 * y.2 + x.2 * y.1 + (x.1 * z.2 + x.2 * z.1)
⊢ (x * (y + z)).2 = (x * y + x * z).2

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ x.1 * (y.1 + z.1) + 3 * x.2 * (y.2 + z.2) = x.1 * y.1 + 3 * x.2 * y.2 + (x.1 * z.1 + 3 * x.2 * z.2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ x.1 * (y.2 + z.2) + x.2 * (y.1 + z.1) = x.1 * y.2 + x.2 * y.1 + (x.1 * z.2 + x.2 * z.1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ : ((x + y) * z).1 = (x * z + y * z).1
h₂ : ((x + y) * z).2 = (x * z + y * z).2
⊢ (x + y) * z = x * z + y * z

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₁ : (x.1 + y.1) * z.1 + 3 * (x.2 + y.2) * z.2 = x.1 * z.1 + 3 * x.2 * z.2 + (y.1 * z.1 + 3 * y.2 * z.2)
⊢ ((x + y) * z).1 = (x * z + y * z).1

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
h₂ : (x.1 + y.1) * z.2 + (x.2 + y.2) * z.1 = x.1 * z.2 + x.2 * z.1 + (y.1 * z.2 + y.2 * z.1)
⊢ ((x + y) * z).2 = (x * z + y * z).2

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.1 + 3 * (x.2 + y.2) * z.2 = x.1 * z.1 + 3 * x.2 * z.2 + (y.1 * z.1 + 3 * y.2 * z.2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.2 + (x.2 + y.2) * z.1 = x.1 * z.2 + x.2 * z.1 + (y.1 * z.2 + y.2 * z.1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
h₁ : (0 * x).1 = 0.1
h₂ : (0 * x).2 = 0.2
⊢ 0 * x = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (0 * x).1 = 0.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (0 * x).2 = 0.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
h₁ : (x * 0).1 = 0.1
h₂ : (x * 0).2 = 0.2
⊢ x * 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (x * 0).1 = 0.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x : X q
⊢ (x * 0).2 = 0.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x x_1 : X q
h₁ : (x * x_1).1 = (x_1 * x).1
h₂ : (x * x_1).2 = (x_1 * x).2
⊢ x * x_1 = x_1 * x

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x x_1 : X q
h₁ : x.1 * x_1.1 + 3 * x.2 * x_1.2 = x_1.1 * x.1 + 3 * x_1.2 * x.2
⊢ (x * x_1).1 = (x_1 * x).1

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x x_1 : X q
h₂ : x.1 * x_1.2 + x.2 * x_1.1 = x_1.1 * x.2 + x_1.2 * x.1
⊢ (x * x_1).2 = (x_1 * x).2

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x x_1 : X q
⊢ x.1 * x_1.1 + 3 * x.2 * x_1.2 = x_1.1 * x.1 + 3 * x_1.2 * x.2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
x x_1 : X q
⊢ x.1 * x_1.2 + x.2 * x_1.1 = x_1.1 * x.2 + x_1.2 * x.1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (1 < q)
⊢ Nontrivial (X q)

Tactic:
⟨⟨0, 1, ne_of_apply_ne Prod.fst zero_ne_one⟩⟩

Premises used: zero_ne_one, Nontrivial.mk, ne_of_apply_ne, Prod.fst, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
n : ℤ
⊢ Eq (α := ZMod q) (↑n : X q).1 (↑n : ZMod q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
n : ℤ
⊢ Eq (α := ZMod q) (↑n : X q).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
n m : ℤ
h₁ : (↑(n * m) : X q).1 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).1
h₂ : (↑(n * m) : X q).2 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).2
⊢ (↑(n * m) : X q) = HMul.hMul (α := X q) (↑n : X q) (↑m : X q)

Tactic:
ext
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
n m : ℤ
⊢ (↑(n * m) : X q).1 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
n m : ℤ
⊢ (↑(n * m) : X q).2 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).2

Tactic:
simp