k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ gcd k (m * n) ∣ gcd k m * gcd k n
k m n : Nat
⊢ gcd k (m * n) ∣ gcd k m * gcd k n
let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
  prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ m' * n' ∣ gcd k m * gcd k n
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ gcd k (m * n) ∣ gcd k m * gcd k n
rw [h]
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
h' : m' * n' ∣ k
⊢ m' * n' ∣ gcd k m * gcd k n
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ m' * n' ∣ gcd k m * gcd k n
have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..
no goals
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
h' : m' * n' ∣ k
⊢ m' * n' ∣ gcd k m * gcd k n
exact Nat.mul_dvd_mul
  (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
  (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')