-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_mul_dvd_mul_gcd [GCDMonoid α] (k m n : α) : gcd k (m * n) ∣ gcd k m * gcd k n

Proof state:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ gcd k n

Tactic:
have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'

Result:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hn'k : n' ∣ k
⊢ n' ∣ gcd k n

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' * n' ∣ gcd k m * gcd k n

Tactic:
apply mul_dvd_mul

Result:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ gcd k m

case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ gcd k n

Proof state:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hn'k : n' ∣ k
⊢ n' ∣ gcd k n

Tactic:
exact dvd_gcd hn'k hn'

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ gcd k (m * n) ∣ gcd k m * gcd k n

Tactic:
rw [h]

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ m' * n' ∣ gcd k m * gcd k n

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n : α
⊢ gcd k (m * n) ∣ gcd k m * gcd k n

Tactic:
obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ gcd k (m * n) ∣ gcd k m * gcd k n

Proof state:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hm'k : m' ∣ k
⊢ m' ∣ gcd k m

Tactic:
exact dvd_gcd hm'k hm'

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
⊢ m' * n' ∣ gcd k m * gcd k n

Tactic:
have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' * n' ∣ gcd k m * gcd k n

Proof state:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ gcd k m

Tactic:
have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'

Result:
case intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hm'k : m' ∣ k
⊢ m' ∣ gcd k m