m n k : ℕ+
h : Coprime k n
⊢ gcd (k * m) n = gcd m n
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
intro h
case a
m n k : ℕ+
h : Coprime k n
⊢ ↑(gcd (k * m) n) = ↑(gcd m n)
m n k : ℕ+
h : Coprime k n
⊢ gcd (k * m) n = gcd m n
apply eq
case a
m n k : ℕ+
h : Coprime k n
⊢ Nat.gcd (↑k * ↑m) ↑n = Nat.gcd ↑m ↑n
case a
m n k : ℕ+
h : Coprime k n
⊢ ↑(gcd (k * m) n) = ↑(gcd m n)
simp only [gcd_coe, mul_coe]
case a.H
m n k : ℕ+
h : Coprime k n
⊢ coprime ↑k ↑n
case a
m n k : ℕ+
h : Coprime k n
⊢ Nat.gcd (↑k * ↑m) ↑n = Nat.gcd ↑m ↑n
apply Nat.coprime.gcd_mul_left_cancel
no goals
case a.H
m n k : ℕ+
h : Coprime k n
⊢ coprime ↑k ↑n
simpa