awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
refine : n ∣ HPow.hPow (α := ℕ) 1 (n - 1) - 1
⊢ n.FermatPsp 1

Tactic:
refine ⟨show n ∣ 1 ^ (n - 1) - 1 from ?_, h₂, h₁⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ 0 = HPow.hPow (α := ℕ) 1 (n - 1) - 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n ∣ HPow.hPow (α := ℕ) 1 (n - 1) - 1

Tactic:
exact show 0 = 1 ^ (n - 1) - 1 by simp ▸ dvd_zero n
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
rw : b < ∑ k ∈ Finset.range b, a ^ k
⊢ b < (a ^ b - 1) / (a - 1)

Tactic:
rw [← Nat.geomSum_eq ha]

Premises used: Nat.geomSum_eq
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b = ∑ x ∈ Finset.range b, 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
i : ℕ
hi : i ∈ Finset.range b
⊢ 0 < a

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
refine : ∃ i ∈ Finset.range b, 1 < a ^ i
⊢ LT.lt (α := ℕ) (∑ x ∈ Finset.range b, 1) (∑ k ∈ Finset.range b, a ^ k)

Tactic:
refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_

Premises used: Nat.one_le_pow, Finset.sum_lt_sum
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 1 < b

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 1 < HPow.hPow (β := ℕ) a 1

Tactic:
simpa using ha
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ ∃ i ∈ Finset.range b, 1 < a ^ i

Tactic:
exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using ha⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
b₁ : b = ∑ x ∈ Finset.range b, 1
b₂ : LT.lt (α := ℕ) (∑ x ∈ Finset.range b, 1) (∑ k ∈ Finset.range b, a ^ k)
⊢ b < ∑ k ∈ Finset.range b, a ^ k

Tactic:
calc
    b = ∑ _ ∈ Finset.range b, (1 : ℕ) := by simp
    _ < _ := by
      refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using ha⟩

Premises used: Finset.range, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
rw : 2 * a.succ ≤ a ^ b + 1
⊢ 2 ≤ (a ^ b + 1) / (a + 1)

Tactic:
rw [Nat.le_div_iff_mul_le (Nat.zero_lt_succ _)]

Premises used: Nat.zero_lt_succ, Nat.le_div_iff_mul_le
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
a₁ : Nat.mul 2 a + 1 ≤ a ^ b
⊢ 2 * a.succ ≤ a ^ b + 1

Tactic:
apply Nat.succ_le_succ

Premises used: Nat.succ_le_succ
-- Module: Mathlib.NumberTheory.FermatPsp
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
nlinarith₂ nlinarith₃ : HPow.hPow (β := ℕ) a 2 * a < 2 * a + 1 → GT.gt (α := ℤ) 2 0
⊢ 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
rw rw₁ : HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 2 * a
⊢ HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 3

Tactic:
rw [Nat.pow_succ a 2]

Premises used: Nat.pow_succ, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ HPow.hPow (β := ℕ) a 3 ≤ a ^ b

Tactic:
pow_right_mono₀ (Nat.le_of_succ_le ha) hb

Premises used: Nat.le_of_succ_le, pow_right_mono₀
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
a₁ : 2 * a + 1 ≤ HPow.hPow (β := ℕ) a 2 * a
a₂ : HPow.hPow (β := ℕ) a 2 * a = HPow.hPow (β := ℕ) a 3
⊢ Nat.mul 2 a + 1 ≤ a ^ b

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

Premises used: Nat.le_of_succ_le, pow_right_mono₀
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
⊢ b - 1 ∣ b ^ p - 1

Tactic:
simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow b 1 p

Premises used: one_pow, Nat.sub_dvd_pow_sub_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
⊢ 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
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ b + 1 ∣ b ^ p + 1

Tactic:
simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1

Premises used: one_pow, Odd.nat_add_dvd_pow_add_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
h : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
⊢ 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
-- Module: Mathlib.NumberTheory.FermatPsp
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 ^ p - 1) * (b ^ p + 1) / ((b - 1) * (b + 1))

Tactic:
Nat.div_mul_div_comm q₁ q₂

Premises used: Nat.div_mul_div_comm
-- Module: Mathlib.NumberTheory.FermatPsp
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)
h₁ : HPow.hPow (β := ℕ) b 2 - 1 = (b - 1) * (b + 1)
⊢ (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
convert! Nat.div_mul_div_comm q₁ q₂ using 2

Premises used: Nat.div_mul_div_comm
-- Module: Mathlib.NumberTheory.FermatPsp
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 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2
⊢ b ^ (2 * p) - 1 = (b ^ p - 1) * (b ^ p + 1)

Tactic:
rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]

Premises used: Nat.sq_sub_sq, HSub.hSub, mul_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
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)
h₁ h₂ : HPow.hPow (β := ℕ) b 2 - 1 = HPow.hPow (β := ℕ) b 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2
⊢ HPow.hPow (β := ℕ) b 2 - 1 = (b - 1) * (b + 1)

Tactic:
rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]

Premises used: Nat.sq_sub_sq, HSub.hSub, mul_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
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 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1)) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))
⊢ b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))

Tactic:
rw [Nat.sub_sub]

Premises used: Nat.sub_sub
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1)) = b ^ (2 * p) - (1 + (HPow.hPow (β := ℕ) b 2 - 1))
⊢ 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]

Premises used: Nat.add_sub_assoc
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : b ^ (2 * p) - HPow.hPow (β := ℕ) b 2 = b ^ (2 * p) - HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - (1 + HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - HPow.hPow (β := ℕ) b 2

Tactic:
rw [Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_cancel_left
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : b ^ (p * 2) - HPow.hPow (β := ℕ) b 2 = b ^ (p * 2) - HPow.hPow (β := ℕ) b 2
⊢ b ^ (2 * p) - HPow.hPow (β := ℕ) b 2 = b ^ (p * 2) - HPow.hPow (β := ℕ) b 2

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2
⊢ b ^ (p * 2) - HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b ^ p + b) * (b ^ p - b) = (b ^ p + b) * (b ^ p - b)
⊢ HPow.hPow (β := ℕ) (b ^ p) 2 - HPow.hPow (β := ℕ) b 2 = (b ^ p + b) * (b ^ p - b)

Tactic:
rw [Nat.sq_sub_sq]

Premises used: Nat.sq_sub_sq
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)

Tactic:
rw [Nat.sub_add_cancel hp]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
⊢ (b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)

Tactic:
rw [pow_succ']

Premises used: Nat.pow_succ'
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
⊢ (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ HPow.hPow (β := ℕ) b 2
rw rw₁ : (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rw [Nat.mul_sub_left_distrib]

Premises used: Nat.mul_sub_left_distrib
-- 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)
set :
  let A := (b ^ p - 1) / (b - 1);
  (A * ((b ^ p + 1) / (b + 1))).FermatPsp b
⊢ ((b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))).FermatPsp b

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

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_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)
⊢ 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_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
⊢ 1 < A

Tactic:
lia
-- 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
⊢ 1 < A

Tactic:
have hi_A : 1 < A := by lia
-- 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
⊢ 1 < B

Tactic:
have hi_B : 1 < B := b_id_helper b_ge_two p_gt_two
-- 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
⊢ 0 < b

Tactic:
lia
-- 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
⊢ 0 < b

Tactic:
have hi_b : 0 < b := by lia
-- 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
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
have := Nat.pow_le_pow_left b_ge_two 2
-- 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
this : HPow.hPow (α := ℕ) (β := ℕ) 2 2 ≤ HPow.hPow (β := ℕ) b 2
⊢ 0 < HPow.hPow (β := ℕ) b 2 - 1

Tactic:
lia
-- 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
⊢ 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
-- 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
⊢ 1 ≤ b ^ (2 * p)

Tactic:
have hi_bpowtwop : 1 ≤ b ^ (2 * p) := Nat.one_le_pow (2 * p) b hi_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)
⊢ 1 ≤ b ^ (p - 1)

Tactic:
have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_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)
⊢ Odd p

Tactic:
have p_odd : Odd p := p_prime.odd_of_ne_two p_gt_two.ne.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
⊢ ¬Prime (A * B)

Tactic:
have AB_not_prime : ¬Nat.Prime (A * B) := Nat.not_prime_mul hi_A.ne' hi_B.ne'
-- 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)
⊢ 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
-- 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)
⊢ HPow.hPow (β := ℕ) b 2 - 1 ∣ b ^ (2 * p) - 1

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

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)
⊢ 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
-- 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
⊢ (A * B).FermatPsp b

Tactic:
⟨?_, AB_not_prime, one_lt_mul'' hi_A hi_B⟩

Premises used: Nat.FermatPsp, And.intro, one_lt_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)
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
refine : (A * B).ProbablePrime b
⊢ (A * B).FermatPsp b

Tactic:
refine ⟨?_, AB_not_prime, one_lt_mul'' hi_A hi_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
⊢ 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

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, 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)
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)
⊢ A * B * (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1

Tactic:
rw [Nat.div_mul_cancel hd] at AB_id

Premises used: Nat.div_mul_cancel
-- 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 : A * B * (HPow.hPow (β := ℕ) b 2 - 1) = b ^ (2 * p) - 1
⊢ 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

Premises used: HSub.hSub, HPow.hPow, 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)
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)
⊢ 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

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat, one_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)
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 ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1)

Tactic:
rw [← Nat.mul_sub_right_distrib, mul_comm] at AB_id

Premises used: Nat.mul_sub_right_distrib, 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)
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)
rw : b ^ (2 * p) - 1 - (HPow.hPow (β := ℕ) b 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
⊢ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rw [AB_id]