k m n : ℕ+
h : coprime ↑m ↑n
⊢ gcd k (m * n) = gcd k m * gcd k n
k m n : ℕ+
h : Coprime m n
⊢ gcd k (m * n) = gcd k m * gcd k n
rw [← coprime_coe] at h
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ ↑(gcd k (m * n)) = ↑(gcd k m * gcd k n)
k m n : ℕ+
h : coprime ↑m ↑n
⊢ gcd k (m * n) = gcd k m * gcd k n
apply eq
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ Nat.gcd (↑k) (↑m * ↑n) = Nat.gcd ↑k ↑m * Nat.gcd ↑k ↑n
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ ↑(gcd k (m * n)) = ↑(gcd k m * gcd k n)
simp only [gcd_coe, mul_coe]
no goals
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ Nat.gcd (↑k) (↑m * ↑n) = Nat.gcd ↑k ↑m * Nat.gcd ↑k ↑n
apply Nat.coprime.gcd_mul k h