b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, FermatPsp n b
refine' Filter.frequently_atTop.2 fun n => _
case intro
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : FermatPsp p b ∧ n ≤ p
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
b : ℕ
h : 1 ≤ b
n : ℕ
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n
no goals
case intro
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : FermatPsp p b ∧ n ≤ p
⊢ ∃ b_1, b_1 ≥ n ∧ FermatPsp b_1 b
exact ⟨p, hp.2, hp.1⟩