mathlib3

8e50164d - chore(data/int/basic): remove some `eq.mpr`s from `int.induction_on'` (#12873)