Theorem: Section15Sheet3.infinite_setOf_solutions (FormalisingMathematics2024/Section15numberTheory/Sheet3.lean)

State before:
⊢ Set.Infinite {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}
Tactic:
rw [infinite_iff_arb_large]
State after:
⊢ ∀ (N : ℕ), ∃ n > N, n ∈ {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}

State before:
⊢ ∀ (N : ℕ), ∃ n > N, n ∈ {n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1}
Tactic:
exact arb_large_soln
State after:
no goals