awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : p.Coprime (HPow.hPow (β := ℕ) b 2 - 1)
q₂ : p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b ^ (p - 1) - 1
q₃ : p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b)
q₄ : p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b))
rwa : 2 * (p * (HPow.hPow (β := ℕ) b 2 - 1)) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
rwa₁ : p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
rwa₂ rwa₃ rwa₄ rwa₅ : p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b))
⊢ 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rwa [mul_assoc, mul_comm, mul_assoc b]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
⊢ 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)

Tactic:
have ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1) := by
    suffices q : 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b) by rwa [ha₁]
    -- We already proved that `b ^ 2 - 1 ∣ b ^ (p - 1) - 1`.
    -- Since `2 ∣ b ^ p + b` and `p ∣ b ^ p + b`, if we show that 2 and p are coprime, then we
    -- know that `2 * p ∣ b ^ p + b`
    have q₁ : Nat.Coprime p (b ^ 2 - 1) :=
      haveI q₂ : ¬p ∣ b ^ 2 - 1 := by
        rw [mul_comm] at not_dvd
        exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd
      (Nat.Prime.coprime_iff_not_dvd p_prime).mpr q₂
    have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.Coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄
    have q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b) := mul_dvd_mul q₂ ha₂
    have q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b)) :=
      dvd_mul_of_dvd_right q₃ _
    rwa [mul_assoc, mul_comm, mul_assoc b]
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (2 * p) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)

Tactic:
rw [mul_comm] at ha₅

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : (HPow.hPow (β := ℕ) b 2 - 1) * (2 * p) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1

Tactic:
Nat.dvd_of_mul_dvd_mul_left hi_bsquared ha₅

Premises used: Nat.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : (HPow.hPow (β := ℕ) b 2 - 1) * (2 * p) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1

Tactic:
exact Nat.dvd_of_mul_dvd_mul_left hi_bsquared ha₅

Premises used: Nat.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
⊢ 2 * p ∣ A * B - 1

Tactic:
have ha₆ : 2 * p ∣ A * B - 1 := by
    rw [mul_comm] at ha₅
    exact Nat.dvd_of_mul_dvd_mul_left hi_bsquared ha₅
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
h : b ^ (2 * p) - 1 = A * B * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ A * B ∣ b ^ (2 * p) - 1

Tactic:
use b ^ 2 - 1
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
⊢ A * B * (HPow.hPow (β := ℕ) b 2 - 1) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1) * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
have : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1) :=
      congr_arg (fun x : ℕ => x * (b ^ 2 - 1)) AB_id
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
this :
  A * B * (HPow.hPow (β := ℕ) b 2 - 1) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1) * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ b ^ (2 * p) - 1 = A * B * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
simpa only [add_comm, Nat.div_mul_cancel hd, Nat.sub_add_cancel hi_bpowtwop] using this.symm

Premises used: Nat.div_mul_cancel, add_comm, Nat.sub_add_cancel, Eq.symm
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
⊢ A * B ∣ b ^ (2 * p) - 1

Tactic:
have ha₇ : A * B ∣ b ^ (2 * p) - 1 := by
    use b ^ 2 - 1
    have : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1) :=
      congr_arg (fun x : ℕ => x * (b ^ 2 - 1)) AB_id
    simpa only [add_comm, Nat.div_mul_cancel hd, Nat.sub_add_cancel hi_bpowtwop] using this.symm
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
ha₇ : A * B ∣ b ^ (2 * p) - 1
obtain : ∀ (q : ℕ) (hq : A * B - 1 = 2 * p * q), (A * B).ProbablePrime b
⊢ (A * B).ProbablePrime b

Tactic:
obtain ⟨q, hq⟩ := ha₆
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1

Tactic:
simpa only [one_pow, pow_mul, hq] using Nat.sub_dvd_pow_sub_pow _ 1 q

Premises used: one_pow, Nat.sub_dvd_pow_sub_pow, pow_mul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1

Tactic:
have ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1 := by
    simpa only [one_pow, pow_mul, hq] using Nat.sub_dvd_pow_sub_pow _ 1 q
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1
⊢ (A * B).ProbablePrime b

Tactic:
dvd_trans ha₇ ha₈

Premises used: dvd_trans, Nat.ProbablePrime
-- Module: Mathlib.NumberTheory.FermatPsp
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)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1
⊢ (A * B).ProbablePrime b

Tactic:
exact dvd_trans ha₇ ha₈

Premises used: dvd_trans
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
set :
  let A := (b ^ p - 1) / (b - 1);
  p < A * ((b ^ p + 1) / (b + 1))
⊢ p < (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))

Tactic:
set A := (b ^ p - 1) / (b - 1)

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
set :
  let B := (b ^ p + 1) / (b + 1);
  p < A * B
⊢ p < A * ((b ^ p + 1) / (b + 1))

Tactic:
set B := (b ^ p + 1) / (b + 1)

Premises used: HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A

Tactic:
have hA : p < A := a_id_helper b_ge_two p_gt_two
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
⊢ 1 < B

Tactic:
have : 1 < B := b_id_helper b_ge_two p_gt_two
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
this : 1 < B
⊢ 0 < B

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
⊢ 0 < B

Tactic:
have hB : 0 < B := by
    have : 1 < B := b_id_helper b_ge_two p_gt_two
    lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hB : 0 < B
⊢ p < A * B

Tactic:
hA.trans_le (Nat.le_mul_of_pos_right _ hB)

Premises used: Nat.le_mul_of_pos_right, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hB : 0 < B
⊢ p < A * B

Tactic:
exact hA.trans_le (Nat.le_mul_of_pos_right _ hB)

Premises used: Nat.le_mul_of_pos_right, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
pos : ∀ (b_ge_two : 2 ≤ b), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
neg : ∀ (b_ge_two : ¬2 ≤ b), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n

Tactic:
by_cases b_ge_two : 2 ≤ b
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ (p : ℕ), b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p ∧ Prime p

Tactic:
have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h_1 : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ (p : ℕ), b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p ∧ Prime p
pos : ∀ (p : ℕ) (hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p) (hp₂ : Prime p), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n

Tactic:
obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
⊢ 0 < b

Tactic:
have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
⊢ 4 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
⊢ LT.lt (α := ℕ) 1 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
⊢ 0 < HPow.hPow (β := ℕ) b 2 - 1

Tactic:
have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (lt_of_lt_of_le (by simp) h₂)
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
⊢ 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ b * (HPow.hPow (β := ℕ) b 2 - 1) < p

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ b * (HPow.hPow (β := ℕ) b 2 - 1) < p

Tactic:
have h₅ : b * (b ^ 2 - 1) < p := by lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
⊢ ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
⊢ 2 < p

Tactic:
have h₉ : 2 < p := lt_of_le_of_lt h₈ h₅
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
⊢ p < b.psp_from_prime p

Tactic:
have h₁₀ := psp_from_prime_gt_p b_ge_two h₉