m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
m n k : ℕ+
⊢ Coprime k m → gcd m (k * n) = gcd m n
intro h
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd n m
m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
iterate 2 rw [gcd_comm]; symm;
no goals
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd n m
apply Coprime.gcd_mul_left_cancel _ h
m n k : ℕ+
h : Coprime k m
⊢ gcd n m = gcd (k * n) m
m n k : ℕ+
h : Coprime k m
⊢ gcd m n = gcd (k * n) m
rw [gcd_comm]
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd n m
m n k : ℕ+
h : Coprime k m
⊢ gcd n m = gcd (k * n) m
symm