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>

src/data/real/basic.lean

@@ -66,12 +66,15 @@ instance : has_one ℝ := ⟨one⟩
 instance : has_add ℝ := ⟨add⟩
 instance : has_neg ℝ := ⟨neg⟩
 instance : has_mul ℝ := ⟨mul⟩
+instance : has_sub ℝ := ⟨λ a b, a + (-b)⟩
 noncomputable instance : has_inv ℝ := ⟨inv'⟩
 
 lemma of_cauchy_zero : (⟨0⟩ : ℝ) = 0 := show _ = zero, by rw zero
 lemma of_cauchy_one : (⟨1⟩ : ℝ) = 1 := show _ = one, by rw one
 lemma of_cauchy_add (a b) : (⟨a + b⟩ : ℝ) = ⟨a⟩ + ⟨b⟩ := show _ = add _ _, by rw add
 lemma of_cauchy_neg (a) : (⟨-a⟩ : ℝ) = -⟨a⟩ := show _ = neg _, by rw neg
+lemma of_cauchy_sub (a b) : (⟨a - b⟩ : ℝ) = ⟨a⟩ - ⟨b⟩ :=
+by { rw [sub_eq_add_neg, of_cauchy_add, of_cauchy_neg], refl }
 lemma of_cauchy_mul (a b) : (⟨a * b⟩ : ℝ) = ⟨a⟩ * ⟨b⟩ := show _ = mul _ _, by rw mul
 lemma of_cauchy_inv {f} : (⟨f⁻¹⟩ : ℝ) = ⟨f⟩⁻¹ := show _ = inv' _, by rw inv'
 
@@ -83,17 +86,22 @@ lemma cauchy_neg : ∀ a, (-a : ℝ).cauchy = -a.cauchy
 | ⟨a⟩ := show (neg _).cauchy = _, by rw neg
 lemma cauchy_mul : ∀ a b, (a * b : ℝ).cauchy = a.cauchy * b.cauchy
 | ⟨a⟩ ⟨b⟩ := show (mul _ _).cauchy = _, by rw mul
+lemma cauchy_sub : ∀ a b, (a - b : ℝ).cauchy = a.cauchy - b.cauchy
+| ⟨a⟩ ⟨b⟩ := by { rw [sub_eq_add_neg, ←cauchy_neg, ←cauchy_add], refl }
 lemma cauchy_inv : ∀ f, (f⁻¹ : ℝ).cauchy = f.cauchy⁻¹
 | ⟨f⟩ := show (inv' _).cauchy = _, by rw inv'
 
-/-- `real.equiv_Cauchy` as a ring equivalence. -/
-@[simps]
-def ring_equiv_Cauchy : ℝ ≃+* cau_seq.completion.Cauchy abs :=
-{ to_fun := cauchy,
-  inv_fun := of_cauchy,
-  map_add' := cauchy_add,
-  map_mul' := cauchy_mul,
-  ..equiv_Cauchy }
+instance : has_nat_cast ℝ := { nat_cast := λ n, ⟨n⟩ }
+instance : has_int_cast ℝ := { int_cast := λ z, ⟨z⟩ }
+instance : has_rat_cast ℝ := { rat_cast := λ q, ⟨q⟩ }
+
+lemma of_cauchy_nat_cast (n : ℕ) : (⟨n⟩ : ℝ) = n := rfl
+lemma of_cauchy_int_cast (z : ℤ) : (⟨z⟩ : ℝ) = z := rfl
+lemma of_cauchy_rat_cast (q : ℚ) : (⟨q⟩ : ℝ) = q := rfl
+
+lemma cauchy_nat_cast (n : ℕ) : (n : ℝ).cauchy = n := rfl
+lemma cauchy_int_cast (z : ℤ) : (z : ℝ).cauchy = z := rfl
+lemma cauchy_rat_cast (q : ℚ) : (q : ℝ).cauchy = q := rfl
 
 instance : comm_ring ℝ :=
 begin
@@ -102,30 +110,28 @@ begin
                   mul   := (*),
                   add   := (+),
                   neg   := @has_neg.neg ℝ _,
-                  sub   := λ a b, a + (-b),
-                  nat_cast := λ n, ⟨n⟩,
-                  int_cast := λ n, ⟨n⟩,
+                  sub   := @has_sub.sub ℝ _,
                   npow  := @npow_rec ℝ ⟨1⟩ ⟨(*)⟩,
                   nsmul := @nsmul_rec ℝ ⟨0⟩ ⟨(+)⟩,
-                  zsmul := @zsmul_rec ℝ ⟨0⟩ ⟨(+)⟩ ⟨@has_neg.neg ℝ _⟩ };
+                  zsmul := @zsmul_rec ℝ ⟨0⟩ ⟨(+)⟩ ⟨@has_neg.neg ℝ _⟩,
+                  ..real.has_nat_cast,
+                  ..real.has_int_cast, };
   repeat { rintro ⟨_⟩, };
   try { refl };
   simp [← of_cauchy_zero, ← of_cauchy_one, ←of_cauchy_add, ←of_cauchy_neg, ←of_cauchy_mul,
-    λ n, show @coe ℕ ℝ ⟨_⟩ n = ⟨n⟩, from rfl];
+    λ n, show @coe ℕ ℝ ⟨_⟩ n = ⟨n⟩, from rfl, has_nat_cast.nat_cast, has_int_cast.int_cast];
   apply add_assoc <|> apply add_comm <|> apply mul_assoc <|> apply mul_comm <|>
     apply left_distrib <|> apply right_distrib <|> apply sub_eq_add_neg <|> skip,
 end
 
-
-instance : has_rat_cast ℝ := { rat_cast := λ q, ⟨q⟩ }
-
-lemma of_cauchy_nat_cast (n : ℕ) : (⟨n⟩ : ℝ) = n := rfl
-lemma of_cauchy_int_cast (z : ℤ) : (⟨z⟩ : ℝ) = z := rfl
-lemma of_cauchy_rat_cast (q : ℚ) : (⟨q⟩ : ℝ) = q := rfl
-
-lemma cauchy_nat_cast (n : ℕ) : (n : ℝ).cauchy = n := rfl
-lemma cauchy_int_cast (z : ℤ) : (z : ℝ).cauchy = z := rfl
-lemma cauchy_rat_cast (q : ℚ) : (q : ℝ).cauchy = q := rfl
+/-- `real.equiv_Cauchy` as a ring equivalence. -/
+@[simps]
+def ring_equiv_Cauchy : ℝ ≃+* cau_seq.completion.Cauchy abs :=
+{ to_fun := cauchy,
+  inv_fun := of_cauchy,
+  map_add' := cauchy_add,
+  map_mul' := cauchy_mul,
+  ..equiv_Cauchy }
 
 /-! Extra instances to short-circuit type class resolution.
 
@@ -149,7 +155,6 @@ instance : comm_monoid ℝ        := by apply_instance
 instance : monoid ℝ             := by apply_instance
 instance : comm_semigroup ℝ     := by apply_instance
 instance : semigroup ℝ          := by apply_instance
-instance : has_sub ℝ            := by apply_instance
 instance : inhabited ℝ          := ⟨0⟩
 
 /-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/