add protected to deprecations

Author: kim-em

src/Init/Data/Int/DivModLemmas.lean

@@ -1272,8 +1272,8 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
 
 /-! ### Deprecations -/
 
-@[deprecated Int.zero_tdiv (since := "2024-09-11")] abbrev zero_div := @Int.zero_tdiv
-@[deprecated Int.tdiv_zero (since := "2024-09-11")] abbrev div_zero := @Int.tdiv_zero
+@[deprecated Int.zero_tdiv (since := "2024-09-11")] protected abbrev zero_div := @Int.zero_tdiv
+@[deprecated Int.tdiv_zero (since := "2024-09-11")] protected abbrev div_zero := @Int.tdiv_zero
 @[deprecated tdiv_eq_ediv (since := "2024-09-11")] abbrev div_eq_ediv := @tdiv_eq_ediv
 @[deprecated fdiv_eq_tdiv (since := "2024-09-11")] abbrev fdiv_eq_div := @fdiv_eq_tdiv
 @[deprecated zero_tmod (since := "2024-09-11")] abbrev zero_mod := @zero_tmod
@@ -1285,25 +1285,25 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
 @[deprecated tmod_def (since := "2024-09-11")] abbrev mod_def := @tmod_def
 @[deprecated tmod_eq_emod (since := "2024-09-11")] abbrev mod_eq_emod := @tmod_eq_emod
 @[deprecated fmod_eq_tmod (since := "2024-09-11")] abbrev fmod_eq_mod := @fmod_eq_tmod
-@[deprecated Int.tdiv_one (since := "2024-09-11")] abbrev div_one := @Int.tdiv_one
-@[deprecated Int.tdiv_neg (since := "2024-09-11")] abbrev div_neg := @Int.tdiv_neg
-@[deprecated Int.neg_tdiv (since := "2024-09-11")] abbrev neg_div := @Int.neg_tdiv
-@[deprecated Int.neg_tdiv_neg (since := "2024-09-11")] abbrev neg_div_neg := @Int.neg_tdiv_neg
-@[deprecated Int.tdiv_nonneg (since := "2024-09-11")] abbrev div_nonneg := @Int.tdiv_nonneg
-@[deprecated Int.tdiv_nonpos (since := "2024-09-11")] abbrev div_nonpos := @Int.tdiv_nonpos
+@[deprecated Int.tdiv_one (since := "2024-09-11")] protected abbrev div_one := @Int.tdiv_one
+@[deprecated Int.tdiv_neg (since := "2024-09-11")] protected abbrev div_neg := @Int.tdiv_neg
+@[deprecated Int.neg_tdiv (since := "2024-09-11")] protected abbrev neg_div := @Int.neg_tdiv
+@[deprecated Int.neg_tdiv_neg (since := "2024-09-11")] protected abbrev neg_div_neg := @Int.neg_tdiv_neg
+@[deprecated Int.tdiv_nonneg (since := "2024-09-11")] protected abbrev div_nonneg := @Int.tdiv_nonneg
+@[deprecated Int.tdiv_nonpos (since := "2024-09-11")] protected abbrev div_nonpos := @Int.tdiv_nonpos
 @[deprecated Int.tdiv_eq_zero_of_lt (since := "2024-09-11")] abbrev div_eq_zero_of_lt := @Int.tdiv_eq_zero_of_lt
-@[deprecated Int.mul_tdiv_cancel (since := "2024-09-11")] abbrev mul_div_cancel := @Int.mul_tdiv_cancel
-@[deprecated Int.mul_tdiv_cancel_left (since := "2024-09-11")] abbrev mul_div_cancel_left := @Int.mul_tdiv_cancel_left
-@[deprecated Int.tdiv_self (since := "2024-09-11")] abbrev div_self := @Int.tdiv_self
+@[deprecated Int.mul_tdiv_cancel (since := "2024-09-11")] protected abbrev mul_div_cancel := @Int.mul_tdiv_cancel
+@[deprecated Int.mul_tdiv_cancel_left (since := "2024-09-11")] protected abbrev mul_div_cancel_left := @Int.mul_tdiv_cancel_left
+@[deprecated Int.tdiv_self (since := "2024-09-11")] protected abbrev div_self := @Int.tdiv_self
 @[deprecated Int.mul_tdiv_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev mul_div_cancel_of_mod_eq_zero := @Int.mul_tdiv_cancel_of_tmod_eq_zero
 @[deprecated Int.tdiv_mul_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev div_mul_cancel_of_mod_eq_zero := @Int.tdiv_mul_cancel_of_tmod_eq_zero
 @[deprecated Int.dvd_of_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_of_mod_eq_zero := @Int.dvd_of_tmod_eq_zero
-@[deprecated Int.mul_tdiv_assoc (since := "2024-09-11")] abbrev mul_div_assoc := @Int.mul_tdiv_assoc
-@[deprecated Int.mul_tdiv_assoc' (since := "2024-09-11")] abbrev mul_div_assoc' := @Int.mul_tdiv_assoc'
+@[deprecated Int.mul_tdiv_assoc (since := "2024-09-11")] protected abbrev mul_div_assoc := @Int.mul_tdiv_assoc
+@[deprecated Int.mul_tdiv_assoc' (since := "2024-09-11")] protected abbrev mul_div_assoc' := @Int.mul_tdiv_assoc'
 @[deprecated Int.tdiv_dvd_tdiv (since := "2024-09-11")] abbrev div_dvd_div := @Int.tdiv_dvd_tdiv
 @[deprecated Int.natAbs_tdiv (since := "2024-09-11")] abbrev natAbs_div := @Int.natAbs_tdiv
-@[deprecated Int.tdiv_eq_of_eq_mul_right (since := "2024-09-11")] abbrev div_eq_of_eq_mul_right := @Int.tdiv_eq_of_eq_mul_right
-@[deprecated Int.eq_tdiv_of_mul_eq_right (since := "2024-09-11")] abbrev eq_div_of_mul_eq_right := @Int.eq_tdiv_of_mul_eq_right
+@[deprecated Int.tdiv_eq_of_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_right := @Int.tdiv_eq_of_eq_mul_right
+@[deprecated Int.eq_tdiv_of_mul_eq_right (since := "2024-09-11")] protected abbrev eq_div_of_mul_eq_right := @Int.eq_tdiv_of_mul_eq_right
 @[deprecated Int.ofNat_tmod (since := "2024-09-11")] abbrev ofNat_mod := @Int.ofNat_tmod
 @[deprecated Int.tmod_one (since := "2024-09-11")] abbrev mod_one := @Int.tmod_one
 @[deprecated Int.tmod_eq_of_lt (since := "2024-09-11")] abbrev mod_eq_of_lt := @Int.tmod_eq_of_lt
@@ -1316,18 +1316,18 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
 @[deprecated Int.dvd_iff_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_iff_mod_eq_zero := @Int.dvd_iff_tmod_eq_zero
 @[deprecated Int.neg_mul_tmod_right (since := "2024-09-11")] abbrev neg_mul_mod_right := @Int.neg_mul_tmod_right
 @[deprecated Int.neg_mul_tmod_left (since := "2024-09-11")] abbrev neg_mul_mod_left := @Int.neg_mul_tmod_left
-@[deprecated Int.tdiv_mul_cancel (since := "2024-09-11")] abbrev div_mul_cancel := @Int.tdiv_mul_cancel
-@[deprecated Int.mul_tdiv_cancel' (since := "2024-09-11")] abbrev mul_div_cancel' := @Int.mul_tdiv_cancel'
-@[deprecated Int.eq_mul_of_tdiv_eq_right (since := "2024-09-11")] abbrev eq_mul_of_div_eq_right := @Int.eq_mul_of_tdiv_eq_right
+@[deprecated Int.tdiv_mul_cancel (since := "2024-09-11")] protected abbrev div_mul_cancel := @Int.tdiv_mul_cancel
+@[deprecated Int.mul_tdiv_cancel' (since := "2024-09-11")] protected abbrev mul_div_cancel' := @Int.mul_tdiv_cancel'
+@[deprecated Int.eq_mul_of_tdiv_eq_right (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_right := @Int.eq_mul_of_tdiv_eq_right
 @[deprecated Int.tmod_self (since := "2024-09-11")] abbrev mod_self := @Int.tmod_self
 @[deprecated Int.neg_tmod_self (since := "2024-09-11")] abbrev neg_mod_self := @Int.neg_tmod_self
 @[deprecated Int.lt_tdiv_add_one_mul_self (since := "2024-09-11")] abbrev lt_div_add_one_mul_self := @Int.lt_tdiv_add_one_mul_self
-@[deprecated Int.tdiv_eq_iff_eq_mul_right (since := "2024-09-11")] abbrev div_eq_iff_eq_mul_right := @Int.tdiv_eq_iff_eq_mul_right
-@[deprecated Int.tdiv_eq_iff_eq_mul_left (since := "2024-09-11")] abbrev div_eq_iff_eq_mul_left := @Int.tdiv_eq_iff_eq_mul_left
-@[deprecated Int.eq_mul_of_tdiv_eq_left (since := "2024-09-11")] abbrev eq_mul_of_div_eq_left := @Int.eq_mul_of_tdiv_eq_left
-@[deprecated Int.tdiv_eq_of_eq_mul_left (since := "2024-09-11")] abbrev div_eq_of_eq_mul_left := @Int.tdiv_eq_of_eq_mul_left
-@[deprecated Int.eq_zero_of_tdiv_eq_zero (since := "2024-09-11")] abbrev eq_zero_of_div_eq_zero := @Int.eq_zero_of_tdiv_eq_zero
-@[deprecated Int.tdiv_left_inj (since := "2024-09-11")] abbrev div_left_inj := @Int.tdiv_left_inj
+@[deprecated Int.tdiv_eq_iff_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_right := @Int.tdiv_eq_iff_eq_mul_right
+@[deprecated Int.tdiv_eq_iff_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_left := @Int.tdiv_eq_iff_eq_mul_left
+@[deprecated Int.eq_mul_of_tdiv_eq_left (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_left := @Int.eq_mul_of_tdiv_eq_left
+@[deprecated Int.tdiv_eq_of_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_left := @Int.tdiv_eq_of_eq_mul_left
+@[deprecated Int.eq_zero_of_tdiv_eq_zero (since := "2024-09-11")] protected abbrev eq_zero_of_div_eq_zero := @Int.eq_zero_of_tdiv_eq_zero
+@[deprecated Int.tdiv_left_inj (since := "2024-09-11")] protected abbrev div_left_inj := @Int.tdiv_left_inj
 @[deprecated Int.tdiv_sign (since := "2024-09-11")] abbrev div_sign := @Int.tdiv_sign
-@[deprecated Int.sign_eq_tdiv_abs (since := "2024-09-11")] abbrev sign_eq_div_abs := @Int.sign_eq_tdiv_abs
+@[deprecated Int.sign_eq_tdiv_abs (since := "2024-09-11")] protected abbrev sign_eq_div_abs := @Int.sign_eq_tdiv_abs
 @[deprecated Int.tdiv_eq_ediv_of_dvd (since := "2024-09-11")] abbrev div_eq_ediv_of_dvd := @Int.tdiv_eq_ediv_of_dvd