awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LucasLehmer
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
succ₃ 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
⊢ sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)

Tactic:
rw [sModNat_aux, ih, sModNat, ← ih]

Premises used: LucasLehmer.norm_num_ext.sModNat, LucasLehmer.norm_num_ext.sModNat_aux
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q k : ℕ
zero : sModNat_aux (4 % q) q 0 = sModNat q 0
succ : ∀ (k : ℕ) (ih : sModNat_aux (4 % q) q k = sModNat q k), sModNat_aux (4 % q) q (k + 1) = sModNat q (k + 1)
⊢ sModNat_aux (4 % q) q k = sModNat q k

Tactic:
induction k with
  | zero => rfl
  | succ k ih => rw [sModNat_aux, ih, sModNat, ← ih]

Premises used: LucasLehmer.norm_num_ext.sModNat, LucasLehmer.norm_num_ext.sModNat_aux
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q_1 i q b : ℕ
⊢ sModNatTR.go q 0 b = sModNat_aux b q 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q_1 i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k
b : ℕ
succ :
  sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q
⊢ sModNatTR.go q (k + 1) b = sModNat_aux b q (k + 1)

Tactic:
rw [sModNatTR.go, ih, sModNat_aux]

Premises used: LucasLehmer.norm_num_ext.sModNat_aux, _private.0.LucasLehmer.norm_num_ext.sModNatTR.go
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q_1 i q b : ℕ
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q 0 = (HPow.hPow (β := ℕ) (sModNat_aux b q 0) 2 + (q - 2)) % q

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
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
succ₂ 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
⊢ 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:
rw [sModNat_aux, ih, sModNat_aux]

Premises used: LucasLehmer.norm_num_ext.sModNat_aux
-- Module: Mathlib.NumberTheory.LucasLehmer
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
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
⊢ sModNat_aux ((HPow.hPow (β := ℕ) b 2 + (q - 2)) % q) q k = (HPow.hPow (β := ℕ) (sModNat_aux b q k) 2 + (q - 2)) % q

Tactic:
induction k with
      | zero => rfl
      | succ k ih =>
        rw [sModNat_aux, ih, sModNat_aux]

Premises used: LucasLehmer.norm_num_ext.sModNat_aux
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q_1 i b q k : ℕ
zero : ∀ (b : ℕ), sModNatTR.go q 0 b = sModNat_aux b q 0
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)
⊢ sModNatTR.go q k b = sModNat_aux b q k

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]

Premises used: LucasLehmer.norm_num_ext.sModNat_aux, _private.0.LucasLehmer.norm_num_ext.sModNatTR.go
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
q i : ℕ
rw : sModNatTR.go q i (4 % q) = sModNat q i
rw₁ : sModNat_aux (4 % q) q i = sModNat q i
rw₂ rw₃ : sModNat q i = sModNat q i
⊢ sModNatTR q i = sModNat q i

Tactic:
rw [sModNatTR, helper, sModNat_aux_eq]

Premises used: LucasLehmer.norm_num_ext.sModNat_aux_eq, LucasLehmer.norm_num_ext.sModNatTR
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
⊢ 1 < p

Tactic:
rw [Nat.blt_eq] at hp

Premises used: Nat.blt_eq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
hp₁ : 1 < p
⊢ sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0

Tactic:
rw [Nat.blt_eq] at hp

Premises used: Nat.blt_eq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
rw : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ LucasLehmerTest p

Tactic:
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat, h]

Premises used: LucasLehmer.LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero, LucasLehmer.norm_num_ext.sModNat_eq_sMod, LucasLehmer.norm_num_ext.sModNatTR_eq_sModNat
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) = 0
⊢ Eq (α := ℤ) (↑0 : ℤ) 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true
⊢ 1 < p

Tactic:
rw [Nat.blt_eq] at hp

Premises used: Nat.blt_eq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true
hp₁ : 1 < p
⊢ Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true

Tactic:
rw [Nat.blt_eq] at hp

Premises used: Nat.blt_eq
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) = true
⊢ 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

Premises used: Nat.pos_iff_ne_zero, Nat.ble_eq, Nat.succ_le_iff
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) ≠ 0
rw : ¬Eq (α := ℤ) (↑(sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) : ℤ) 0
⊢ ¬LucasLehmerTest p

Tactic:
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat]

Premises used: LucasLehmer.LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero, LucasLehmer.norm_num_ext.sModNat_eq_sMod, LucasLehmer.norm_num_ext.sModNatTR_eq_sModNat
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
hp : 1 < p
h : sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2) ≠ 0
⊢ ¬Eq (α := ℤ) (↑(sModNatTR (HPow.hPow (α := ℕ) 2 p - 1) (p - 2)) : ℤ) 0

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n k : ℕ
rw rw₁ :
  k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n = k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n
⊢ 1 * (k / HPow.hPow (α := ℕ) 2 n) + k % HPow.hPow (α := ℕ) 2 n =
    k / HPow.hPow (α := ℕ) 2 n + k % HPow.hPow (α := ℕ) 2 n

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.NumberTheory.LucasPrimality
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
right : p ≠ 1
⊢ p ≠ 0 ∧ p ≠ 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
a : ZMod 0
ha : a ^ HSub.hSub (α := ℕ) 0 1 = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ HSub.hSub (α := ℕ) 0 1 → a ^ (HSub.hSub (α := ℕ) 0 1 / q) ≠ 1
⊢ False

Tactic:
hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Premises used: dvd_zero, Nat.prime_two, pow_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
a : ZMod 0
ha : a ^ HSub.hSub (α := ℕ) 0 1 = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ HSub.hSub (α := ℕ) 0 1 → a ^ (HSub.hSub (α := ℕ) 0 1 / q) ≠ 1
⊢ False

Tactic:
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Premises used: dvd_zero, Nat.prime_two, pow_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
a : ZMod 1
ha : a ^ HSub.hSub (α := ℕ) 1 1 = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ HSub.hSub (α := ℕ) 1 1 → a ^ (HSub.hSub (α := ℕ) 1 1 / q) ≠ 1
⊢ False

Tactic:
hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Premises used: dvd_zero, Nat.prime_two, pow_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
a : ZMod 1
ha : a ^ HSub.hSub (α := ℕ) 1 1 = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ HSub.hSub (α := ℕ) 1 1 → a ^ (HSub.hSub (α := ℕ) 1 1 / q) ≠ 1
⊢ False

Tactic:
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Premises used: dvd_zero, Nat.prime_two, pow_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LucasPrimality
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

Tactic:
have h : p ≠ 0 ∧ p ≠ 1 := by
    constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
-- Module: Mathlib.NumberTheory.LucasPrimality
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
⊢ 1 < p

Tactic:
have hp1 : 1 < p := Nat.one_lt_iff_ne_zero_and_ne_one.2 h
-- Module: Mathlib.NumberTheory.LucasPrimality
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
⊢ NeZero p

Tactic:
have : NeZero p := ⟨h.1⟩
-- Module: Mathlib.NumberTheory.LucasPrimality
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
rw : Fintype.card (ZMod p)ˣ = p - 1
⊢ Nat.Prime p

Tactic:
rw [Nat.prime_iff_card_units]

Premises used: Nat.prime_iff_card_units
-- Module: Mathlib.NumberTheory.LucasPrimality
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
apply : p - 1 ≤ Fintype.card (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm

Premises used: Nat.card_units_zmod_lt_sub_one, LE.le.antisymm
-- Module: Mathlib.NumberTheory.LucasPrimality
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 : ℕ
rwa₁ rwa₂ rwa₃ rwa₄ : a ^ (p + 1 - Nat.succ 1) = 1
⊢ a * a ^ (p - Nat.succ 1) = 1

Tactic:
rwa [← pow_succ', tsub_add_eq_add_tsub hp1]

Premises used: tsub_add_eq_add_tsub, pow_succ'
-- Module: Mathlib.NumberTheory.LucasPrimality
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' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - Nat.succ 1)) ⋯
⊢ p - 1 = orderOf a

Tactic:
(orderOf_eq_of_pow_and_pow_div_prime (tsub_pos_of_lt hp1) ha hd).symm

Premises used: orderOf_eq_of_pow_and_pow_div_prime, Eq.symm, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.LucasPrimality
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' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - Nat.succ 1)) ⋯
⊢ orderOf a = orderOf a'

Tactic:
orderOf_injective (Units.coeHom _) Units.val_injective a'

Premises used: Units.coeHom, Units.val_injective, orderOf_injective
-- Module: Mathlib.NumberTheory.LucasPrimality
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' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - Nat.succ 1)) ⋯
⊢ orderOf a' ≤ Fintype.card (ZMod p)ˣ

Tactic:
orderOf_le_card_univ

Premises used: orderOf_le_card_univ
-- Module: Mathlib.NumberTheory.LucasPrimality
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' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - Nat.succ 1)) ⋯
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ

Tactic:
calc p - 1 = orderOf a := (orderOf_eq_of_pow_and_pow_div_prime (tsub_pos_of_lt hp1) ha hd).symm
    _ = orderOf a' := orderOf_injective (Units.coeHom _) Units.val_injective a'
    _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ

Premises used: Units.coeHom, orderOf_le_card_univ, orderOf_eq_of_pow_and_pow_div_prime, Units, Fintype.card, ZMod, orderOf, Units.val_injective, Eq.symm, orderOf_injective, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
p : ℕ
hP : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨hP⟩
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
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
⊢ ∃ (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)ˣ)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.NumberTheory.LucasPrimality
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
rwa₁ : Fintype.card (ZMod p)ˣ = p - 1
rwa₂ rwa₃ rwa₄ rwa₅ : Nat.Prime p
⊢ orderOf g = p - 1

Tactic:
rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card,
      ← Nat.prime_iff_card_units]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.prime_iff_card_units, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.LucasPrimality
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

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]
-- Module: Mathlib.NumberTheory.LucasPrimality
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
⊢ 0 < p - 1

Tactic:
have h2 := tsub_pos_iff_lt.2 hP.one_lt
-- Module: Mathlib.NumberTheory.LucasPrimality
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
⊢ 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

Premises used: Units.coeHom, orderOf_eq_iff, Units.val_injective, orderOf_injective
-- Module: Mathlib.NumberTheory.LucasPrimality
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
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
⊢ 0 < p - 1

Tactic:
rw [← orderOf_injective (Units.coeHom _) Units.val_injective _, orderOf_eq_iff h2] at h1

Premises used: Units.coeHom, orderOf_eq_iff, Units.val_injective, orderOf_injective
-- Module: Mathlib.NumberTheory.LucasPrimality
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

Tactic:
⟨g, h1.1, fun q hq hqd ↦ ?_⟩

Premises used: Units.val, And.left, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LucasPrimality
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
refine : ∀ (q : ℕ) (hq : Nat.Prime q) (hqd : q ∣ p - 1), (↑g : ZMod p) ^ ((p - 1) / q) ≠ 1
⊢ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

Tactic:
refine ⟨g, h1.1, fun q hq hqd ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LucasPrimality
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
⊢ 1 < q

Tactic:
replace hq := hq.one_lt
-- Module: Mathlib.NumberTheory.LucasPrimality
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 : ℕ
hqd : q ∣ p - 1
hq : 1 < q
⊢ (↑g : ZMod p) ^ ((p - 1) / q) ≠ 1

Tactic:
h1.2 _ (Nat.div_lt_self h2 hq) (Nat.div_pos (Nat.le_of_dvd h2 hqd) (zero_lt_one.trans hq))

Premises used: Nat.div_lt_self, zero_lt_one, And.right, LT.lt.trans, Nat.le_of_dvd, Nat.div_pos
-- Module: Mathlib.NumberTheory.LucasPrimality
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 : ℕ
hqd : q ∣ p - 1
hq : 1 < q
⊢ (↑g : ZMod p) ^ ((p - 1) / q) ≠ 1

Tactic:
exact h1.2 _ (Nat.div_lt_self h2 hq) (Nat.div_pos (Nat.le_of_dvd h2 hqd) (zero_lt_one.trans hq))

Premises used: Nat.div_lt_self, zero_lt_one, And.right, LT.lt.trans, Nat.le_of_dvd, Nat.div_pos
-- Module: Mathlib.NumberTheory.LucasPrimality
Goal:
p : ℕ
⊢ Nat.Prime p ↔ ∃ (a : ZMod p), a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

Tactic:
⟨reverse_lucas_primality p, fun ⟨a, ⟨ha, hb⟩⟩ ↦ lucas_primality p a ha hb⟩

Premises used: Nat.Prime, lucas_primality, Iff.intro, reverse_lucas_primality, _private.0.lucas_primality_iff.match_1
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
hp : p ≠ 0
apply : 1 ≤ ‖(map (castRingHom ℂ) p).leadingCoeff‖
⊢ 1 ≤ (map (castRingHom ℂ) p).mahlerMeasure

Tactic:
apply le_trans _ (p.map (castRingHom ℂ)).leadingCoeff_le_mahlerMeasure

Premises used: Int.castRingHom, Polynomial.leadingCoeff_le_mahlerMeasure, Polynomial.map, Complex, le_trans
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
hp : p ≠ 0
rw : 1 ≤ norm (E := ℂ) (↑p.leadingCoeff : ℂ)
⊢ 1 ≤ ‖(map (castRingHom ℂ) p).leadingCoeff‖

Tactic:
rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast]

Premises used: eq_intCast, Polynomial.leadingCoeff_map_of_injective, Int.castRingHom, Complex, RingHom.injective_int
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
hp : p ≠ 0
norm_cast : 1 ≤ |p.leadingCoeff|
⊢ 1 ≤ norm (E := ℂ) (↑p.leadingCoeff : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ |p.leadingCoeff|

Tactic:
one_le_abs <| leadingCoeff_ne_zero.mpr hp

Premises used: Iff.mpr, Int.one_le_abs, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ |p.leadingCoeff|

Tactic:
exact one_le_abs <| leadingCoeff_ne_zero.mpr hp

Premises used: Iff.mpr, Int.one_le_abs, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.NumberTheory.MahlerMeasure
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
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
⊢ (boxPoly n B₁ B₂).ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Tactic:
trans Set.ncard (α := Fin (n + 1) → ℤ) (Finset.Icc (⌈B₁ ·⌉) (⌊B₂ ·⌋))

Premises used: Int.floor, Finset.Icc, SetLike.coe, Int.ceil, Set.ncard
-- Module: Mathlib.NumberTheory.MahlerMeasure
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

Tactic:
Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩

Premises used: Equiv.mk, Polynomial.toFn, Subtype.mk, HAdd.hAdd, Set.ncard_congr', OfNat.ofNat, Subtype.val, DFunLike.coe, Polynomial.ofFn