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)
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)
⊢ 1 ≤ p

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

Tactic:
exact bp_helper hi_b (by grind)

Premises used: _private.0.Nat.bp_helper
-- 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
⊢ (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)
-- 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)
rw : Even (b ^ p + b)
rw₁ : Even (b ^ p) ↔ Even b
rw₂ rw₃ : Even b ↔ Even b
⊢ 2 ∣ b ^ p + b

Tactic:
rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]

Premises used: Nat.even_add, Nat.even_pow', Nat.Prime.ne_zero, even_iff_two_dvd
-- 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)
⊢ 2 ∣ b ^ p + b

Tactic:
have ha₂ : 2 ∣ b ^ p + b := by
    rw [← even_iff_two_dvd, Nat.even_add, Nat.even_pow' p_prime.ne_zero]
-- 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
⊢ ¬p ∣ b

Tactic:
have : ¬p ∣ b := mt (fun h : p ∣ b => dvd_mul_of_dvd_left h _) not_dvd
-- 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
this : ¬p ∣ b
⊢ p.Coprime b

Tactic:
have : p.Coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
-- 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
this_1 : ¬p ∣ b
this : p.Coprime b
⊢ IsCoprime (R := ℤ) (↑b : ℤ) (↑p : ℤ)

Tactic:
have : IsCoprime (b : ℤ) ↑p := this.symm.isCoprime
-- 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
this_1 : ¬p ∣ b
this_2 : p.Coprime b
this : IsCoprime (R := ℤ) (↑b : ℤ) (↑p : ℤ)
⊢ HPow.hPow (α := ℤ) (↑b : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]

Tactic:
have : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p] := Int.ModEq.pow_card_sub_one_eq_one p_prime this
-- 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
this_1 : ¬p ∣ b
this_2 : p.Coprime b
this_3 : IsCoprime (R := ℤ) (↑b : ℤ) (↑p : ℤ)
this : HPow.hPow (α := ℤ) (↑b : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
have : ↑p ∣ ↑b ^ (p - 1) - ↑1 := mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
-- 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
this_1 : ¬p ∣ b
this_2 : p.Coprime b
this_3 : IsCoprime (R := ℤ) (↑b : ℤ) (↑p : ℤ)
this_4 : HPow.hPow (α := ℤ) (↑b : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
this : p ∣ b ^ (p - 1) - 1
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
mod_cast this

Premises used: Dvd.dvd, HSub.hSub, cast, HPow.hPow, Eq.refl, 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
this_1 : ¬p ∣ b
this_2 : p.Coprime b
this_3 : IsCoprime (R := ℤ) (↑b : ℤ) (↑p : ℤ)
this_4 : HPow.hPow (α := ℤ) (↑b : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
this : p ∣ b ^ (p - 1) - 1
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
exact mod_cast this
-- 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
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
have ha₃ : p ∣ b ^ (p - 1) - 1 := by
    have : ¬p ∣ b := mt (fun h : p ∣ b => dvd_mul_of_dvd_left h _) not_dvd
    have : p.Coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
    have : IsCoprime (b : ℤ) ↑p := this.symm.isCoprime
    have : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p] := Int.ModEq.pow_card_sub_one_eq_one p_prime this
    have : ↑p ∣ ↑b ^ (p - 1) - ↑1 := mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
    exact mod_cast this
-- 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
obtain : ∀ (k : ℕ) (hk : p = 2 * k + 1), HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
obtain ⟨k, hk⟩ := p_odd
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
⊢ p - 1 = 2 * k

Tactic:
simp [hk]
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
⊢ 2 ∣ p - 1

Tactic:
have : 2 ∣ p - 1 := ⟨k, by simp [hk]⟩
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
this : 2 ∣ p - 1
obtain : ∀ (c : ℕ) (hc : p - 1 = 2 * c), HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
obtain ⟨c, hc⟩ := this
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ HPow.hPow (β := ℕ) b 2 ^ c - 1

Tactic:
simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow _ 1 c

Premises used: one_pow, Nat.sub_dvd_pow_sub_pow, 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)
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
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ HPow.hPow (β := ℕ) b 2 ^ c - 1

Tactic:
have : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1 := by
      simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow _ 1 c
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this : HPow.hPow (β := ℕ) b 2 - 1 ∣ HPow.hPow (β := ℕ) b 2 ^ c - 1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * c) - 1), HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * c) - 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * c) - 1

Tactic:
rwa [← pow_mul] at this

Premises used: pow_mul
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this : HPow.hPow (β := ℕ) b 2 - 1 ∣ HPow.hPow (β := ℕ) b 2 ^ c - 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * c) - 1

Tactic:
have : b ^ 2 - 1 ∣ b ^ (2 * c) - 1 := by rwa [← pow_mul] at this
-- 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)
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
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this_1 : HPow.hPow (β := ℕ) b 2 - 1 ∣ HPow.hPow (β := ℕ) b 2 ^ c - 1
this : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * c) - 1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1), HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
rwa [← hc] at this
-- 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
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
have ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1 := by
    obtain ⟨k, hk⟩ := p_odd
    have : 2 ∣ p - 1 := ⟨k, by simp [hk]⟩
    obtain ⟨c, hc⟩ := this
    have : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1 := by
      simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow _ 1 c
    have : b ^ 2 - 1 ∣ b ^ (2 * c) - 1 := by rwa [← pow_mul] at this
    rwa [← hc] at this
-- 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 : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
rwa rwa₁ rwa₂ rwa₃ : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)

Tactic:
rwa [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
suffices : 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ 2 * p * (HPow.hPow (β := ℕ) b 2 - 1) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)

Tactic:
suffices q : 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b) by rwa [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
⊢ ¬p ∣ (HPow.hPow (β := ℕ) b 2 - 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
⊢ let A := (b ^ p - 1) / (b - 1);
  p < A

Tactic:
rw [mul_comm] at not_dvd

Premises used: mul_comm