Theorem: infinite_set_of_solutions (IIScExperiments/NumberTheory3.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 ∈ { n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1 }

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