data.rat.cast mathlib4#1261

Stream: mathlib4

[Ruben Van de Velde]

This one unsurprisingly has a bunch of issues. Help very much welcome

[Siddhartha Gadgil]

I have "fixed" many of the issues, but it has to be checked if the fix is correct.

• In many cases theorems with norm_cast attribute had no casting, so I removed the attribute (should the statement be changed instead?)
• A couple of proofs that were by norm_cast needed to use rw and apply with specific lemmas (which were no longer norm_cast
• In one case a statement had to be made more explicit.

[Siddhartha Gadgil]

All errors are now fixed. However someone should review to see that there is no accidental change in statement meanings.