How to apply `gcd_dvd_iff_exists`

Stream: new members

[tsuki]

I want to use gcd_dvd_iff_exists to complete the proof, but fail to describe \exist, What should I do with this?

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

theorem imo_1959_p1 (n : ℕ) (h₀ : 0 < n) : Nat.gcd (21 * n^2 + 4*n) (14 * n^2 + 3*n) = n := by
  have h₁:((-2:ℤ))*(21*n + 4) + (3)*(14*n+3) = 1 := by
    ring_nf
  have h₂: Nat.gcd (21*n + 4) (14 * n + 3) = 1 := by
    sorry
  have h₃: 21 * n^2 + 4*n = n * (21*n + 4) := by
    ring
  have h₄: 14 * n^2 + 3*n = n * (14*n + 3) := by
    ring
  rw[h₃,h₄]
  rw[gcd_mul_left]
  rw[h₂]
  ring

[Kevin Buzzard]

Your goal is about Nat.gcd but the lemma docs#gcd_dvd_iff_exists which you cite is about GCDMonoid.gcd, so it won't apply as things stand.

[tsuki]

Can I write  Nat.gcd for n? I mean if the type of n is Nat?

[Robin Arnez]

Does this work?

theorem imo_1959_p1 (n : ℕ) : Nat.gcd (21 * n^2 + 4*n) (14 * n^2 + 3*n) = n := by
  have h₁:((-2:ℤ))*(21*n + 4) + (3)*(14*n+3) = 1 := by
    ring_nf
  have h₂: Nat.gcd (21*n + 4) (14 * n + 3) = 1 := by
    suffices ((14 * n + 3) + (7 * n + 1)).gcd (14 * n + 3) = 1 by
      ring_nf at this ⊢
      exact this
    rw [Nat.gcd_self_add_left]
    suffices (7 * n + 1).gcd ((7 * n + 1) + (7 * n + 1) + 1) = 1 by
      ring_nf at this ⊢
      exact this
    rw [Nat.gcd_comm, Nat.add_assoc, gcd_self_add_left, gcd_self_add_left, Nat.gcd_one_left]
  have h₃: 21 * n^2 + 4*n = n * (21*n + 4) := by
    ring
  have h₄: 14 * n^2 + 3*n = n * (14*n + 3) := by
    ring
  rw [h₃,h₄]
  rw [Nat.gcd_mul_left]
  rw [h₂]
  ring