no mul_sub in int?

Stream: general

[onriv]

Hi. I am following the tutorial https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html but found the following example failed:

import data.int.basic

variables a b c d : ℤ
example : a * (b - c) = a * b - a * c := mul_sub a b c

for no mul_sub any more. Any way to define it again? Thanks!

[onriv]

Ah my bad, in fact there are mul_sub and sub_mul in init.data.int.basic