mathlib3

f5987b2a - chore(data/real/basic): tweak lemmas about `of_cauchy` (#12829)

chore(data/real/basic): tweak lemmas about `of_cauchy` (#12829) These lemmas are about `real.of_cauchy` not `real.cauchy`, as their name suggests. This also flips the direction of some of the lemmas to be consistent with the zero and one lemmas. Finally, this adds the lemmas about `real.cauchy` that are missing.