Commit 2022-11-20 00:17 4ee6f3d8

feat: port data.{nat, int}.cast.defs (#641) mathlib3 SHA: bb168510ef455e9280a152e7f31673cabd3d7496 Porting notes for Mathlib.Data.Nat.Cast.Defs

1. I have moved AddMonoidWithOne and related lemmas from Mathlib.Algebra.GroupWithZero.Defs into this file. All but 3 of these were in this file in mathlib3, so this is the correct place. The extra 3 are new lemmas in Mathlib4, and I made a note to this effect.
2. mathport marked some translations as dubious because they used AddMonoidWithOne instead of NatCast because the latter didn't exist until this PR, so I just fixed them to use NatCast and #aligned (with no ₓ).
3. I need someone (e.g., @gebner) to rewrite the library note about coercions because I don't know enough.
4. I reimplemented Nat.binCast from scratch because we don't have Nat.binaryRec. The proof of Nat.binCast_eq can likely be improved quite a bit.
5. I marked Nat.cast_bit0 and Nat.cast_bit1 as deprecated since bit0 and bit1 are deprecated.
6. I added an instance of OfNat R n for n : ℕ when R has an AddMonoidWithOne instance. I think we want this in order to talk about literals as terms in R (e.g., 37 : R). This instance does not appear in mathlib3 and is new.
7. I kept the (lack of) simp attributes from mathlib3 for certain lemmas which were already ported to mathlib4. This caused some breakage which I fixed. I thought it was better to be consistent with the mathlib3 simp set. Per Gabriel's suggestion, I have kept these as simp lemmas. Porting notes for Mathlib.Data.Int.Cast.Defs
8. This file already existed in Mathlib4, but it's contents corresponded to things in mathlib3's data.int.cast.basic, so I have moved the previous contents to Mathlib.Data.Int.Cast.Basic, hence the reason for the weird diff.
9. I have moved AddGroupWithOne and the rest of that material out of Mathlib.Algebra.GroupWithZero.Defs so these files are now independent and Mathlib.Data.Int.Cast.Defs I think is a faithful and complete translation of the mathlib3 file.