feat(data/complex/is_R_or_C): Create a proper coercion from ℝ (#4824)

This PR creates a proper coercion `ℝ → 𝕜` for `[is_R_or_C 𝕜]`, modelled on the code in `data/nat/cast`, as per the discussion [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Hilbert.20space.20is.20isometric.20to.20its.20dual).



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

src/analysis/normed_space/inner_product.lean

@@ -67,7 +67,6 @@ open is_R_or_C real
 open_locale big_operators classical
 
 variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
-local notation `𝓚` := @is_R_or_C.of_real 𝕜 _
 
 /-- Syntactic typeclass for types endowed with an inner product -/
 class has_inner (𝕜 E : Type*) := (inner : E → E → 𝕜)
@@ -148,9 +147,9 @@ variables [add_comm_group F] [semimodule 𝕜 F] [c : inner_product_space.core 
 include c
 
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 F _ x y
-local notation `𝓚` := @is_R_or_C.of_real 𝕜 _
 local notation `norm_sqK` := @is_R_or_C.norm_sq 𝕜 _
 local notation `reK` := @is_R_or_C.re 𝕜 _
+local notation `absK` := @is_R_or_C.abs 𝕜 _
 local notation `ext_iff` := @is_R_or_C.ext_iff 𝕜 _
 local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
 
@@ -177,7 +176,7 @@ c.add_left _ _ _
 lemma inner_add_right {x y z : F} : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ :=
 by rw [←inner_conj_sym, inner_add_left, ring_hom.map_add]; simp only [inner_conj_sym]
 
-lemma inner_norm_sq_eq_inner_self (x : F) : 𝓚 (norm_sqF x) = ⟪x, x⟫ :=
+lemma inner_norm_sq_eq_inner_self (x : F) : (norm_sqF x : 𝕜) = ⟪x, x⟫ :=
 begin
   rw ext_iff,
   exact ⟨by simp only [of_real_re]; refl, by simp only [inner_self_nonneg_im, of_real_im]⟩
@@ -204,7 +203,7 @@ by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_hom.map_zero]
 lemma inner_self_eq_zero {x : F} : ⟪x, x⟫ = 0 ↔ x = 0 :=
 iff.intro (c.definite _) (by { rintro rfl, exact inner_zero_left })
 
-lemma inner_self_re_to_K {x : F} : 𝓚 (re ⟪x, x⟫) = ⟪x, x⟫ :=
+lemma inner_self_re_to_K {x : F} : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by norm_num [ext_iff, inner_self_nonneg_im]
 
 lemma inner_abs_conj_sym {x y : F} : abs ⟪x, y⟫ = abs ⟪y, x⟫ :=
@@ -252,7 +251,7 @@ begin
       have : ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = 1 / ⟪y, y⟫ :=
         by rw [div_mul_eq_div_mul_one_div, div_self hy', one_mul],
       rw [this, div_eq_mul_inv, one_mul, ←div_eq_mul_inv] },
-    have h₄ : ⟪y, y⟫ = 𝓚 (re ⟪y, y⟫) := by simp only [inner_self_re_to_K],
+    have h₄ : ⟪y, y⟫ = re ⟪y, y⟫ := by simp only [inner_self_re_to_K],
     have h₅ : re ⟪y, y⟫ > 0,
     { refine lt_of_le_of_ne inner_self_nonneg _,
       intro H,
@@ -271,7 +270,7 @@ begin
                   : by field_simp [-mul_re, inner_conj_sym, hT, conj_div, h₁, h₃]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc]
-      ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / 𝓚 (re ⟪y, y⟫))
+      ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)
                   : by conv_lhs { rw [h₄] }
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫
                   : by rw [div_re_of_real]
@@ -378,6 +377,7 @@ variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 local notation `IK` := @is_R_or_C.I 𝕜 _
 local notation `absR` := _root_.abs
+local notation `absK` := @is_R_or_C.abs 𝕜 _
 local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
 local postfix `⋆`:90 := complex.conj
 
@@ -488,21 +488,21 @@ end
 lemma real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 :=
 by { have h := @inner_self_nonpos ℝ F _ _ x, simpa using h }
 
-@[simp] lemma inner_self_re_to_K {x : E} : 𝓚 (re ⟪x, x⟫) = ⟪x, x⟫ :=
+@[simp] lemma inner_self_re_to_K {x : E} : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by rw is_R_or_C.ext_iff; exact ⟨by simp, by simp [inner_self_nonneg_im]⟩
 
 lemma inner_self_re_abs {x : E} : re ⟪x, x⟫ = abs ⟪x, x⟫ :=
 begin
-  have H : ⟪x, x⟫ = 𝓚 (re ⟪x, x⟫) + 𝓚 (im ⟪x, x⟫) * I,
+  have H : ⟪x, x⟫ = (re ⟪x, x⟫ : 𝕜) + im ⟪x, x⟫ * I,
   { rw re_add_im, },
-  rw [H, is_add_hom.map_add re (𝓚 (re ⟪x, x⟫)) ((𝓚 (im ⟪x, x⟫)) * I)],
+  rw [H, is_add_hom.map_add re ((re ⟪x, x⟫) : 𝕜) (((im ⟪x, x⟫) : 𝕜) * I)],
   rw [mul_re, I_re, mul_zero, I_im, zero_sub, tactic.ring.add_neg_eq_sub],
   rw [of_real_re, of_real_im, sub_zero, inner_self_nonneg_im],
   simp only [abs_of_real, add_zero, of_real_zero, zero_mul],
   exact (_root_.abs_of_nonneg inner_self_nonneg).symm,
 end
 
-lemma inner_self_abs_to_K {x : E} : 𝓚 (abs ⟪x, x⟫) = ⟪x, x⟫ :=
+lemma inner_self_abs_to_K {x : E} : (absK ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
 by { rw[←inner_self_re_abs], exact inner_self_re_to_K }
 
 lemma real_inner_self_abs {x : F} : absR ⟪x, x⟫_ℝ = ⟪x, x⟫_ℝ :=
@@ -575,7 +575,7 @@ begin
       have : ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = 1 / ⟪y, y⟫ :=
         by rw [div_mul_eq_div_mul_one_div, div_self hy', one_mul],
       rw [this, div_eq_mul_inv, one_mul, ←div_eq_mul_inv] },
-    have h₄ : ⟪y, y⟫ = 𝓚 (re ⟪y, y⟫) := by simp,
+    have h₄ : ⟪y, y⟫ = re ⟪y, y⟫ := by simp,
     have h₅ : re ⟪y, y⟫ > 0,
     { refine lt_of_le_of_ne inner_self_nonneg _,
       intro H,
@@ -594,7 +594,7 @@ begin
                   : by field_simp [-mul_re, hT, conj_div, h₁, h₃, inner_conj_sym]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc]
-      ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / 𝓚 (re ⟪y, y⟫))
+      ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)
                   : by conv_lhs { rw [h₄] }
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫
                   : by rw [div_re_of_real]
@@ -868,7 +868,7 @@ end
 norms, has absolute value 1 if and only if they are nonzero and one is
 a multiple of the other. One form of equality case for Cauchy-Schwarz. -/
 lemma abs_inner_div_norm_mul_norm_eq_one_iff (x y : E) :
-  abs (⟪x, y⟫ / 𝓚 (∥x∥ * ∥y∥)) = 1 ↔ (x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x) :=
+  abs (⟪x, y⟫ / (∥x∥ * ∥y∥)) = 1 ↔ (x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x) :=
 begin
   split,
   { intro h,
@@ -878,18 +878,22 @@ begin
       norm_num at h,
       exact h },
     refine and.intro hx0 _,
-    set r := ⟪x, y⟫ / 𝓚 (∥x∥ * ∥x∥) with hr,
+    set r := ⟪x, y⟫ / (∥x∥ * ∥x∥) with hr,
     use r,
     set t := y - r • x with ht,
     have ht0 : ⟪x, t⟫ = 0,
-    { rw [ht, inner_sub_right, inner_smul_right, hr, ←inner_self_eq_norm_square, inner_self_re_to_K,
+    { rw [ht, inner_sub_right, inner_smul_right, hr],
+      norm_cast,
+      rw [←inner_self_eq_norm_square, inner_self_re_to_K,
           div_mul_cancel _ (λ h, hx0 (inner_self_eq_zero.1 h)), sub_self] },
     replace h : ∥r • x∥ / ∥t + r • x∥ = 1,
-    { rwa [←sub_add_cancel y (r • x), ←ht, inner_add_right, ht0, zero_add, inner_smul_right,
+    { rw [←sub_add_cancel y (r • x), ←ht, inner_add_right, ht0, zero_add, inner_smul_right,
         is_R_or_C.abs_div, is_R_or_C.abs_mul, ←inner_self_re_abs,
-        inner_self_eq_norm_square, of_real_mul, is_R_or_C.abs_mul, abs_of_real, abs_of_real,
-        abs_norm_eq_norm, abs_norm_eq_norm, ←mul_assoc, mul_comm,
-        mul_div_mul_left _ _ (λ h, hx0 (norm_eq_zero.1 h)), ←is_R_or_C.norm_eq_abs, ←norm_smul] at h },
+        inner_self_eq_norm_square] at h,
+      norm_cast at h,
+      rwa [_root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm, ←mul_assoc, mul_comm,
+        mul_div_mul_left _ _ (λ h, hx0 (norm_eq_zero.1 h)), ←is_R_or_C.norm_eq_abs,
+        ←norm_smul] at h },
     have hr0 : r ≠ 0,
     { intro hr0,
       rw [hr0, zero_smul, norm_zero, zero_div] at h,
@@ -899,7 +903,7 @@ begin
     { rw [eq_of_div_eq_one h] },
     replace h2 : ⟪r • x, r • x⟫ = ⟪t, t⟫ + ⟪t, r • x⟫ + ⟪r • x, t⟫ + ⟪r • x, r • x⟫,
     { rw [pow_two, pow_two, ←inner_self_eq_norm_square, ←inner_self_eq_norm_square ] at h2,
-      have h2' := congr_arg (λ z, 𝓚 z) h2,
+      have h2' := congr_arg (λ z : ℝ, (z : 𝕜)) h2,
       simp_rw [inner_self_re_to_K, inner_add_add_self] at h2',
       exact h2' },
     conv at h2 in ⟪r • x, t⟫ { rw [inner_smul_left, ht0, mul_zero] },
@@ -910,8 +914,9 @@ begin
     exact eq_of_sub_eq_zero ht.symm },
   { intro h,
     rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩,
-    rw hy,
-    rw [is_R_or_C.abs_div, abs_of_real, _root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm],
+    rw [hy, is_R_or_C.abs_div],
+    norm_cast,
+    rw [_root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm],
     exact abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr }
 end
 
@@ -920,7 +925,10 @@ norms, has absolute value 1 if and only if they are nonzero and one is
 a multiple of the other. One form of equality case for Cauchy-Schwarz. -/
 lemma abs_real_inner_div_norm_mul_norm_eq_one_iff (x y : F) :
   absR (⟪x, y⟫_ℝ / (∥x∥ * ∥y∥)) = 1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r ≠ 0 ∧ y = r • x) :=
-by simpa using abs_inner_div_norm_mul_norm_eq_one_iff x y
+begin
+  have := @abs_inner_div_norm_mul_norm_eq_one_iff ℝ F _ _ x y,
+  simpa [coe_real_eq_id] using this,
+end
 
 /--
 If the inner product of two vectors is equal to the product of their norms, then the two vectors
@@ -932,12 +940,14 @@ begin
   have hx0' : ∥x∥ ≠ 0 := by simp [norm_eq_zero, hx0],
   have hy0' : ∥y∥ ≠ 0 := by simp [norm_eq_zero, hy0],
   have hxy0 : ∥x∥ * ∥y∥ ≠ 0 := by simp [hx0', hy0'],
-  have h₁ : abs ⟪x, y⟫ = ∥x∥ * ∥y∥ ↔ abs (⟪x, y⟫ / 𝓚 (∥x∥ * ∥y∥)) = 1,
+  have h₁ : abs ⟪x, y⟫ = ∥x∥ * ∥y∥ ↔ abs (⟪x, y⟫ / (∥x∥ * ∥y∥)) = 1,
   { refine ⟨_ ,_⟩,
     { intro h,
+      norm_cast,
       rw [is_R_or_C.abs_div, h, abs_of_real, _root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm],
       exact div_self hxy0 },
     { intro h,
+      norm_cast at h,
       rwa [is_R_or_C.abs_div, abs_of_real, _root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm,
           div_eq_one_iff_eq hxy0] at h } },
   rw [h₁, abs_inner_div_norm_mul_norm_eq_one_iff x y],
@@ -1106,7 +1116,7 @@ def inner_product_space.is_R_or_C_to_real : inner_product_space ℝ E :=
     change re ⟪x + y, z⟫ = re ⟪x, z⟫ + re ⟪y, z⟫,
     simp [inner_add_left] },
   smul_left := λ x y r, by {
-    change re ⟪(algebra_map ℝ 𝕜 r) • x, y⟫ = r * re ⟪x, y⟫,
+    change re ⟪(r : 𝕜) • x, y⟫ = r * re ⟪x, y⟫,
     simp [inner_smul_left] },
   ..has_inner.is_R_or_C_to_real 𝕜,
   ..normed_space.restrict_scalars ℝ 𝕜 E }