awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L
⊢ ∃ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))),
    ∀ (n : ℕ),
      f n ≡ L [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
          ⊤]
have refine : ∀ (n : ℕ),
  f n ≡ L [SMOD
    HSMul.hSMul (β :=
      Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
        ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
      (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
      ⊤]
Tactic: refine ⟨L, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L
n : ℕ
⊢ f n ≡ L [SMOD
    HSMul.hSMul (β :=
      Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
        ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
      (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
      ⊤]
have obtain : ∀ (y : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
  (hy :
    y ∈
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K]))
  (hL :
    Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i)
      ((fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y)),
  f n ≡ (fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y [SMOD
    HSMul.hSMul (β :=
      Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
        ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
      (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
      ⊤]
Tactic: obtain ⟨y, hy, rfl⟩ := Set.mem_iInter.mp hL n
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
m n : ℕ
h : m < n
⊢ HPow.hPow (α := ℕ) 2 m < HPow.hPow (α := ℕ) 2 n
have h₁ : LT.lt (α := ℕ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 (n + 1) - 1 = 2 * (HPow.hPow (α := ℕ) 2 n - 1) + 1
have this : 1 ≤ HPow.hPow (α := ℕ) 2 n
Tactic: have := Nat.one_le_pow n 2 two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
h : Prime (mersenne p)
⊢ Prime p
have apply : p ≠ 1
Tactic: apply Nat.prime_of_pow_sub_one_prime _ h |>.2
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
k : ℕ
⊢ mersenne k + 1 = HPow.hPow (α := ℕ) 2 k
have rw : 1 ≤ HPow.hPow (α := ℕ) 2 k
Tactic: rw [mersenne, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n n_1 : ℕ
hmn : 2 ≤ n_1
h : mersenne n_1 % 4 = 3
⊢ mersenne (n_1 + 1) % 4 = 3
have succ : (2 * mersenne n_1 + 1) % 4 = 3
Tactic: rw [mersenne_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ mersenne n % 4 = 3
have base : mersenne 2 % 4 = 3
Tactic: induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n : ℕ
h : 2 ≤ n
base : mersenne 2 % 4 = 3
⊢ mersenne n % 4 = 3
have succ : ∀ (n : ℕ), 2 ≤ n → mersenne n % 4 = 3 → mersenne (n + 1) % 4 = 3
Tactic: induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n : ℕ
odd : Odd n
h : 3 ≤ n
⊢ mersenne n % 3 = 1
have obtain : ∀ (k : ℕ) (h : 3 ≤ 2 * k + 1), mersenne (2 * k + 1) % 3 = 1
Tactic: obtain ⟨k, rfl⟩ := odd
Cleared hypotheses: n, odd, h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
k : ℕ
h : 3 ≤ 2 * k + 1
⊢ mersenne (2 * k + 1) % 3 = 1
have h₁ : 1 ≤ k
Tactic: replace h : 1 ≤ k := by lia
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
k j : ℕ
hmn : 1 ≤ j
h : mersenne (2 * j + 1) % 3 = 1
⊢ mersenne (2 * (j + 1) + 1) % 3 = 1
have succ : (2 * (2 * mersenne (2 * j + 1) + 1) + 1) % 3 = 1
Tactic: rw [mersenne_succ, show 2 * (j + 1) = 2 * j + 1 + 1 by lia, mersenne_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
k : ℕ
h : 1 ≤ k
⊢ mersenne (2 * k + 1) % 3 = 1
have base : mersenne (HMul.hMul (α := ℕ) 2 1 + 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
k : ℕ
h : 1 ≤ k
base : mersenne (HMul.hMul (α := ℕ) 2 1 + 1) % 3 = 1
⊢ mersenne (2 * k + 1) % 3 = 1
have succ : ∀ (j : ℕ), 1 ≤ j → mersenne (2 * j + 1) % 3 = 1 → mersenne (2 * (j + 1) + 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n n_1 : ℕ
hmn : 3 ≤ n_1
h : mersenne n_1 % 8 = 7
⊢ mersenne (n_1 + 1) % 8 = 7
have succ : (2 * mersenne n_1 + 1) % 8 = 7
Tactic: rw [mersenne_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n : ℕ
h : 3 ≤ n
⊢ mersenne n % 8 = 7
have base : mersenne 3 % 8 = 7
Tactic: induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n : ℕ
h : 3 ≤ n
base : mersenne 3 % 8 = 7
⊢ mersenne n % 8 = 7
have succ : ∀ (n : ℕ), 3 ≤ n → mersenne n % 8 = 7 → mersenne (n + 1) % 8 = 7
Tactic: induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
⊢ legendreSym (mersenne p) 2 = 1
have this : mersenne p % 8 = 7
Tactic: have := mersenne_mod_eight hp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ legendreSym (mersenne p) 2 = 1
have rw : Eq (α := ℤ) (if mersenne p % 2 = 0 then 0 else if mersenne p % 8 = 1 ∨ mersenne p % 8 = 7 then 1 else -1) 1
Tactic: rw [legendreSym.at_two (by lia), ZMod.χ₈_nat_eq_if_mod_eight]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ legendreSym (mersenne p) 3 = -1
have rw : -legendreSym 3 (HMod.hMod (α := ℤ) (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 (HMod.hMod (α := ℤ) (↑(mersenne p) : ℤ) (↑3 : ℤ)) = -1
have rw_mod_cast : -legendreSym 3 (↑1 : ℤ) = Int.negSucc 0
Tactic: rw_mod_cast [mersenne_mod_three odd hp]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ 0 ≤ sMod p i
have zero : 0 ≤ sMod p 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
zero : 0 ≤ sMod p 0
⊢ 0 ≤ sMod p i
have succ : ∀ (n : ℕ), 0 ≤ sMod p (n + 1)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : p ≠ 0
n : ℕ
⊢ 0 ≤ (HPow.hPow (β := ℕ) (sMod p n) 2 - 2) % (HPow.hPow (α := ℤ) 2 p - 1)
have succ : HPow.hPow (α := ℤ) 2 p - 1 ≠ 0
Tactic: apply Int.emod_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p i : ℕ
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p i
have zero : sMod p 0 % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p i : ℕ
zero : sMod p 0 % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p 0
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p i
have succ : ∀ (n : ℕ), sMod p (n + 1) % (HPow.hPow (α := ℤ) 2 p - 1) = sMod p (n + 1)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i < HPow.hPow (α := ℤ) 2 p - 1
have rw : sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) < HPow.hPow (α := ℤ) 2 p - 1
Tactic: rw [← sMod_mod]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i % (HPow.hPow (α := ℤ) 2 p - 1) < HPow.hPow (α := ℤ) 2 p - 1
have refine : |HPow.hPow (α := ℤ) 2 p - 1| = HPow.hPow (α := ℤ) 2 p - 1
Tactic: refine (Int.emod_lt_abs _ (mersenne_int_ne_zero p hp)).trans_eq ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p' 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))
have 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
Tactic: push_cast [s, sZMod, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p' i : ℕ
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))
have zero : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) 0) (↑(s 0) : ZMod (2 ^ (p' + 2) - 1))
Tactic: induction i with
  | zero => dsimp [s, sZMod]; simp
  | succ i ih => push_cast [s, sZMod, ih]; rfl
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p' i : ℕ
zero : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) 0) (↑(s 0) : ZMod (2 ^ (p' + 2) - 1))
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) (sZMod (p' + 2) i) (↑(s i) : ZMod (2 ^ (p' + 2) - 1))
have 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))
Tactic: induction i with
  | zero => dsimp [s, sZMod]; simp
  | succ i ih => push_cast [s, sZMod, ih]; rfl
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p i : ℕ
⊢ sZMod p i = (↑(sMod p i) : ZMod (2 ^ p - 1))
have zero : sZMod p 0 = (↑(sMod p 0) : ZMod (2 ^ p - 1))
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p i : ℕ
zero : sZMod p 0 = (↑(sMod p 0) : ZMod (2 ^ p - 1))
⊢ sZMod p i = (↑(sMod p i) : ZMod (2 ^ p - 1))
have succ : ∀ (n : ℕ), sZMod p n = (↑(sMod p n) : ZMod (2 ^ p - 1)) → sZMod p (n + 1) = (↑(sMod p (n + 1)) : ZMod (2 ^ p - 1))
Tactic: induction i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
⊢ sZMod p 0 = (↑(sMod p 0) : ZMod (2 ^ p - 1))
have zero : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) 4 4
Tactic: push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p n : ℕ
h : sZMod p n = (↑(sMod p n) : ZMod (2 ^ p - 1))
⊢ sZMod p (n + 1) = (↑(sMod p (n + 1)) : ZMod (2 ^ p - 1))
have 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
Tactic: push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
have rw : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 ↔ sMod p (p - 2) = 0
Tactic: rw [sZMod_eq_sMod p]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
w : 1 < p
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 ↔ sMod p (p - 2) = 0
have mp : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 → sMod p (p - 2) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
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
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0 ↔ sMod p (p - 2) = 0
have mpr : sMod p (p - 2) = 0 → Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
w : 1 < p
h : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
⊢ sMod p (p - 2) = 0
have apply : 0 ≤ sMod p (p - 2)
Tactic: apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h)
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
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)
⊢ sMod p (p - 2) = 0
have apply₁ : sMod p (p - 2) < HPow.hPow (α := ℤ) 2 p - 1
Tactic: apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h)
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑(sMod p (p - 2)) : ZMod (2 ^ p - 1)) 0
have mpr : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 p - 1)) (↑0 : ZMod (2 ^ p - 1)) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y : X q
h₁ : x.1 = y.1
h₂ : x.2 = y.2
⊢ x = y
have mk : ∀ (fst snd : ZMod q) (h₁ : (fst, snd).1 = y.1) (h₂ : (fst, snd).2 = y.2), (fst, snd) = y
Tactic: cases x
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
y : X q
fst snd : ZMod q
h₁ : (fst, snd).1 = y.1
h₂ : (fst, snd).2 = y.2
⊢ (fst, snd) = y
have 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)
Tactic: cases y
Cleared hypotheses: y, h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ x * y * z = x * (y * z)
have h₁ : (x * y * z).1 = (x * (y * z)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
h₁ : (x * y * z).1 = (x * (y * z)).1
⊢ x * y * z = x * (y * z)
have h₂ : (x * y * z).2 = (x * (y * z)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ (x * y * z).1 = (x * (y * z)).1
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ (x * y * z).2 = (x * (y * z)).2
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
⊢ 1 * x = x
have h₁ : (1 * x).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
h₁ : (1 * x).1 = x.1
⊢ 1 * x = x
have h₂ : (1 * x).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
⊢ x * 1 = x
have h₁ : (x * 1).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
h₁ : (x * 1).1 = x.1
⊢ x * 1 = x
have h₂ : (x * 1).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ Eq (α := X q) (↑0) 0
have h₁ : Eq (α := ZMod q) (↑0).1 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
h₁ : Eq (α := ZMod q) (↑0).1 0.1
⊢ Eq (α := X q) (↑0) 0
have h₂ : Eq (α := ZMod q) (↑0).2 0.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q x : ℕ
⊢ ↑(x + 1) = HAdd.hAdd (α := X q) (↑x) 1
have h₁ : (↑(x + 1)).1 = (HAdd.hAdd (α := X q) (↑x) 1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q x : ℕ
h₁ : (↑(x + 1)).1 = (HAdd.hAdd (α := X q) (↑x) 1).1
⊢ ↑(x + 1) = HAdd.hAdd (α := X q) (↑x) 1
have h₂ : (↑(x + 1)).2 = (HAdd.hAdd (α := X q) (↑x) 1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
⊢ Eq (α := X q) ((↑(↑n : ℤ) : ZMod q), 0) (↑n : X q)
have h₁ : Eq (α := ZMod q) ((↑(↑n : ℤ) : ZMod q), 0).1 (↑n : X q).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
h₁ : Eq (α := ZMod q) ((↑(↑n : ℤ) : ZMod q), 0).1 (↑n : X q).1
⊢ Eq (α := X q) ((↑(↑n : ℤ) : ZMod q), 0) (↑n : X q)
have h₂ : Eq (α := ZMod q) ((↑(↑n : ℤ) : ZMod q), 0).2 (↑n : X q).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
⊢ Eq (α := X q) ((↑(Int.negSucc n) : ZMod q), 0) (-(↑(n + 1) : X q))
have h₁ : Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).1 (-(↑(n + 1) : X q)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
h₁ : Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).1 (-(↑(n + 1) : X q)).1
⊢ Eq (α := X q) ((↑(Int.negSucc n) : ZMod q), 0) (-(↑(n + 1) : X q))
have h₂ : Eq (α := ZMod q) ((↑(Int.negSucc n) : ZMod q), 0).2 (-(↑(n + 1) : X q)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ x * (y + z) = x * y + x * z
have h₁ : (x * (y + z)).1 = (x * y + x * z).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
h₁ : (x * (y + z)).1 = (x * y + x * z).1
⊢ x * (y + z) = x * y + x * z
have h₂ : (x * (y + z)).2 = (x * y + x * z).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ (x * (y + z)).1 = (x * y + x * z).1
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ (x * (y + z)).2 = (x * y + x * z).2
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ (x + y) * z = x * z + y * z
have h₁ : ((x + y) * z).1 = (x * z + y * z).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
h₁ : ((x + y) * z).1 = (x * z + y * z).1
⊢ (x + y) * z = x * z + y * z
have h₂ : ((x + y) * z).2 = (x * z + y * z).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ ((x + y) * z).1 = (x * z + y * z).1
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x y z : X q
⊢ ((x + y) * z).2 = (x * z + y * z).2
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
⊢ 0 * x = 0
have h₁ : (0 * x).1 = 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
h₁ : (0 * x).1 = 0.1
⊢ 0 * x = 0
have h₂ : (0 * x).2 = 0.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
⊢ x * 0 = 0
have h₁ : (x * 0).1 = 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x : X q
h₁ : (x * 0).1 = 0.1
⊢ x * 0 = 0
have h₂ : (x * 0).2 = 0.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x x_1 : X q
⊢ x * x_1 = x_1 * x
have h₁ : (x * x_1).1 = (x_1 * x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x x_1 : X q
h₁ : (x * x_1).1 = (x_1 * x).1
⊢ x * x_1 = x_1 * x
have h₂ : (x * x_1).2 = (x_1 * x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x x_1 : X q
⊢ (x * x_1).1 = (x_1 * x).1
have h₁ : x.1 * x_1.1 + 3 * x.2 * x_1.2 = x_1.1 * x.1 + 3 * x_1.2 * x.2
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
x x_1 : X q
⊢ (x * x_1).2 = (x_1 * x).2
have h₂ : x.1 * x_1.2 + x.2 * x_1.1 = x_1.1 * x.2 + x_1.2 * x.1
Tactic: dsimp