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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
⊢ let A := (b ^ p - 1) / (b - 1);
  1 < A

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
⊢ let B := (b ^ p + 1) / (b + 1);
  1 < B

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  1 < B
⊢ 0 < b

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  1 < B
hi_b₁ : 0 < b
⊢ 0 < HPow.hPow (β := ℕ) b 2 - 1

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  1 < B
hi_b₁ : 0 < b
hi_bsquared₁ : 0 < HPow.hPow (β := ℕ) b 2 - 1
⊢ 1 ≤ b ^ (2 * p)

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  1 < B
hi_b₁ : 0 < b
hi_bsquared₁ : 0 < HPow.hPow (β := ℕ) b 2 - 1
hi_bpowtwop₁ : 1 ≤ b ^ (2 * p)
⊢ 1 ≤ b ^ (p - 1)

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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)
⊢ Odd p

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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
⊢ let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
⊢ let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
AB_id₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
AB_id₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd₁ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
⊢ let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
AB_id₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd₁ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₅ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 ∣ b ^ p + b

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
AB_id₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd₁ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₅ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₆ : 2 ∣ b ^ p + b
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
rw [mul_comm] at not_dvd

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
not_dvd₁ : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
hA₁ :
  let A := (b ^ p - 1) / (b - 1);
  p < A
hi_A₁ :
  let A := (b ^ p - 1) / (b - 1);
  1 < A
hi_B₁ :
  let B := (b ^ p + 1) / (b + 1);
  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₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  ¬Prime (A * B)
AB_id₁ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  A * B = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)
hd₁ : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1
ha₅ :
  let A := (b ^ p - 1) / (b - 1);
  let B := (b ^ p + 1) / (b + 1);
  (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
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
rw [mul_comm] at not_dvd

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 ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
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
⊢ ¬p ∣ HPow.hPow (β := ℕ) b 2 - 1

Tactic:
mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd

Premises used: dvd_mul_of_dvd_left, mt
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 1) * b
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
⊢ ¬p ∣ HPow.hPow (β := ℕ) b 2 - 1

Tactic:
exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd

Premises used: dvd_mul_of_dvd_left, mt
-- 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
⊢ p.Coprime (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
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₂
-- 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)
⊢ p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b ^ (p - 1) - 1

Tactic:
have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.Coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ 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
q₁ : p.Coprime (HPow.hPow (β := ℕ) b 2 - 1)
q₂ : p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b ^ (p - 1) - 1
⊢ p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
have q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b) := mul_dvd_mul q₂ 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
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)
⊢ p * (HPow.hPow (β := ℕ) b 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b))

Tactic:
have q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b)) :=
      dvd_mul_of_dvd_right q₃ _