Commit 2022-12-13 21:04 7d2d6ee6

View on Github →

chore: bump to get std4#63 (use Nat.cast in place of Int.ofNat) (#972) This verifies that https://github.com/leanprover/std4/pull/63 will work in mathlib4. Before merging this:

  • check that https://github.com/leanprover/std4/pull/63 has been merged
  • change lakefile.lean to point back to "main" for the std4 dependency
  • we may want to golf the proofs where I have added simp only [Int.ofNat_eq_coe], to combine these into the adjacent rw/simp.

Estimated changes

deleted theorem Int.coe_nat_le
deleted theorem Int.coe_nat_lt
modified theorem Int.coe_nat_nonneg
deleted theorem Int.ofNat_eq_coe