-- Mathlib/NumberTheory/FermatPsp.lean
theorem psp_from_prime_gt_p {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_prime : p.Prime)
    (p_gt_two : 2 < p) : p < psp_from_prime b p

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ b ^ 2 - 1 ∣ b ^ (2 * p) - 1

Tactic:
simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p

Result:
no goals

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
⊢ p < A * ((b ^ p + 1) / (b + 1))

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

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A * B

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
⊢ p < Nat.psp_from_prime b p

Tactic:
unfold psp_from_prime

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
⊢ p < (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1))

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < A * B

Tactic:
rw [show A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1) from
    AB_id_helper _ _ b_ge_two (p_prime.odd_of_ne_two p_gt_two.ne.symm)]

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Proof state:
case h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
⊢ (b ^ 2) ^ (p - 1) * b ^ 2 - p > p * b ^ 2 - p

Tactic:
have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right _ (show 0 < b ^ 2 by positivity)

Result:
case h₂
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
this : p ≤ p * b ^ 2
⊢ (b ^ 2) ^ (p - 1) * b ^ 2 - p > p * b ^ 2 - p

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this : 2 ≤ 2 * p - 2
⊢ p < b ^ (2 * p - 2)

Tactic:
have : 2 + p ≤ 2 * p := by omega

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this✝ : 2 ≤ 2 * p - 2
this : 2 + p ≤ 2 * p
⊢ p < b ^ (2 * p - 2)

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * (b ^ 2 - 1) < b ^ (2 * p) - 1

Tactic:
rw [Nat.mul_sub_left_distrib, mul_one, pow_mul]

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ p - 1

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this✝¹ : 2 ≤ 2 * p - 2
this✝ : 2 + p ≤ 2 * p
this : p ≤ 2 * p - 2
⊢ p < b ^ (2 * p - 2)

Tactic:
exact this.trans_lt (Nat.lt_pow_self b_ge_two)

Result:
no goals

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Tactic:
suffices h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1 by
  have h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1) :=
    Nat.div_lt_div_of_lt_of_dvd AB_dvd h
  have h₂ : 0 < b ^ 2 - 1 := by
    linarith [show 3 ≤ b ^ 2 - 1 from le_tsub_of_add_le_left (show 4 ≤ b ^ 2 by nlinarith)]
  rwa [Nat.mul_div_cancel _ h₂] at h₁

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * (b ^ 2 - 1) < b ^ (2 * p) - 1

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
h : p * (b ^ 2 - 1) < b ^ (2 * p) - 1
h₁ : p * (b ^ 2 - 1) / (b ^ 2 - 1) < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
⊢ 0 < b ^ 2 - 1

Tactic:
linarith [show 3 ≤ b ^ 2 - 1 from le_tsub_of_add_le_left (show 4 ≤ b ^ 2 by nlinarith)]

Result:
no goals

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Tactic:
have AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1 := by
  simpa only [one_pow, pow_mul] using nat_sub_dvd_pow_sub_pow _ 1 p

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
this : 2 ≤ 2 * p - 2
⊢ 2 + p ≤ 2 * p

Tactic:
omega

Result:
no goals

Proof state:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ (p - 1 + 1) - 1

Tactic:
rw [Nat.pow_succ (b ^ 2)]

Result:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
⊢ p * b ^ 2 - p < (b ^ 2) ^ (p - 1) * b ^ 2 - 1