awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False
have ha1₁ : Eq (α := ZMod p) 1 0
Tactic: rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
Cleared hypotheses: ha1, h
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1
have ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
Tactic: have ha0 : (a : ZMod p) ≠ 0 := by
    intro h
    rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
    exact one_ne_zero ha1
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)
have hnot : ¬HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hnot : ¬HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = 1
⊢ orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)
have hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ ¬HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = 1
have hnot : ¬Eq (α := ZMod p) (-1) 1
Tactic: rw [ha1]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
have hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n * 2) = 1
Tactic: rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n * 2) = 1
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
have hfin₁ : HPow.hPow (β := ℕ) (HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n)) 2 = 1
Tactic: rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n * 2) = 1
hfin₁ : HPow.hPow (β := ℕ) (HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n)) 2 = 1
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
have hfin₂ : HPow.hPow (α := ZMod p) (β := ℕ) (-1) 2 = 1
Tactic: rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n * 2) = 1
hfin₁ : HPow.hPow (β := ℕ) (HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n)) 2 = 1
hfin₂ : HPow.hPow (α := ZMod p) (β := ℕ) (-1) 2 = 1
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
have hfin₃ : Eq (α := ZMod p) 1 1
Tactic: rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1
have ha : orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: have ha : orderOf (a : ZMod p) = 2 ^ (n + 1) := by
    apply orderOf_eq_prime_pow
    · rw [ha1]
      exact neg_one_ne_one
    · rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
have this : Fact (Prime p)
Tactic: have : Fact p.Prime := Fact.mk hp
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
have hp2 : p ≠ 2
Tactic: have hp2 : p ≠ 2 := by
    exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ p % 8 = 1
have obtain : ∀ (k : ℕ) (hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))
  (hpdvd : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ∣ n.fermatNumber)
  (this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))) (hp2 : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ≠ 2),
  (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1) % 8 = 1
Tactic: obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd
Cleared hypotheses: p, hp, hpdvd, this, hp2
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
hn : 1 < n
k : ℕ
hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1)
hpdvd : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ∣ n.fermatNumber
this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))
hp2 : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ≠ 2
⊢ (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1) % 8 = 1
have obtain : ∀ (n : ℕ) (hn : 1 < n + succ 1) (hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1))
  (hpdvd : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber)
  (this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1)))
  (hp2 : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ≠ 2), (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1) % 8 = 1
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
Cleared hypotheses: n, hn, hp, hpdvd, this, hp2
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1)
hpdvd : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1))
hp2 : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1) % 8 = 1
have rw : (k * HPow.hPow (α := ℕ) 2 n % 8 * (HPow.hPow (α := ℕ) 2 (succ 1 + 1) % 8) % 8 + 1) % 8 = 1
Tactic: rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
have hp8 : p % 8 = 1
Tactic: have hp8 : p % 8 = 1 := by
    obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd
    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
    rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]
    simp
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
have obtain : ∀ (a : ZMod p) (ha : 2 = a * a), ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
Tactic: obtain ⟨a, ha⟩ := (exists_sq_eq_two_iff hp2).mpr (Or.inl hp8)
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
have suffices : p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
Tactic: suffices h : p ∣ a.val ^ (2 ^ (n + 1)) + 1 by
    exact pow_pow_add_primeFactors_one_lt hp hp2 h
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
have rw : ∀ (hpdvd : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1) (this : Fact (Prime p)) (hp2 : p ≠ 2)
  (hp8 : p % 8 = 1) (a : ZMod p) (ha : 2 = a * a), p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
Tactic: rw [fermatNumber] at hpdvd
Cleared hypotheses: hpdvd, this, hp2, hp8, a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
have rw : ∀ (this : Fact (Prime p)) (hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0) (hp2 : p ≠ 2)
  (hp8 : p % 8 = 1) (a : ZMod p) (ha : 2 = a * a),
  HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
Tactic: rw [← natCast_eq_zero_iff, Nat.cast_add _ 1, Nat.cast_one, Nat.cast_pow] at hpdvd ⊢
Cleared hypotheses: hpdvd, this, hp2, hp8, a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa₂ : a ^ (2 * HPow.hPow (α := ℕ) 2 n) + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
rwa₂ : a ^ (2 * HPow.hPow (α := ℕ) 2 n) + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa₃ : HPow.hPow (β := ℕ) a 2 ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
rwa₂ : a ^ (2 * HPow.hPow (α := ℕ) 2 n) + 1 = 0
rwa₃ : HPow.hPow (β := ℕ) a 2 ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa₄ : (a * a) ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
rwa₂ : a ^ (2 * HPow.hPow (α := ℕ) 2 n) + 1 = 0
rwa₃ : HPow.hPow (β := ℕ) a 2 ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
rwa₄ : (a * a) ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
have rwa₅ : HPow.hPow (α := ZMod p) 2 (HPow.hPow (α := ℕ) 2 n) + 1 = 0
Tactic: rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
⊢ a = 2 ∧ Prime n
have han1 : 1 < a ^ n
Tactic: have han1 : 1 < a ^ n := tsub_pos_iff_lt.mp hP.pos
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
⊢ a = 2 ∧ Prime n
have hn0 : n ≠ 0
Tactic: have hn0 : n ≠ 0 := fun h ↦ (h ▸ han1).ne' rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
⊢ a = 2 ∧ Prime n
have ha1 : 1 < a
Tactic: have ha1 : 1 < a := (Nat.one_lt_pow_iff hn0).mp han1
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
⊢ a = 2 ∧ Prime n
have ha0 : 0 < a
Tactic: have ha0 : 0 < a := one_pos.trans ha1
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
⊢ a = 2
have contrapose! : ∀ (hn1 : a ≠ 2), n = 1
Tactic: contrapose! hn1
Cleared hypotheses: hn1
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 ∣ a ^ n - HPow.hPow (α := ℕ) 1 n := ⋯
⊢ n = 1
have h₁ : a - 1 = a ^ n - 1
Tactic: rw [one_pow, hP.dvd_iff_eq (mt (Nat.sub_eq_iff_eq_add ha1.le).mp hn1), eq_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
⊢ a = 2 ∧ Prime n
have ha2 : a = 2
Tactic: have ha2 : a = 2 := by
    contrapose! hn1
    let h := Nat.sub_dvd_pow_sub_pow a 1 n
    rw [one_pow, hP.dvd_iff_eq (mt (Nat.sub_eq_iff_eq_add ha1.le).mp hn1), eq_comm] at h
    exact (pow_eq_self_iff ha1).mp (Nat.sub_one_cancel ha0 (pow_pos ha0 n) h).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
ha2 : a = 2
⊢ a = 2 ∧ Prime n
have subst : ∀ (hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)) (han1 : 1 < HPow.hPow (α := ℕ) 2 n) (ha1 : LT.lt (α := ℕ) 1 2)
  (ha0 : LT.lt (α := ℕ) 0 2), Eq (α := ℕ) 2 2 ∧ Prime n
Tactic: subst ha2
Cleared hypotheses: a, hP, han1, ha1, ha0, ha2
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
⊢ Eq (α := ℕ) 2 2 ∧ Prime n
have refine : ∀ (d : ℕ) (hdn : d ∣ n), d = 1 ∨ d = n
Tactic: refine ⟨rfl, Nat.prime_def.mpr ⟨(two_le_iff n).mpr ⟨hn0, hn1⟩, fun d hdn ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
⊢ d = 1 ∨ d = n
have hinj : ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y
Tactic: have hinj : ∀ x y, 2 ^ x - 1 = 2 ^ y - 1 → x = y :=
    fun x y h ↦ Nat.pow_right_injective le_rfl (sub_one_cancel (pow_pos ha0 x) (pow_pos ha0 y) h)
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y
h : HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 d ^ (n / d) - HPow.hPow (α := ℕ) 1 (n / d) := ⋯
⊢ d = 1 ∨ d = n
have h₁ : HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 n - 1
Tactic: rw [one_pow, ← pow_mul, Nat.mul_div_cancel' hdn] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
⊢ n.Coprime b
have pos : ∀ (h₃ : 2 ≤ n), n.Coprime b
Tactic: by_cases h₃ : 2 ≤ n
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
pos : ∀ (h₃ : 2 ≤ n), n.Coprime b
⊢ n.Coprime b
have neg : ∀ (h₃ : ¬2 ≤ n), n.Coprime b
Tactic: by_cases h₃ : 2 ≤ n
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ n.Coprime b
have pos : ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b
Tactic: apply Nat.coprime_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ False
have pos : k ∣ 1
Tactic: apply Nat.Prime.not_dvd_one hk
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ k ∣ 1
have h₄ : k ∣ (k * j) ^ (k * m - 1) - 1
Tactic: replace h := dvd_of_mul_right_dvd h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1
have pos : k ∣ (k * j) ^ (k * m - 1)
Tactic: rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
have pos : k * m - 1 ≠ 0
Tactic: refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b
have neg : Coprime 1 b
Tactic: rw [show n = 1 by lia]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
n b : ℕ
h : 1 ≤ b
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
have this : 1 ≤ b ^ (n - 1)
Tactic: have : 1 ≤ b ^ (n - 1) := one_le_pow₀ h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
have rw : n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
Tactic: rw [Nat.ModEq.comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
have mp : n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
mp : n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
have mpr : 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ 1 ≡ b ^ (n - 1) [MOD n]
have mp : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑(b ^ (n - 1)) : ℤ) (↑1 : ℤ)
Tactic: apply Nat.modEq_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
⊢ n.Coprime b
have hp : n.ProbablePrime b
Tactic: rcases h with ⟨hp, _, hn₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
hp : n.ProbablePrime b
⊢ n.Coprime b
have left : ¬Prime n
Tactic: rcases h with ⟨hp, _, hn₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left : ¬Prime n
⊢ n.Coprime b
have hn₂ : 1 < n
Tactic: rcases h with ⟨hp, _, hn₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n.FermatPsp 1
have refine : n ∣ HPow.hPow (α := ℕ) 1 (n - 1) - 1
Tactic: refine ⟨show n ∣ 1 ^ (n - 1) - 1 from ?_, h₂, h₁⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < (a ^ b - 1) / (a - 1)
have rw : b < ∑ k ∈ Finset.range b, a ^ k
Tactic: rw [← Nat.geomSum_eq ha]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ LT.lt (α := ℕ) (∑ x ∈ Finset.range b, 1) (∑ k ∈ Finset.range b, a ^ k)
have refine : ∃ i ∈ Finset.range b, 1 < a ^ i
Tactic: refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < ∑ k ∈ Finset.range b, a ^ k
have b₁ : b = ∑ x ∈ Finset.range b, 1
Tactic: calc
    b = ∑ _ ∈ Finset.range b, (1 : ℕ) := by simp
    _ < _ := by
      refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using ha⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
b₁ : b = ∑ x ∈ Finset.range b, 1
⊢ b < ∑ k ∈ Finset.range b, a ^ k
have b₂ : LT.lt (α := ℕ) (∑ x ∈ Finset.range b, 1) (∑ k ∈ Finset.range b, a ^ k)
Tactic: calc
    b = ∑ _ ∈ Finset.range b, (1 : ℕ) := by simp
    _ < _ := by
      refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using ha⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 ≤ (a ^ b + 1) / (a + 1)
have rw : 2 * a.succ ≤ a ^ b + 1
Tactic: rw [Nat.le_div_iff_mul_le (Nat.zero_lt_succ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1
have a₁ : Nat.mul 2 a + 1 ≤ a ^ b
Tactic: apply Nat.succ_le_succ