fix(data/real/basic): provide a computable module instance (#8164)

Without this instance, `normed_field.to_normed_space` and `normed_space.to_module` is tried first, but this results in a noncomputable instance.





Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/real/basic.lean

@@ -76,7 +76,11 @@ begin
     apply left_distrib <|> apply right_distrib <|> apply sub_eq_add_neg <|> skip
 end
 
-/- Extra instances to short-circuit type class resolution -/
+/-! Extra instances to short-circuit type class resolution.
+
+ These short-circuits have an additional property of ensuring that a computable path is found; if
+ `field ℝ` is found first, then decaying it to these typeclasses would result in a `noncomputable`
+ version of them. -/
 instance : ring ℝ               := by apply_instance
 instance : comm_semiring ℝ      := by apply_instance
 instance : semiring ℝ           := by apply_instance
@@ -93,6 +97,7 @@ instance : monoid ℝ             := by apply_instance
 instance : comm_semigroup ℝ     := by apply_instance
 instance : semigroup ℝ          := by apply_instance
 instance : has_sub ℝ            := by apply_instance
+instance : module ℝ ℝ           := by apply_instance
 instance : inhabited ℝ          := ⟨0⟩
 
 /-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/

src/geometry/manifold/instances/real.lean

@@ -93,8 +93,10 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :
   end,
   right_inv'  := λx hx, update_eq_iff.2 ⟨max_eq_left hx, λ i _, rfl⟩,
   source_eq    := rfl,
-  unique_diff' := by simpa only [singleton_pi]
-    using unique_diff_on.pi (fin n) (λ _, ℝ) _ _ (λ i ∈ ({0} : set (fin n)), unique_diff_on_Ici 0),
+  unique_diff' :=
+    have this : unique_diff_on ℝ _ :=
+      unique_diff_on.pi (fin n) (λ _, ℝ) _ _ (λ i ∈ ({0} : set (fin n)), unique_diff_on_Ici 0),
+    by simpa only [singleton_pi] using this,
   continuous_to_fun  := continuous_subtype_val,
   continuous_inv_fun := continuous_subtype_mk _ $ continuous_id.update 0 $
     (continuous_apply 0).max continuous_const }
@@ -113,8 +115,10 @@ def model_with_corners_euclidean_quadrant (n : ℕ) :
   left_inv'   := λ ⟨xval, xprop⟩ hx, by { ext i, simp only [subtype.coe_mk, xprop i, max_eq_left] },
   right_inv' := λ x hx, by { ext1 i, simp only [hx i, max_eq_left] },
   source_eq    := rfl,
-  unique_diff' := by simpa only [pi_univ_Ici]
-    using unique_diff_on.univ_pi (fin n) (λ _, ℝ) _ (λ i, unique_diff_on_Ici 0),
+  unique_diff' :=
+    have this : unique_diff_on ℝ _ :=
+      unique_diff_on.univ_pi (fin n) (λ _, ℝ) _ (λ i, unique_diff_on_Ici 0),
+    by simpa only [pi_univ_Ici] using this,
   continuous_to_fun  := continuous_subtype_val,
   continuous_inv_fun := continuous_subtype_mk _ $ continuous_pi $ λ i,
     (continuous_id.max continuous_const).comp (continuous_apply i) }