[Merged by Bors] - feat: port Data.Int.Cast.Basic

[j-loreaux]

mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Porting notes:

1. Some lemmas were transferred from Data.Int.Cast.Defs in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.)
2. The lemmas just mentioned have retained their simp attribute for the reason Gabriel mentioned on that PR ([Merged by Bors] - feat: port data.{nat, int}.cast.defs #641), even though that attribute isn't present on the mathlib3 version.
3. The bit0 and bit1 lemmas have been marked as deprecated.
4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have #aligned all of these with ₓ. I believe this is the correct thing to do, but confirmation would be nice.

---

• The first commit is the raw mathport output
• After getting the file to compile, I left one commit before I deleted the dubious translation warnings, so you can look at that to compare.

[j-loreaux]

@digama0 can you confirm for me that #align ...ₓ is the right thing to do in this situation?

[digama0]

I use the convention that any #align ...ₓ should have a short comment after it identifying why it's a dubious translation, e.g. reordered implicits, mismatching universes, Int.div alignment. In this case, I take it it's the typeclass args on the function? The answer to your question is probably yes, but it would be good to document the reason.

[gebner]

Suggested change

	#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ
	#align int.cast_neg_succ_of_nat Int.cast_negSucc

We definitely want to translate these without the ₓ. The only reason this statement is different is because coe is gone now, but this lemma is the closest approximation we've got in Lean 4. I think the statement is even defeq to the Lean 3 version.

(Note sure about the precise semantics of #align foo Fooₓ so maybe the ₓ does what I want.)

[j-loreaux]

There is no ₓ that appears in the final translation. The ₓ is just a signal to mathport that the types don't match and it should use the type of Foo downstream instead of foo.

I think in this case the dubious translations are arising mostly (if not entirely) from the fact that the nightly on which this mathport output was based came from a mathlib4 before I had ported Data.{Nat, Int}.Cast.Defs. I will check again when the next nightly comes out to see if these are still marked as dubious.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style