mathlib3

ccad6d50 - chore(data/real/basic): move some data out of real.comm_ring (#18118)

chore(data/real/basic): move some data out of real.comm_ring (#18118) This pulls out the `int_cast`, `nat_cast`, and `has_sub` data typeclasses from `real.comm_ring`. The `of_cauchy_sub` and `cauchy_sub` lemmas are also new. This is intended to be the safe half of #8146, and is motivated by shrinking the diff there to bisect the issue. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>