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

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

case right
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1

State before:
case left
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 3380 * t ^ 2 + 416 * t + 13
State after:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)

State before:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)
Tactic:
ring
State after:
no goals

State before:
case right
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 1300 * t ^ 2 + 160 * t + 5
State after:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)

State before:
case h
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)
Tactic:
ring
State after:
no goals