-- Mathlib/NumberTheory/FermatPsp.lean
theorem exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) :
    ∃ n : ℕ, FermatPsp n b ∧ m ≤ n

Proof state:
case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)

Result:
case pos
b : ℕ
h✝ : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ p, b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ 1 < 2 * (m + 2)

Tactic:
omega

Result:
no goals

Proof state:
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ n, n.FermatPsp 1 ∧ m ≤ n

Tactic:
use 2 * (m + 2)

Result:
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
⊢ b * (b ^ 2 - 1) < p

Tactic:
omega

Result:
no goals

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)

Tactic:
have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by omega) (by omega)

Result:
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (gt_of_ge_of_gt h₂ (by norm_num))

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
use psp_from_prime b p

Result:
case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ (Nat.psp_from_prime b p).FermatPsp b ∧ m ≤ Nat.psp_from_prime b p

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < Nat.psp_from_prime b p
⊢ m ≤ p

Tactic:
omega

Result:
no goals

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₅ : b * (b ^ 2 - 1) < p := by omega

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ 2 ≠ 1

Tactic:
omega

Result:
no goals

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
by_cases b_ge_two : 2 ≤ b

Result:
case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₁ : b = 1 := by omega

Result:
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ 4 > 1

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ b = 1

Tactic:
omega

Result:
no goals

Proof state:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ m + 2 ≠ 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
b : ℕ
h✝ : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ p, b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h

Result:
case pos.intro.intro
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n