Theorem: arb_large_soln (IIScExperiments/Solutions/NumberTheory3Solutions.lean)

State before:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
intro N
State after:
N : ℕ
⊢ ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1

State before:
N : ℕ
⊢ ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
use 65 * N + 4
State after:
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1

State before:
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
refine ⟨?_, ?_⟩
State after:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N

case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1

State before:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N

case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
{ linarith }
State after:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1

State before:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
{ apply divides_of_cong_four }
State after:
no goals

State before:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N
Tactic:
linarith
State after:
no goals

State before:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
apply divides_of_cong_four
State after:
no goals