exact (Nat.dvd_add_right h3).mp (h5 ▸ h4)
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
no goals