Theorem: Imo1959P1.calculation (Compfiles/Imo1959P1.lean)

State before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
⊢ k ∣ 1
Tactic:
have h3 : k ∣ 2 * (21 * n + 4) := h1.mul_left 2
State after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
⊢ k ∣ 1

State before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
⊢ k ∣ 1
Tactic:
have h4 : k ∣ 3 * (14 * n + 3) := h2.mul_left 3
State after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ k ∣ 1

State before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ k ∣ 1
Tactic:
have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1 := by ring
State after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
⊢ k ∣ 1

State before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
⊢ k ∣ 1
Tactic:
exact (Nat.dvd_add_right h3).mp (h5 ▸ h4)
State after:
no goals

State before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
Tactic:
ring
State after:
no goals