Theorem: Section15Sheet3Solutions.arb_large_soln (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet3.lean)

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

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

State before:
case h
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
constructor
State after:
case h.left
N : ℕ
⊢ 65 * N + 4 > N

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

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

State before:
case h.right
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