awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
have ha₆ : (HPow.hPow (β := ℕ) b 2 - 1) * (2 * p) ∣ (HPow.hPow (β := ℕ) b 2 - 1) * (A * B - 1)
Tactic: rw [mul_comm] at ha₅
Cleared hypotheses: ha₅
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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)
⊢ (A * B).ProbablePrime b
have ha₆ : 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₅
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
have h : b ^ (2 * p) - 1 = A * B * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: use b ^ 2 - 1
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ b ^ (2 * p) - 1 = A * B * (HPow.hPow (β := ℕ) b 2 - 1)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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).ProbablePrime b
have ha₇ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
⊢ (A * B).ProbablePrime b
have obtain : ∀ (q : ℕ) (hq : A * B - 1 = 2 * p * q), (A * B).ProbablePrime b
Tactic: obtain ⟨q, hq⟩ := ha₆
Cleared hypotheses: ha₆
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ (A * B).ProbablePrime b
have ha₈ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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 * B
have hA : p < A
Tactic: have hA : p < A := a_id_helper b_ge_two p_gt_two
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
have this : 1 < B
Tactic: have : 1 < B := b_id_helper b_ge_two p_gt_two
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ p < A * B
have hB : 0 < B
Tactic: have hB : 0 < B := by
    have : 1 < B := b_id_helper b_ge_two p_gt_two
    lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have pos : ∀ (b_ge_two : 2 ≤ b), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
Tactic: by_cases b_ge_two : 2 ≤ b
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
pos : ∀ (b_ge_two : 2 ≤ b), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have neg : ∀ (b_ge_two : ¬2 ≤ b), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
Tactic: by_cases b_ge_two : 2 ≤ b
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₁ : ∃ (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)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have pos : ∀ (p : ℕ) (hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p) (hp₂ : Prime p), ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
Tactic: obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₁ : 0 < b
Tactic: have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
Tactic: have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₃ : 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₂)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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)
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
Tactic: have h₅ : b * (b ^ 2 - 1) < p := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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)
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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)
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
Tactic: have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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)
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₉ : 2 < p
Tactic: have h₉ : 2 < p := lt_of_le_of_lt h₈ h₅
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
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
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₁₀ : p < b.psp_from_prime p
Tactic: have h₁₀ := psp_from_prime_gt_p b_ge_two h₉
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
h₁₀ : p < b.psp_from_prime p
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₁₁ : (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p
Tactic: use psp_from_prime b p
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
h₁₀ : p < b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p
have h₁₁ : (b.psp_from_prime p).FermatPsp b
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
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
h₁₀ : p < b.psp_from_prime p
h₁₁ : (b.psp_from_prime p).FermatPsp b
⊢ (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p
have h₁₂ : m ≤ b.psp_from_prime p
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have h₁ : b = 1
Tactic: have h₁ : b = 1 := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n
have neg : ∃ (n : ℕ), n.FermatPsp 1 ∧ m ≤ n
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ (n : ℕ), n.FermatPsp 1 ∧ m ≤ n
have h₂ : (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)
Tactic: use 2 * (m + 2)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (hypothesis)
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)
have this : ¬Prime (2 * (m + 2))
Tactic: have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by lia) (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b
have refine : ∀ (n : ℕ), ∃ b_1 ≥ n, b_1.FermatPsp b
Tactic: refine Filter.frequently_atTop.2 fun n => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FermatPsp (goal)
Goal:
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b
have obtain : ∀ (p : ℕ) (hp : p.FermatPsp b ∧ n ≤ p), ∃ b_1 ≥ n, b_1.FermatPsp b
Tactic: obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
n : ℕ
s : Set ℕ
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have simp_rw : IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
  n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
n : ℕ
s : Set ℕ
simp_rw :
  IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have simp_rw₁ : Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
    Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | k ∉ AddSubmonoid.closure s}) n ↔
  n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
n : ℕ
s : Set ℕ
simp_rw :
  IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₁ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | k ∉ AddSubmonoid.closure s}) n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have simp_rw₂ : Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
    Membership.mem (γ := Set ℕ)
      {x : ℕ | ∀ ⦃a : ℕ⦄, Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} a → a ≤ x} n ↔
  n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
n : ℕ
s : Set ℕ
simp_rw :
  IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₁ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | k ∉ AddSubmonoid.closure s}) n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₂ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ)
        {x : ℕ | ∀ ⦃a : ℕ⦄, Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} a → a ≤ x} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have simp_rw₃ : (n ∉ AddSubmonoid.closure s ∧ ∀ ⦃a : ℕ⦄, a ∉ AddSubmonoid.closure s → a ≤ n) ↔
  n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
n : ℕ
s : Set ℕ
simp_rw :
  IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₁ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | k ∉ AddSubmonoid.closure s}) n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₂ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ)
        {x : ℕ | ∀ ⦃a : ℕ⦄, Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} a → a ≤ x} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₃ :
  (n ∉ AddSubmonoid.closure s ∧ ∀ ⦃a : ℕ⦄, a ∉ AddSubmonoid.closure s → a ≤ n) ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have simp_rw₄ : (n ∉ AddSubmonoid.closure s ∧ ∀ ⦃a : ℕ⦄, ¬a ≤ n → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) a) ↔
  n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ FrobeniusNumber (m * n - m - n) {m, n}
have simp_rw : IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
Tactic: simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (hypothesis)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
have hmn : m + n ≤ m * n
Tactic: have hmn : m + n ≤ m * n := add_le_mul hm hn
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
have left : Membership.mem (γ := Set ℕ) {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
left : Membership.mem (γ := Set ℕ) {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
⊢ IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
have right : Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k}) (m * n - m - n)
Tactic: constructor