awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HPow.hPow (α := X q) 2 ((q + 1) / 2) * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2
rw rw₁ : Eq (α := X q) 2 2
⊢ Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)

Tactic:
rw [map_ofNat]

Premises used: map_ofNat
-- 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 : HPow.hPow (α := X q) 2 ((q + 1) / 2) * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2
⊢ Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)

Tactic:
have coe : (2 : X q) = (2 : ZMod q) := by rw [map_ofNat]
-- 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 : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
⊢ -2 = HMul.hMul (α := X q) 2 (-1)

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
pow2 : HPow.hPow (α := ZMod q) 2 ((q + 1) / 2) = 2
this : HPow.hPow (α := X q) 2 ((q + 1) / 2) * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
⊢ 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)

Tactic:
rw [coe, ← map_pow, pow2, ← coe,
    (by ring : (-2 : X q) = 2 * -1)] at this

Premises used: map_pow
-- 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 : HPow.hPow (α := X q) 2 ((q + 1) / 2) * HPow.hPow (α := X q) ω ((q + 1) / 2) = -2
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
this₁ : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)
⊢ Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)

Tactic:
rw [coe, ← map_pow, pow2, ← coe,
    (by ring : (-2 : X q) = 2 * -1)] at this

Premises used: map_pow
-- 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 : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
⊢ HPow.hPow (α := X q) ω ((q + 1) / 2) = -1

Tactic:
(IsUnit.of_mul_eq_one (M := X q) ↑((q + 1) / 2) ?_).mul_left_cancel this

Premises used: IsUnit.of_mul_eq_one, HDiv.hDiv, Nat.cast, IsUnit.mul_left_cancel, HAdd.hAdd, OfNat.ofNat
-- 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 : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
refine : HMul.hMul (α := X q) 2 (↑((q + 1) / 2) : X q) = 1
⊢ HPow.hPow (α := X q) ω ((q + 1) / 2) = -1

Tactic:
refine (IsUnit.of_mul_eq_one (M := X q) ↑((q + 1) / 2) ?_).mul_left_cancel this

Premises used: IsUnit.of_mul_eq_one, HDiv.hDiv, Nat.cast, IsUnit.mul_left_cancel, HAdd.hAdd, OfNat.ofNat
-- 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 : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
norm_cast : Eq (α := X q) (↑(2 * ((q + 1) / 2)) : X q) 1
⊢ HMul.hMul (α := X q) 2 (↑((q + 1) / 2) : X q) = 1

Tactic:
norm_cast
-- 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 : 2 * HPow.hPow (α := X q) ω ((q + 1) / 2) = HMul.hMul (α := X q) 2 (-1)
coe : Eq (α := X q) 2 ((ZMod.castHom ⋯ (X q) : (a : ZMod q) → X q) 2)
⊢ Eq (α := X q) (↑(2 * ((q + 1) / 2)) : X q) 1

Tactic:
simp [Nat.mul_div_cancel' odd.add_one.two_dvd]

Premises used: Even.two_dvd, Odd.add_one, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
rw : -1 * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
⊢ HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)

Tactic:
rw [pow_ω odd leg3 leg2]

Premises used: LucasLehmer.X.pow_ω
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
⊢ -1 * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)

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
hq4 : 4 ∣ q + 1
⊢ HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)

Tactic:
have : (ω : X q) ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4) := by
    rw [pow_ω odd leg3 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
hq4 : 4 ∣ q + 1
this :
  HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
rcases : ∀ (k : ℕ) (hk : q + 1 = 4 * k), (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
rcases hq4 with ⟨k, hk⟩
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
this :
  HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
k : ℕ
hk : q + 1 = 4 * k
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this :
  HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
have div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4 := by rcases hq4 with ⟨k, hk⟩; lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this :
  HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ HPow.hPow (α := X q) ω ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)

Tactic:
rw [div4, pow_add, mul_assoc, ← mul_pow, ω_mul_ωb, one_pow, mul_one] at this

Premises used: one_pow, mul_assoc, pow_add, LucasLehmer.X.ω_mul_ωb, mul_one, mul_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this :
  HPow.hPow (α := X q) ω ((q + 1) / 2) * HPow.hPow (α := X q) ωb ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
this₁ : HPow.hPow (α := X q) ω ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
rw [div4, pow_add, mul_assoc, ← mul_pow, ω_mul_ωb, one_pow, mul_one] at this

Premises used: one_pow, mul_assoc, pow_add, LucasLehmer.X.ω_mul_ωb, mul_one, mul_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : HPow.hPow (α := X q) ω ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
rw : -HPow.hPow (α := X q) ωb ((q + 1) / 4) + HPow.hPow (α := X q) ωb ((q + 1) / 4) = 0
⊢ HPow.hPow (α := X q) ω ((q + 1) / 4) + HPow.hPow (α := X q) ωb ((q + 1) / 4) = 0

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : HPow.hPow (α := X q) ω ((q + 1) / 4) = -HPow.hPow (α := X q) ωb ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ -HPow.hPow (α := X q) ωb ((q + 1) / 4) + HPow.hPow (α := X q) ωb ((q + 1) / 4) = 0

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : NeZero q
rw : Fintype.card (ZMod q) * Fintype.card (ZMod q) = HPow.hPow (β := ℕ) q 2
rw₁ : q * q = HPow.hPow (β := ℕ) q 2
rw₂ rw₃ : q * q = q * q
⊢ Fintype.card (ZMod q × ZMod q) = HPow.hPow (β := ℕ) q 2

Tactic:
rw [Fintype.card_prod, ZMod.card q, sq]

Premises used: sq, Fintype.card_prod, ZMod.card
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : NeZero q
w : 1 < q
⊢ Fact (1 < q)

Tactic:
have : Fact (1 < (q : ℕ)) := ⟨w⟩
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : NeZero q
w : 1 < q
this : Fact (1 < q)
⊢ Fintype.card (X q)ˣ < Fintype.card (X q)

Tactic:
card_units_lt (X q)

Premises used: card_units_lt, LucasLehmer.X
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : NeZero q
w : 1 < q
this : Fact (1 < q)
h : HPow.hPow (β := ℕ) q 2 = Fintype.card (X q)
⊢ Fintype.card (X q)ˣ < HPow.hPow (β := ℕ) q 2

Tactic:
convert! card_units_lt (X q)
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q : ℕ
inst : NeZero q
w : 1 < q
this : Fact (1 < q)
h h₁ : HPow.hPow (β := ℕ) q 2 = HPow.hPow (β := ℕ) q 2
⊢ HPow.hPow (β := ℕ) q 2 = Fintype.card (X q)

Tactic:
rw [card_eq]

Premises used: LucasLehmer.X.card_eq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ 2 < q (p' + 2)

Tactic:
(minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_

Premises used: Iff.mpr, one_lt_mersenne, Nat.minFac, LT.lt.ne', Nat.Prime.two_le, LE.le.lt_of_ne', Nat.minFac_prime, ite
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
refine_1 : 1 < p' + 2
refine_2 : (mersenne (p' + 2)).minFac ≠ 2
⊢ 2 < q (p' + 2)

Tactic:
refine (minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_

Premises used: Iff.mpr, one_lt_mersenne, LT.lt.ne', Nat.Prime.two_le, LE.le.lt_of_ne', Nat.minFac_prime
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ 1 < p' + 2

Tactic:
le_add_left _ _

Premises used: Nat.le_add_left, Nat.lt
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ 1 < p' + 2

Tactic:
exact le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
refine_2 : ¬2 ∣ 2 * HPow.hPow (α := ℕ) 2 (p' + 1) - 1
⊢ (mersenne (p' + 2)).minFac ≠ 2

Tactic:
rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']

Premises used: Nat.pow_succ', Nat.minFac_eq_two_iff, Ne, mersenne
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ ¬2 ∣ 2 * HPow.hPow (α := ℕ) 2 (p' + 1) - 1

Tactic:
Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

Premises used: Nat.one_le_two_pow, Nat.two_not_dvd_two_mul_sub_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
⊢ ¬2 ∣ 2 * HPow.hPow (α := ℕ) 2 (p' + 1) - 1

Tactic:
exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

Premises used: Nat.one_le_two_pow, Nat.two_not_dvd_two_mul_sub_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) (p' + 2 - 2)) 0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (↑(s (p' + 2 - 2)) : ZMod (2 ^ (p' + 2) - 1)) 0

Tactic:
rw [sZMod_eq_s p'] at h

Premises used: LucasLehmer.sZMod_eq_s
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (↑(s (p' + 2 - 2)) : ZMod (2 ^ (p' + 2) - 1)) 0
⊢ HPow.hPow (α := ℤ) 2 (p' + 2) - 1 ∣ s p'

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' : ℕ
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (↑(s (p' + 2 - 2)) : ZMod (2 ^ (p' + 2) - 1)) 0
⊢ HPow.hPow (α := ℤ) 2 (p' + 2) - 1 ∣ s p'

Tactic:
replace h : 2 ^ (p' + 2) - 1 ∣ s p' := by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
h : HPow.hPow (α := ℤ) 2 (p' + 2) - 1 ∣ s p'
obtain :
  ∀ (k : ℤ) (h : s p' = (HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k),
    ∃ (k : ℤ),
      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
⊢ ∃ (k : ℤ),
    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:
obtain ⟨k, h⟩ := h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h : s p' = (HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k
h₁ :
  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
⊢ ∃ (k : ℤ),
    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:
use k
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h : s p' = (HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k
⊢ Eq (α := X (↑(q (p' + 2)) : ℕ)) ((fun (n : ℤ) ↦ ((↑n : X (↑(q (p' + 2)) : ℕ)) : X (↑(q (p' + 2)) : ℕ))) (s p'))
    ((fun (n : ℤ) ↦ ((↑n : X (↑(q (p' + 2)) : ℕ)) : X (↑(q (p' + 2)) : ℕ))) ((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k))

Tactic:
replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  Eq (α := X (↑(q (p' + 2)) : ℕ)) (↑(s p') : X (↑(q (p' + 2)) : ℕ))
    (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p') =
    (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))

Tactic:
rw [closed_form] at h

Premises used: LucasLehmer.X.closed_form
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p') =
    (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
⊢ Eq (α := X (↑(q (p' + 2)) : ℕ))
    ((fun (x : X (↑(q (p' + 2)) : ℕ)) ↦ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') * x)
      (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p')))
    ((fun (x : X (↑(q (p' + 2)) : ℕ)) ↦ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') * x)
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ)))

Tactic:
replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p')) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
⊢ HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p')) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
⊢ HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)

Tactic:
have t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1) := by ring
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p')) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = 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') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))

Tactic:
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h

Premises used: one_pow, pow_add, HPow.hPow, LucasLehmer.X.ω_mul_ωb, LucasLehmer.X.ωb, mul_add, LucasLehmer.X.ω, OfNat.ofNat, mul_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ωb (HPow.hPow (α := ℕ) 2 p')) =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
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)) + 1 =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
⊢ HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)

Tactic:
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h

Premises used: one_pow, pow_add, HPow.hPow, LucasLehmer.X.ω_mul_ωb, LucasLehmer.X.ωb, mul_add, LucasLehmer.X.ω, OfNat.ofNat, mul_pow
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 1 =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 1 =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ))
        (↑k : X (↑(q (p' + 2)) : ℕ)) *
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p')

Tactic:
rw [mul_comm, coe_mul] at h

Premises used: mul_comm, LucasLehmer.X.coe_mul
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 1 =
    HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') *
      (↑((HPow.hPow (α := ℤ) 2 (p' + 2) - 1) * k) : X (↑(q (p' + 2)) : ℕ))
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)) + 1 =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ))
        (↑k : X (↑(q (p' + 2)) : ℕ)) *
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p')
⊢ HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)

Tactic:
rw [mul_comm, coe_mul] at h

Premises used: mul_comm, LucasLehmer.X.coe_mul
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 1 =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ))
        (↑k : X (↑(q (p' + 2)) : ℕ)) *
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p')
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)
⊢ HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 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')

Tactic:
rw [mul_comm _ (k : X (q (p' + 2)))] at h

Premises used: Int.cast, mul_comm
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 1 =
    HMul.hMul (α := X (↑(q (p' + 2)) : ℕ)) (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ))
        (↑k : X (↑(q (p' + 2)) : ℕ)) *
      HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p')
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)) + 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')
⊢ HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = HPow.hPow (α := ℕ) 2 (p' + 1)

Tactic:
rw [mul_comm _ (k : X (q (p' + 2)))] at h

Premises used: Int.cast, mul_comm
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p' : ℕ
k : ℤ
h :
  HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 (p' + 1)) + 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')
t : HPow.hPow (α := ℕ) 2 p' + HPow.hPow (α := ℕ) 2 p' = 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)) : ℕ))
          (↑(HPow.hPow (α := ℤ) 2 (p' + 2) - 1) : X (↑(q (p' + 2)) : ℕ)) *
        HPow.hPow (α := X (↑(q (p' + 2)) : ℕ)) ω (HPow.hPow (α := ℕ) 2 p') -
      1

Tactic:
replace h := eq_sub_of_add_eq h
-- 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
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide