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

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

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

State before:
case refine_1
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1

case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
{ use 3380*t^2 + 416*t + 13
  ring }
State after:
case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1

State before:
case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
{ use 1300*t^2 + 160*t + 5
  ring }
State after:
no goals

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

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

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

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