awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₂ : HPow.hPow (α := ℕ) 2 (2 * HPow.hPow (α := ℕ) 2 n) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw₃ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₂ : HPow.hPow (α := ℕ) 2 (2 * HPow.hPow (α := ℕ) 2 n) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw₄ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₂ : HPow.hPow (α := ℕ) 2 (2 * HPow.hPow (α := ℕ) 2 n) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₄ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw₅ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
⊢ 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 ≤
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2
have this : 0 ≤ 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
Tactic: have : 0 ≤ 1 + 2 ^ (2 ^ n * 4) := le_add_left _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
this : 0 ≤ 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
⊢ 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 ≤
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2
have ring_nf : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 ≤
  1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 2)) + 1 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2 -
      2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2
have rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 2)) + 1 + 2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) -
    2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) =
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2 -
    2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2
Tactic: rw [← add_sub_self_right (2 ^ 2 ^ (n + 2) + 1) <| 2 * 2 ^ 2 ^ (n + 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
⊢ (↑(n + 2).fermatNumber : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1).fermatNumber : ℤ) 2 -
      2 * HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑n.fermatNumber : ℤ) 1) 2
have rw : HSub.hSub (α := ℤ) (↑(HPow.hPow (β := ℕ) (n + 1).fermatNumber 2) : ℤ)
    (↑(2 * HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2) : ℤ) =
  HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1).fermatNumber : ℤ) 2 -
    2 * HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑n.fermatNumber : ℤ) 1) 2
Tactic: rw [Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq,
    Nat.cast_sub <| two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq n]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
m n : ℕ
hmn : m ≠ n
⊢ m.fermatNumber.Coprime n.fermatNumber
have inr : ∀ (this : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber) (hmn' : ¬m < n),
  m.fermatNumber.Coprime n.fermatNumber
Tactic: wlog hmn' : m < n
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
m n : ℕ
hmn : m ≠ n
inr :
  ∀ (this : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber) (hmn' : ¬m < n),
    m.fermatNumber.Coprime n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber
have wlog : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber
Tactic: wlog hmn' : m < n
Cleared hypotheses: m, n, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber
have h_n : d ∣ n.fermatNumber
Tactic: have h_n : d ∣ fermatNumber n := gcd_dvd_right ..
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber
have h_m : d ∣ 2
Tactic: have h_m : d ∣ 2 := (Nat.dvd_add_right <| (gcd_dvd_left _ _).trans <| dvd_prod_of_mem _
    <| mem_range.mpr hmn').mp <| fermatNumber_eq_prod_add_two _ ▸ h_n
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
⊢ m.fermatNumber.Coprime n.fermatNumber
have refine : ∀ (h_two : d = 2), False
Tactic: refine ((dvd_prime prime_two).mp h_m).resolve_right fun h_two ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a n : ℕ
ha : 1 < a
hn : n ≠ 0
hP : Prime (a ^ n + 1)
⊢ ∃ (m : ℕ), n = HPow.hPow (α := ℕ) 2 m
have obtain : ∀ (k m : ℕ) (hm : Odd m) (hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0) (hP : Prime (a ^ (HPow.hPow (α := ℕ) 2 k * m) + 1)),
  ∃ (m_1 : ℕ), HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 m_1
Tactic: obtain ⟨k, m, hm, rfl⟩ := exists_eq_two_pow_mul_odd hn
Cleared hypotheses: n, hn, hP
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime (a ^ (HPow.hPow (α := ℕ) 2 k * m) + 1)
⊢ ∃ (m_1 : ℕ), HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 m_1
have hP₁ : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
Tactic: rw [pow_mul] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
⊢ ∃ (m_1 : ℕ), HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 m_1
have h : HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
Tactic: use k
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
⊢ HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
have ha₁ : 1 < a ^ HPow.hPow (α := ℕ) 2 k
Tactic: replace ha : 1 < a ^ 2 ^ k := one_lt_pow (pow_ne_zero k two_ne_zero) ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
a k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
ha : 1 < a ^ HPow.hPow (α := ℕ) 2 k
h : a ^ HPow.hPow (α := ℕ) 2 k + 1 ∣ (a ^ HPow.hPow (α := ℕ) 2 k) ^ m + HPow.hPow (α := ℕ) 1 m := ⋯
⊢ HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
have h₁ : m = 1
Tactic: rw [one_pow, hP.dvd_iff_eq (Nat.lt_add_right 1 ha).ne', add_left_inj, pow_eq_self_iff ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
ha : 1 < a ^ HPow.hPow (α := ℕ) 2 k
h : m = 1
⊢ HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
have h₁ : HPow.hPow (α := ℕ) 2 k * 1 = HPow.hPow (α := ℕ) 2 k
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
a k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
ha : 1 < a ^ HPow.hPow (α := ℕ) 2 k
h : m = 1
h₁ : HPow.hPow (α := ℕ) 2 k * 1 = HPow.hPow (α := ℕ) 2 k
⊢ HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
have h₂ : HPow.hPow (α := ℕ) 2 k = HPow.hPow (α := ℕ) 2 k
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
⊢ Prime n.fermatNumber
have this : Fact (2 < n.fermatNumber)
Tactic: have := Fact.mk (two_lt_fermatNumber n)
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
⊢ Prime n.fermatNumber
have key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
Tactic: have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
⊢ Prime n.fermatNumber
have ha : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
    (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
  1
Tactic: apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
⊢ Prime n.fermatNumber
have hd : ∀ (q : ℕ),
  Prime q →
    q ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1 →
      HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
          ((HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / q) ≠
        1
Tactic: apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
    (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
  1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₁ : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
    (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
  1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₂ : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
    (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
  1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
ha₂ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
    1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₃ : HPow.hPow (β := ℕ)
    (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
    2 =
  1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
ha₂ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
    1
ha₃ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₄ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₅ : HPow.hPow (β := ℕ)
    (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
    2 =
  1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
ha₂ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
    1
ha₃ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₄ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₅ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₆ : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) (β := ℕ) (-1) 2 = 1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
ha₂ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
    1
ha₃ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₄ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₅ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₆ : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) (β := ℕ) (-1) 2 = 1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
have ha₇ : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 1 1
Tactic: rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
⊢ Prime n.fermatNumber
have h₁ : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
Tactic: apply pepin_primality
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
⊢ HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
have h₁ : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) =
  HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
⊢ HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) =
    HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2)
have h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2
have h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / 2
Tactic: rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / 2
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2
have h₂ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) / 2
Tactic: rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / 2
h₂ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) / 2
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2
have h₃ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)
Tactic: rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]
-- 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
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1
have this : Fact (2 < p)
Tactic: have : Fact (2 < p) := Fact.mk (lt_of_le_of_ne hp.two_le hp2.symm)
-- 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 : Fact (2 < p)
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1
have this₁ : Fact (Prime p)
Tactic: have : Fact p.Prime := Fact.mk hp
-- 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)
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
have rw : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
Tactic: rw [eq_neg_iff_add_eq_zero]
-- 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)
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1
have ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
Tactic: have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
    rw [eq_neg_iff_add_eq_zero]
    exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd