i j k : ℤ
⊢ Nat.gcd (natAbs i * natAbs j) (natAbs k * natAbs j) = Nat.gcd (natAbs i) (natAbs k) * natAbs j
i j k : ℤ
⊢ gcd (i * j) (k * j) = gcd i k * natAbs j
rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
no goals
i j k : ℤ
⊢ Nat.gcd (natAbs i * natAbs j) (natAbs k * natAbs j) = Nat.gcd (natAbs i) (natAbs k) * natAbs j
apply Nat.gcd_mul_right