case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ c

case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd a c * gcd b c
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c = c
apply dvd_antisymm
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ c * d
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ c
apply ((cop.gcd_left _).mul (cop.gcd_left _)).dvd_of_dvd_mul_right
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ a * b
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ c * d
rw [← h]
no goals
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ gcd a c * gcd b c ∣ a * b
apply Nat.mul_dvd_mul (gcd_dvd ..).1 (gcd_dvd ..).1
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd c a * gcd c b
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd a c * gcd b c
rw [gcd_comm a, gcd_comm b]
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd c (a * b)
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd c a * gcd c b
refine Nat.dvd_trans ?_ (gcd_mul_dvd_mul_gcd ..)
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ c
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ gcd c (a * b)
rw [h, gcd_mul_right_right d c]
no goals
case a
c d a b : Nat
cop : coprime c d
h : a * b = c * d
⊢ c ∣ c
apply Nat.dvd_refl