-- Mathlib/NumberTheory/LucasPrimality.lean
theorem lucas_primality (p : ℕ) (a : ZMod p) (ha : a ^ (p - 1) = 1)
    (hd : ∀ q : ℕ, q.Prime → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1) : p.Prime

Proof state:
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 * ?m.1951 = 1

Tactic:
rwa [← pow_succ', tsub_add_eq_add_tsub hp1]

Result:
no goals

Proof state:
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

Tactic:
have : NeZero p := ⟨h.1⟩

Result:
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

Proof state:
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

Tactic:
have h : p ≠ 0 ∧ p ≠ 1 := by
  constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Result:
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

Proof state:
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

Tactic:
have hp1 : 1 < p := Nat.one_lt_iff_ne_zero_and_ne_one.2 h

Result:
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

Proof state:
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:
constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)

Result:
no goals

Proof state:
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

Tactic:
apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm

Result:
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
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ

Proof state:
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
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ

Tactic:
let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a _ (by rwa [← pow_succ', tsub_add_eq_add_tsub hp1])

Result:
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)ˣ

Proof state:
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.ext a'
  _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ

Result:
no goals

Proof state:
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

Tactic:
rw [Nat.prime_iff_card_units]

Result:
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