awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ (HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ωb (HPow.hPow (α := ℕ) 2 p')).1 =
    0
have this₁ : HPow.hPow (α := X (mersenne (p' + 2))) X.ω ((mersenne (p' + 2) + 1) / 4) +
    HPow.hPow (α := X (mersenne (p' + 2))) X.ωb ((mersenne (p' + 2) + 1) / 4) =
  0
Tactic: have := X.ω_pow_trace (q := mersenne (p' + 2)) (by simp)
    (legendreSym_mersenne_three w <| hp.of_mersenne.odd_of_ne_two (by lia))
    (legendreSym_mersenne_two w) (by simp [pow_add])
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this_1 : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this :
  HPow.hPow (α := X (mersenne (p' + 2))) X.ω ((mersenne (p' + 2) + 1) / 4) +
      HPow.hPow (α := X (mersenne (p' + 2))) X.ωb ((mersenne (p' + 2) + 1) / 4) =
    0
⊢ (HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ω (HPow.hPow (α := ℕ) 2 p') +
        HPow.hPow (α := X (HPow.hPow (α := ℕ) 2 (p' + 2) - 1)) X.ωb (HPow.hPow (α := ℕ) 2 p')).1 =
    0
have this₁ : HPow.hPow (α := X (mersenne (p' + 2))) X.ω (HPow.hPow (α := ℕ) 2 p') +
    HPow.hPow (α := X (mersenne (p' + 2))) X.ωb (HPow.hPow (α := ℕ) 2 p') =
  0
Tactic: rw [succ_mersenne, pow_add, show 2 ^ 2 = 4 by norm_num, mul_div_cancel_right₀ _ (by norm_num)]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p : ℕ
hp : 2 ≤ p
n : ℕ
h : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) (n + 1)) : ℤ) = sMod p (n + 1)
have this : HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (α := ℕ) 2 p
Tactic: have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p k : ℕ
hp : 2 ≤ p
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) k) : ℤ) = sMod p k
have zero : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) 0) : ℤ) = sMod p 0
Tactic: induction k with
  | zero => grind [sModNat, sMod]
  | succ =>
    have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp
    grind [sModNat, sMod, Int.emod_eq_add_self_emod]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p k : ℕ
hp : 2 ≤ p
zero : (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) 0) : ℤ) = sMod p 0
⊢ (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) k) : ℤ) = sMod p k
have succ : ∀ (n : ℕ),
  (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) n) : ℤ) = sMod p n →
    (↑(sModNat (HPow.hPow (α := ℕ) 2 p - 1) (n + 1)) : ℤ) = sMod p (n + 1)
Tactic: induction k with
  | zero => grind [sModNat, sMod]
  | succ =>
    have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp
    grind [sModNat, sMod, Int.emod_eq_add_self_emod]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
ih : sModNat_aux (4 % q) q k = sModNat q k
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
have succ : (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q = sModNat q (k + 1)
Tactic: rw [sModNat_aux, ih, sModNat, ← ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
ih : sModNat_aux (4 % q) q k = sModNat q k
succ : (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q = sModNat q (k + 1)
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
have succ₁ : (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q = sModNat q (k + 1)
Tactic: rw [sModNat_aux, ih, sModNat, ← ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
ih : sModNat_aux (4 % q) q k = sModNat q k
succ : (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q = sModNat q (k + 1)
succ₁ : (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q = sModNat q (k + 1)
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
have succ₂ : (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q = (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q
Tactic: rw [sModNat_aux, ih, sModNat, ← ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
ih : sModNat_aux (4 % q) q k = sModNat q k
succ : (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q = sModNat q (k + 1)
succ₁ : (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q = sModNat q (k + 1)
succ₂ : (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q = (HPow.hPow (β := ℕ) (sModNat q k) 2 + (q - 2)) % q
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
have succ₃ : (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q =
  (HPow.hPow (β := ℕ) (sModNat_aux (4 % q) q k) 2 + (q - 2)) % q
Tactic: rw [sModNat_aux, ih, sModNat, ← ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
⊢ sModNat_aux (4 % q) q k = sModNat q k
have zero : sModNat_aux (4 % q) q 0 = sModNat q 0
Tactic: induction k with
  | zero => rfl
  | succ k ih => rw [sModNat_aux, ih, sModNat, ← ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q k : ℕ
zero : sModNat_aux (4 % q) q 0 = sModNat q 0
⊢ sModNat_aux (4 % q) q k = sModNat q k
have succ : ∀ (k : ℕ) (ih : sModNat_aux (4 % q) q k = sModNat q k), sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
Tactic: induction k with
  | zero => rfl
  | succ k ih => rw [sModNat_aux, ih, sModNat, ← ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k
b : ℕ
⊢ sModNatTR.go q (k + 1) b = sModNat_aux b q (k + 1)
have succ : sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
Tactic: rw [sModNatTR.go, ih, sModNat_aux]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q b k : ℕ
ih : sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q (k + 1) =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
have succ : (HPow.hPow (β := ℕ) (sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k) 2 + (q - 2)) % q =
  (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
Tactic: rw [sModNat_aux, ih, sModNat_aux]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q b k : ℕ
ih : sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
succ :
  (HPow.hPow (β := ℕ) (sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k) 2 + (q - 2)) % q =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q (k + 1) =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
have succ₁ : (HPow.hPow (β := ℕ) ((HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q) 2 + (q - 2)) % q =
  (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
Tactic: rw [sModNat_aux, ih, sModNat_aux]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q b k : ℕ
ih : sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
succ :
  (HPow.hPow (β := ℕ) (sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k) 2 + (q - 2)) % q =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
succ₁ :
  (HPow.hPow (β := ℕ) ((HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q) 2 + (q - 2)) % q =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q (k + 1) =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
have succ₂ : (HPow.hPow (β := ℕ) ((HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q) 2 + (q - 2)) % q =
  (HPow.hPow (β := ℕ) ((HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q) 2 + (q - 2)) % q
Tactic: rw [sModNat_aux, ih, sModNat_aux]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q k b : ℕ
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
have succ : sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q 0 = (HPow.hPow (β := ℕ) (sModNat_aux b q 0) 2 + (q - 2)) % q
Tactic: induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNat_aux, ih, sModNat_aux]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i q k b : ℕ
succ :
  sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q 0 = (HPow.hPow (β := ℕ) (sModNat_aux b q 0) 2 + (q - 2)) % q
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
have succ₁ : ∀ (k : ℕ)
  (ih :
    sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k =
      (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q),
  sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q (k + 1) =
    (HPow.hPow (β := ℕ) (sModNat_aux b q (k + 1)) 2 + (q - 2)) % q
Tactic: induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNat_aux, ih, sModNat_aux]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i b q k : ℕ
⊢ sModNatTR.go q k b = sModNat_aux b q k
have zero : ∀ (b : ℕ), sModNatTR.go q 0 b = sModNat_aux b q 0
Tactic: induction k generalizing b with
    | zero => rfl
    | succ k ih =>
      rw [sModNatTR.go, ih, sModNat_aux]
      clear ih
      induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNat_aux, ih, sModNat_aux]
Cleared hypotheses: b, k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q_1 i b q k : ℕ
zero : ∀ (b : ℕ), sModNatTR.go q 0 b = sModNat_aux b q 0
⊢ sModNatTR.go q k b = sModNat_aux b q k
have succ : ∀ (k : ℕ) (ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k) (b : ℕ),
  sModNatTR.go q (k + 1) b = sModNat_aux b q (k + 1)
Tactic: induction k generalizing b with
    | zero => rfl
    | succ k ih =>
      rw [sModNatTR.go, ih, sModNat_aux]
      clear ih
      induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNat_aux, ih, sModNat_aux]
Cleared hypotheses: b, k
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
⊢ sModNatTR q i = sModNat q i
have rw : sModNatTR.go q i (4 % q) = sModNat q i
Tactic: rw [sModNatTR, helper, sModNat_aux_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
rw : sModNatTR.go q i (4 % q) = sModNat q i
⊢ sModNatTR q i = sModNat q i
have rw₁ : sModNat_aux (4 % q) q i = sModNat q i
Tactic: rw [sModNatTR, helper, sModNat_aux_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
rw : sModNatTR.go q i (4 % q) = sModNat q i
rw₁ : sModNat_aux (4 % q) q i = sModNat q i
⊢ sModNatTR q i = sModNat q i
have rw₂ : sModNat q i = sModNat q i
Tactic: rw [sModNatTR, helper, sModNat_aux_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
⊢ LucasLehmerTest p
have hp₁ : 1 < p
Tactic: rw [Nat.blt_eq] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
⊢ LucasLehmerTest p
have rw : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat, h]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p
have hp₁ : 1 < p
Tactic: rw [Nat.blt_eq] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (hypothesis)
Goal:
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p
have h₁ : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) ≠ 0
Tactic: rw [Nat.ble_eq, Nat.succ_le_iff, Nat.pos_iff_ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) ≠ 0
⊢ ¬LucasLehmerTest p
have rw : ¬Eq (α := ℤ) (↑(sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) : ℤ) 0
Tactic: rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
n k : ℕ
⊢ 1 * (k / HPow.hPow (α := ℕ) 2 n) + k % HPow.hPow (α := ℕ) 2 n =
    k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n
have rw : k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n = k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 0 ∧ p ≠ 1
have left : p ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
left : p ≠ 0
⊢ p ≠ 0 ∧ p ≠ 1
have right : p ≠ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ Nat.Prime p
have h : p ≠ 0 ∧ p ≠ 1
Tactic: have h : p ≠ 0 ∧ p ≠ 1 := by
    constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
⊢ Nat.Prime p
have hp1 : 1 < p
Tactic: have hp1 : 1 < p := Nat.one_lt_iff_ne_zero_and_ne_one.2 h
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
⊢ Nat.Prime p
have this : NeZero p
Tactic: have : NeZero p := ⟨h.1⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Nat.Prime p
have rw : Fintype.card (ZMod p)ˣ = p - 1
Tactic: rw [Nat.prime_iff_card_units]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1
have apply : p - 1 ≤ Fintype.card (ZMod p)ˣ
Tactic: apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ a * a ^ (p - Nat.succ 1) = 1
have rwa : a ^ (p - Nat.succ 1 + 1) = 1
Tactic: rwa [← pow_succ', tsub_add_eq_add_tsub hp1]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
rwa : a ^ (p - Nat.succ 1 + 1) = 1
n : ℕ
⊢ a * a ^ (p - Nat.succ 1) = 1
have rwa₁ : a ^ (p + 1 - Nat.succ 1) = 1
Tactic: rwa [← pow_succ', tsub_add_eq_add_tsub hp1]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
hP : Nat.Prime p
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have this : Fact (Nat.Prime p)
Tactic: have : Fact p.Prime := ⟨hP⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have obtain : ∀ (g : (ZMod p)ˣ) (hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x),
  ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := (ZMod p)ˣ)
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
⊢ orderOf g = p - 1
have rwa : Nat.card (ZMod p)ˣ = p - 1
Tactic: rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
      ← Nat.prime_iff_card_units]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
rwa : Nat.card (ZMod p)ˣ = p - 1
⊢ orderOf g = p - 1
have rwa₁ : Fintype.card (ZMod p)ˣ = p - 1
Tactic: rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
      ← Nat.prime_iff_card_units]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have h1 : orderOf g = p - 1
Tactic: have h1 : orderOf g = p - 1 := by
    rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
      ← Nat.prime_iff_card_units]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
h1 : orderOf g = p - 1
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have h2 : 0 < p - 1
Tactic: have h2 := tsub_pos_iff_lt.2 hP.one_lt
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
h1 : orderOf g = p - 1
h2 : 0 < p - 1
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have h1₁ : HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) (p - 1) = 1 ∧
  ∀ m < p - 1, 0 < m → HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) m ≠ 1
Tactic: rw [← orderOf_injective (Units.coeHom _) Units.val_injective _, orderOf_eq_iff h2] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (goal)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
h1 :
  HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) (p - 1) = 1 ∧
    ∀ m < p - 1, 0 < m → HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) m ≠ 1
h2 : 0 < p - 1
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
have refine : ∀ (q : ℕ) (hq : Nat.Prime q) (hqd : q ∣ p - 1), (↑g : ZMod p) ^ ((p - 1) / q) ≠ 1
Tactic: refine ⟨g, h1.1, fun q hq hqd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LucasPrimality (hypothesis)
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), Membership.mem (γ := Subgroup (ZMod p)ˣ) (Subgroup.zpowers g) x
h1 :
  HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) (p - 1) = 1 ∧
    ∀ m < p - 1, 0 < m → HPow.hPow (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) g : ZMod p) m ≠ 1
h2 : 0 < p - 1
q : ℕ
hq : Nat.Prime q
hqd : q ∣ p - 1
⊢ (↑g : ZMod p) ^ ((p - 1) / q) ≠ 1
have hq₁ : 1 < q
Tactic: replace hq := hq.one_lt
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ (map (castRingHom ℂ) p).mahlerMeasure
have apply : 1 ≤ ‖(map (castRingHom ℂ) p).leadingCoeff‖
Tactic: apply le_trans _ (p.map (castRingHom ℂ)).leadingCoeff_le_mahlerMeasure
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ ‖(map (castRingHom ℂ) p).leadingCoeff‖
have rw : 1 ≤ norm (E := ℂ) (↑p.leadingCoeff : ℂ)
Tactic: rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ norm (E := ℂ) (↑p.leadingCoeff : ℂ)
have norm_cast : 1 ≤ |p.leadingCoeff|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (boxPoly n B₁ B₂).ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
have trans : (boxPoly n B₁ B₂).ncard =
  (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
Tactic: trans Set.ncard (α := Fin (n + 1) → ℤ) (Finset.Icc (⌈B₁ ·⌉) (⌊B₂ ·⌋))
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
trans :
  (boxPoly n B₁ B₂).ncard =
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
⊢ (boxPoly n B₁ B₂).ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
have trans₁ : (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard =
  ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
Tactic: trans Set.ncard (α := Fin (n + 1) → ℤ) (Finset.Icc (⌈B₁ ·⌉) (⌊B₂ ·⌋))
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (boxPoly n B₁ B₂).ncard =
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
have refine_1 : ∀ (p : (↑(boxPoly n B₁ B₂) : Type)),
  Membership.mem (α := Fin (n + 1) → ℤ)
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ))
    ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X]) : Fin (n + 1) → ℤ)
Tactic: refine Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
refine_1 :
  ∀ (p : (↑(boxPoly n B₁ B₂) : Type)),
    Membership.mem (α := Fin (n + 1) → ℤ)
      (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ))
      ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X]) : Fin (n + 1) → ℤ)
⊢ (boxPoly n B₁ B₂).ncard =
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
have refine_2 : ∀
  (p :
    (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) : Type)),
  Membership.mem (α := ℤ[X]) (boxPoly n B₁ B₂)
    ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ) : ℤ[X])
Tactic: refine Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩