Commit 2023-11-19 20:53 693fd795

View on Github →

chore: replace exact_mod_cast tactic with mod_cast elaborator where possible (#8404) We still have the exact_mod_cast tactic, used in a few places, which somehow (?) works a little bit harder to prevent the expected type influencing the elaboration of the term. I would like to get to the bottom of this, and it will be easier once the only usages of exact_mod_cast are the ones that don't work using the term elaborator by itself.

Estimated changes

modified theorem Odd.nat_add_dvd_pow_add_pow
modified theorem Int.ceil_eq_on_Ioc'
modified theorem Int.ceil_nonneg
modified theorem Int.floor_sub_one
modified theorem Int.fract_add_one
modified theorem Int.fract_one_add
modified theorem Int.fract_sub_one
modified theorem Nat.floor_sub_one
modified theorem Nat.lt_one_of_floor_lt_one
modified theorem Nat.one_le_floor_iff
modified theorem round_add_nat
modified theorem round_sub_nat
modified theorem Complex.cpow_nat_mul
modified theorem Real.hasDerivAt_tan
modified theorem Real.hasStrictDerivAt_tan
modified theorem NNReal.pi_pos
modified theorem Real.cos_eq_zero_iff
modified theorem Complex.div_int_cast
modified theorem Complex.div_nat_cast
modified theorem Complex.div_rat_cast
modified theorem Finset.ssubset_iff
modified theorem Finsupp.support_eq_empty
modified theorem Int.cast_one_le_of_pos
modified theorem Irrational.ne_zero
modified theorem Real.toNNReal_eq_nat_cast
modified theorem Nat.pairwise_one_le_dist