Commit 2024-03-26 23:09 5bc68d9f

View on Github →

chore(Data/Nat): Use Std lemmas (#11661) Move basic Nat lemmas from Data.Nat.Order.Basic and Data.Nat.Pow to Data.Nat.Defs. Most proofs need adapting, but that's easily solved by replacing the general mathlib lemmas by the new Std Nat-specific lemmas and using omega.

Other changes

  • Move the last few lemmas left in Data.Nat.Pow to Algebra.GroupPower.Order
  • Move the deprecated aliases from Data.Nat.Pow to Algebra.GroupPower.Order
  • Move the bit/bit0/bit1 lemmas from Data.Nat.Order.Basic to Data.Nat.Bits
  • Fix some fallout from not importing Data.Nat.Order.Basic anymore
  • Add a few Nat-specific lemmas to help fix the fallout (look for nolint simpNF)
  • Turn Nat.mul_self_le_mul_self_iff and Nat.mul_self_lt_mul_self_iff around (they were misnamed)
  • Make more arguments to Nat.one_lt_pow implicit

Estimated changes

added theorem StrictMono.nat_pow
added theorem Nat.bit0_le_bit1_iff
added theorem Nat.bit0_le_bit
added theorem Nat.bit0_lt_bit1_iff
added theorem Nat.bit1_le_bit0_iff
added theorem Nat.bit1_lt_bit0_iff
added theorem Nat.bit_le
added theorem Nat.bit_le_bit1
added theorem Nat.bit_lt_bit0
added theorem Nat.bit_lt_bit
added theorem Nat.add_eq_max_iff
added theorem Nat.add_eq_min_iff
added theorem Nat.add_eq_one_iff
added theorem Nat.add_eq_three_iff
added theorem Nat.add_eq_two_iff
added theorem Nat.add_mod_eq_ite
added theorem Nat.add_sub_one_le_mul
added theorem Nat.add_succ_lt_add
added theorem Nat.diag_induction
added theorem Nat.div_dvd_of_dvd
added theorem Nat.div_eq_self
added theorem Nat.div_eq_sub_mod_div
added theorem Nat.div_mul_div_le_div
added theorem Nat.dvd_sub_mod
added theorem Nat.eq_zero_of_le_div
added theorem Nat.eq_zero_of_le_half
added theorem Nat.eq_zero_of_mul_le
added theorem Nat.findGreatest_le
added theorem Nat.findGreatest_mono
added theorem Nat.findGreatest_pos
added theorem Nat.findGreatest_spec
added theorem Nat.find_add
added theorem Nat.find_pos
added theorem Nat.le_add_one_iff
added theorem Nat.le_add_pred_of_pos
added theorem Nat.le_findGreatest
added theorem Nat.le_mul_self
added theorem Nat.le_self_pow
added theorem Nat.lt_mul_self_iff
added theorem Nat.lt_of_lt_pred
added theorem Nat.lt_one_iff
added theorem Nat.lt_pow_self
added theorem Nat.lt_pred_iff
added theorem Nat.lt_two_pow
added theorem Nat.max_eq_zero_iff
added theorem Nat.min_eq_zero_iff
added theorem Nat.mod_mul_mod
added theorem Nat.mul_lt_mul''
added theorem Nat.mul_mod_mod
added theorem Nat.mul_self_inj
added theorem Nat.not_pos_pow_dvd
added theorem Nat.one_le_of_lt
added theorem Nat.one_le_pow'
added theorem Nat.one_le_pow
added theorem Nat.one_lt_pow'
added theorem Nat.one_lt_pow
added theorem Nat.one_lt_pow_iff
added theorem Nat.one_lt_two_pow'
added theorem Nat.one_mod
added theorem Nat.one_mod_of_ne_one
added theorem Nat.pow_left_injective
added theorem Nat.pow_mod
added theorem Nat.pred_le_iff
added theorem Nat.set_induction
added theorem Nat.sq_sub_sq
added theorem Nat.sub_succ'
added theorem Nat.succ_mul_pos
added theorem Nat.two_le_iff
added theorem Nat.two_pow_succ
modified theorem Nat.one_lt_factorial
modified theorem Nat.clog_zero_left
modified theorem Nat.clog_zero_right
modified theorem Nat.log_zero_left
deleted theorem Nat.add_eq_max_iff
deleted theorem Nat.add_eq_min_iff
deleted theorem Nat.add_eq_one_iff
deleted theorem Nat.add_eq_three_iff
deleted theorem Nat.add_eq_two_iff
deleted theorem Nat.add_mod_eq_ite
deleted theorem Nat.add_sub_one_le_mul
deleted theorem Nat.add_succ_lt_add
deleted theorem Nat.bit0_le_bit1_iff
deleted theorem Nat.bit0_le_bit
deleted theorem Nat.bit0_lt_bit1_iff
deleted theorem Nat.bit1_le_bit0_iff
deleted theorem Nat.bit1_lt_bit0_iff
deleted theorem Nat.bit_le
deleted theorem Nat.bit_le_bit1
deleted theorem Nat.bit_lt_bit0
deleted theorem Nat.bit_lt_bit
deleted theorem Nat.diag_induction
deleted theorem Nat.div_dvd_of_dvd
deleted theorem Nat.div_eq_self
deleted theorem Nat.div_eq_sub_mod_div
deleted theorem Nat.div_mul_div_le_div
deleted theorem Nat.dvd_sub_mod
deleted theorem Nat.eq_zero_of_double_le
deleted theorem Nat.eq_zero_of_le_div
deleted theorem Nat.eq_zero_of_le_half
deleted theorem Nat.eq_zero_of_mul_le
deleted theorem Nat.findGreatest_eq_iff
deleted theorem Nat.findGreatest_le
deleted theorem Nat.findGreatest_mono
deleted theorem Nat.findGreatest_pos
deleted theorem Nat.findGreatest_spec
deleted theorem Nat.find_add
deleted theorem Nat.find_pos
deleted theorem Nat.le_add_one_iff
deleted theorem Nat.le_add_pred_of_pos
deleted theorem Nat.le_and_le_add_one_iff
deleted theorem Nat.le_findGreatest
deleted theorem Nat.le_mul_self
deleted theorem Nat.lt_mul_self_iff
deleted theorem Nat.lt_of_lt_pred
deleted theorem Nat.lt_one_iff
deleted theorem Nat.lt_pred_iff
deleted theorem Nat.max_eq_zero_iff
deleted theorem Nat.min_eq_zero_iff
deleted theorem Nat.mul_self_inj
deleted theorem Nat.mul_self_le_mul_self
deleted theorem Nat.mul_self_lt_mul_self
deleted theorem Nat.not_dvd_of_pos_of_lt
deleted theorem Nat.one_le_of_lt
deleted theorem Nat.one_mod
deleted theorem Nat.one_mod_of_ne_one
deleted theorem Nat.pred_le_iff
deleted theorem Nat.set_induction
deleted theorem Nat.set_induction_bounded
deleted theorem Nat.sub_succ'
deleted theorem Nat.succ_mul_pos
deleted theorem Nat.two_le_iff
deleted theorem Nat.two_mul_odd_div_two
modified theorem NeZero.one_le
deleted theorem Nat.le_self_pow
deleted theorem Nat.lt_of_pow_dvd_right
deleted theorem Nat.lt_pow_self
deleted theorem Nat.lt_two_pow
deleted theorem Nat.mul_lt_mul_pow_succ
deleted theorem Nat.not_pos_pow_dvd
deleted theorem Nat.one_le_pow'
deleted theorem Nat.one_le_pow
deleted theorem Nat.one_lt_pow'
deleted theorem Nat.one_lt_pow
deleted theorem Nat.one_lt_pow_iff
deleted theorem Nat.one_lt_two_pow'
deleted theorem Nat.pow_left_injective
deleted theorem Nat.pow_mod
deleted theorem Nat.sq_sub_sq
deleted theorem Nat.two_pow_succ
deleted theorem StrictMono.nat_pow