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