awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
have nlinarith : HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 →
  HMul.hMul (α := ℤ) 4 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑a : ℤ) +
          (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 * (↑a : ℤ) + 1 - (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1)) +
        (0 - (0 - HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) +
      2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
nlinarith :
  HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑a : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 * (↑a : ℤ) + 1 - (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1)) +
          (0 - (0 - HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) =
      0
⊢ 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
have nlinarith₁ : HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 → GT.gt (α := ℤ) 4 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
nlinarith :
  HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑a : ℤ) +
            (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 * (↑a : ℤ) + 1 - (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1)) +
          (0 - (0 - HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * HSub.hSub (α := ℤ) 2 (↑a : ℤ)) =
      0
nlinarith₁ : HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 → GT.gt (α := ℤ) 4 0
⊢ 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
have nlinarith₂ : HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 → GT.gt (α := ℤ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 3
have rw : HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 2 * a
Tactic: rw [Nat.pow_succ a 2]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ Nat.mul 2 a + 1 ≤ a ^ b
have a₁ : 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
Tactic: calc
    2 * a + 1 ≤ a ^ 2 * a := by nlinarith
    _ = a ^ 3 := by rw [Nat.pow_succ a 2]
    _ ≤ a ^ b := pow_right_mono₀ (Nat.le_of_succ_le ha) hb
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
a₁ : 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
⊢ Nat.mul 2 a + 1 ≤ a ^ b
have a₂ : HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 3
Tactic: calc
    2 * a + 1 ≤ a ^ 2 * a := by nlinarith
    _ = a ^ 3 := by rw [Nat.pow_succ a 2]
    _ ≤ a ^ b := pow_right_mono₀ (Nat.le_of_succ_le ha) hb
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
have q₁ : b - 1 ∣ b ^ p - 1
Tactic: have q₁ : b - 1 ∣ b ^ p - 1 := by simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow b 1 p
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
have q₂ : b + 1 ∣ b ^ p + 1
Tactic: have q₂ : b + 1 ∣ b ^ p + 1 := by simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
have h : b ^ (2 * p) - 1 = (b ^ p - 1) * (b ^ p + 1)
Tactic: convert! Nat.div_mul_div_comm q₁ q₂ using 2
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
h_1 : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
h : b ^ (2 * p) - 1 = (b ^ p - 1) * (b ^ p + 1)
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
have h₁ : HPow.hPow (β := ℕ) b 2 - 1 = (b - 1) * (b + 1)
Tactic: convert! Nat.div_mul_div_comm q₁ q₂ using 2
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p - 1) * (b ^ p + 1)
have h : b ^ (2 * p) - 1 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2
Tactic: rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 = (b - 1) * (b + 1)
have h : HPow.hPow (β := ℕ) b 2 - 1 = (b + 1) * (b - 1)
Tactic: rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
h_1 : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
h : HPow.hPow (β := ℕ) b 2 - 1 = (b + 1) * (b - 1)
⊢ HPow.hPow (β := ℕ) b 2 - 1 = (b - 1) * (b + 1)
have h₁ : HPow.hPow (β := ℕ) b 2 - 1 = HPow.hPow (β := ℕ) b 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2
Tactic: rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))
have rw : b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1)) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))
Tactic: rw [Nat.sub_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1)) = b ^ (2 * p) - (1 + HPow.hPow (β := ℕ) b 2 - 1)
have rw : b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1)) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))
Tactic: rw [Nat.add_sub_assoc hi_bsquared]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - (1 + HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - HPow.hPow (β := ℕ) b 2
have rw : b ^ (2 * p) - HPow.hPow (β := ℕ) b 2 = b ^ (2 * p) - HPow.hPow (β := ℕ) b 2
Tactic: rw [Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - HPow.hPow (β := ℕ) b 2 = b ^ (p * 2) - HPow.hPow (β := ℕ) b 2
have rw : b ^ (p * 2) - HPow.hPow (β := ℕ) b 2 = b ^ (p * 2) - HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ b ^ (p * 2) - HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2
have rw : HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2 = (b ^ p + b) * (b ^ p - b)
have rw : (b ^ p + b) * (b ^ p - b) = (b ^ p + b) * (b ^ p - b)
Tactic: rw [Nat.sq_sub_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)
have rw : (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)
have rw : (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
Tactic: rw [Nat.sub_add_cancel hp]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ (b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
have rw : (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)
have rw : (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have rw : (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)
Tactic: rw [Nat.mul_sub_left_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ (A * B).FermatPsp b
have hA : p < A
Tactic: have hA : p < A := a_id_helper b_ge_two p_gt_two
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
⊢ (A * B).FermatPsp b
have hi_A : 1 < A
Tactic: have hi_A : 1 < A := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
⊢ (A * B).FermatPsp b
have hi_B : 1 < B
Tactic: have hi_B : 1 < B := b_id_helper b_ge_two p_gt_two
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
⊢ (A * B).FermatPsp b
have hi_b : 0 < b
Tactic: have hi_b : 0 < b := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
⊢ 0 < HPow.hPow (β := ℕ) b 2 - 1
have this : HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) b 2
Tactic: have := Nat.pow_le_pow_left b_ge_two 2
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
⊢ (A * B).FermatPsp b
have hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
Tactic: have hi_bsquared : 0 < b ^ 2 - 1 := by
    have := Nat.pow_le_pow_left b_ge_two 2
    lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
⊢ (A * B).FermatPsp b
have hi_bpowtwop : 1 ≤ b ^ (2 * p)
Tactic: have hi_bpowtwop : 1 ≤ b ^ (2 * p) := Nat.one_le_pow (2 * p) b hi_b
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
⊢ (A * B).FermatPsp b
have hi_bpowpsubone : 1 ≤ b ^ (p - 1)
Tactic: have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_b
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
⊢ (A * B).FermatPsp b
have p_odd : Odd p
Tactic: have p_odd : Odd p := p_prime.odd_of_ne_two p_gt_two.ne.symm
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
⊢ (A * B).FermatPsp b
have AB_not_prime : ¬Prime (A * B)
Tactic: have AB_not_prime : ¬Nat.Prime (A * B) := Nat.not_prime_mul hi_A.ne' hi_B.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
⊢ (A * B).FermatPsp b
have AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: have AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1) := AB_id_helper _ _ b_ge_two p_odd
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
⊢ (A * B).FermatPsp b
have hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
Tactic: have hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1 := by
    simpa only [one_pow, pow_mul] using Nat.sub_dvd_pow_sub_pow _ 1 p
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
⊢ (A * B).FermatPsp b
have refine : (A * B).ProbablePrime b
Tactic: refine ⟨?_, AB_not_prime, one_lt_mul'' hi_A hi_B⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have AB_id₁ : A * B * (HPow.hPow (β := ℕ) b 2 - 1) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1) * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: apply_fun fun x => x * (b ^ 2 - 1) at AB_id
Cleared hypotheses: AB_id
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
AB_id :
  A * B * (HPow.hPow (β := ℕ) b 2 - 1) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1) * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have AB_id₁ : A * B * (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1
Tactic: rw [Nat.div_mul_cancel hd] at AB_id
Cleared hypotheses: AB_id
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have AB_id₁ : A * B * (HPow.hPow (β := ℕ) b 2 - 1) - (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: apply_fun fun x => x - (b ^ 2 - 1) at AB_id
Cleared hypotheses: AB_id
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
AB_id :
  A * B * (HPow.hPow (β := ℕ) b 2 - 1) - (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have AB_id₁ : A * B * (HPow.hPow (β := ℕ) b 2 - 1) - 1 * (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: nth_rw 2 [← one_mul (b ^ 2 - 1)] at AB_id
Cleared hypotheses: AB_id
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
AB_id :
  A * B * (HPow.hPow (β := ℕ) b 2 - 1) - 1 * (HPow.hPow (β := ℕ) b 2 - 1) =
    b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have AB_id₁ : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: rw [← Nat.mul_sub_right_distrib, mul_comm] at AB_id
Cleared hypotheses: AB_id
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
have rw : b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Tactic: rw [AB_id]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
⊢ (A * B).ProbablePrime b
have ha₁ : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Tactic: have ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b) := by
    apply_fun fun x => x * (b ^ 2 - 1) at AB_id
    rw [Nat.div_mul_cancel hd] at AB_id
    apply_fun fun x => x - (b ^ 2 - 1) at AB_id
    nth_rw 2 [← one_mul (b ^ 2 - 1)] at AB_id
    rw [← Nat.mul_sub_right_distrib, mul_comm] at AB_id
    rw [AB_id]
    exact bp_helper hi_b (by grind)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 ∣ b ^ p + b
have rw : Even (b ^ p + b)
Tactic: rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
rw : Even (b ^ p + b)
⊢ 2 ∣ b ^ p + b
have rw₁ : Even (b ^ p) ↔ Even b
Tactic: rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
rw : Even (b ^ p + b)
rw₁ : Even (b ^ p) ↔ Even b
⊢ 2 ∣ b ^ p + b
have rw₂ : Even b ↔ Even b
Tactic: rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]