refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_…

…C` is not an `instance` anymore (#10629)

This instance caused a search for `[finite_dimensional ?x E]` with an unknown `?x`. Turn it into a lemma and add `haveI` to some proofs. Also add an instance for `K ∙ x`.

src/analysis/inner_product_space/projection.lean

@@ -849,6 +849,7 @@ lemma submodule.finrank_add_inf_finrank_orthogonal {K₁ K₂ : submodule 𝕜 E
   finrank 𝕜 K₁ + finrank 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = finrank 𝕜 K₂ :=
 begin
   haveI := submodule.finite_dimensional_of_le h,
+  haveI := proper_is_R_or_C 𝕜 K₁,
   have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁ᗮ ⊓ K₂),
   rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
       submodule.sup_orthogonal_inf_of_complete_space h] at hd,
@@ -997,14 +998,29 @@ end orthogonal
 section orthogonal_family
 variables {ι : Type*}
 
+/-- An orthogonal family of subspaces of `E` satisfies `direct_sum.submodule_is_internal` (that is,
+they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
+orthogonal complement. -/
+lemma orthogonal_family.submodule_is_internal_iff_of_is_complete [decidable_eq ι]
+  {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 V) (hc : is_complete (↑(supr V) : set E)) :
+  direct_sum.submodule_is_internal V ↔ (supr V)ᗮ = ⊥ :=
+begin
+  haveI : complete_space ↥(supr V) := hc.complete_space_coe,
+  simp only [direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top, hV.independent,
+    true_and, submodule.orthogonal_eq_bot_iff]
+end
+
 /-- An orthogonal family of subspaces of `E` satisfies `direct_sum.submodule_is_internal` (that is,
 they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
 orthogonal complement. -/
 lemma orthogonal_family.submodule_is_internal_iff [decidable_eq ι] [finite_dimensional 𝕜 E]
   {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 V) :
   direct_sum.submodule_is_internal V ↔ (supr V)ᗮ = ⊥ :=
-by simp only [direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top, hV.independent,
-  true_and, submodule.orthogonal_eq_bot_iff]
+begin
+  haveI h := finite_dimensional.proper_is_R_or_C 𝕜 ↥(supr V),
+  exact hV.submodule_is_internal_iff_of_is_complete
+    (complete_space_coe_iff_is_complete.mp infer_instance)
+end
 
 end orthogonal_family
 
@@ -1116,6 +1132,7 @@ lemma maximal_orthonormal_iff_basis_of_finite_dimensional
   (hv : orthonormal 𝕜 (coe : v → E)) :
   (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ ∃ b : basis v 𝕜 E, ⇑b = coe :=
 begin
+  haveI := proper_is_R_or_C 𝕜 (span 𝕜 v),
   rw maximal_orthonormal_iff_orthogonal_complement_eq_bot hv,
   have hv_compl : is_complete (span 𝕜 v : set E) := (span 𝕜 v).complete_of_finite_dimensional,
   rw submodule.orthogonal_eq_bot_iff,

src/analysis/inner_product_space/rayleigh.lean

@@ -228,6 +228,7 @@ finite-dimensional vector space is an eigenvalue for that operator. -/
 lemma has_eigenvalue_supr_of_finite_dimensional (hT : is_self_adjoint T) :
   has_eigenvalue T ↑(⨆ x : {x : E // x ≠ 0}, is_R_or_C.re ⟪T x, x⟫ / ∥(x:E)∥ ^ 2) :=
 begin
+  haveI := finite_dimensional.proper_is_R_or_C 𝕜 E,
   let T' : E →L[𝕜] E := T.to_continuous_linear_map,
   have hT' : is_self_adjoint (T' : E →ₗ[𝕜] E) := hT,
   obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0,
@@ -250,6 +251,7 @@ finite-dimensional vector space is an eigenvalue for that operator. -/
 lemma has_eigenvalue_infi_of_finite_dimensional (hT : is_self_adjoint T) :
   has_eigenvalue T ↑(⨅ x : {x : E // x ≠ 0}, is_R_or_C.re ⟪T x, x⟫ / ∥(x:E)∥ ^ 2) :=
 begin
+  haveI := finite_dimensional.proper_is_R_or_C 𝕜 E,
   let T' : E →L[𝕜] E := T.to_continuous_linear_map,
   have hT' : is_self_adjoint (T' : E →ₗ[𝕜] E) := hT,
   obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0,

src/data/complex/is_R_or_C.lean

@@ -630,18 +630,25 @@ library_note "is_R_or_C instance"
     simp [re_add_im a, algebra.smul_def, algebra_map_eq_of_real]
   end⟩⟩
 
-/-- Over an `is_R_or_C` field, we can register the properness of finite-dimensional normed spaces as
-an instance. -/
-@[priority 900, nolint dangerous_instance] instance proper_is_R_or_C -- note [is_R_or_C instance]
-  {E : Type*} [normed_group E] [normed_space K E] [finite_dimensional K E] :
-  proper_space E :=
+variables (K) (E : Type*) [normed_group E] [normed_space K E]
+
+/-- A finite dimensional vector space Over an `is_R_or_C` is a proper metric space.
+
+This is not an instance because it would cause a search for `finite_dimensional ?x E` before
+`is_R_or_C ?x`. -/
+lemma proper_is_R_or_C [finite_dimensional K E] : proper_space E :=
 begin
   letI : normed_space ℝ E := restrict_scalars.normed_space ℝ K E,
   letI : is_scalar_tower ℝ K E := restrict_scalars.is_scalar_tower _ _ _,
   letI : finite_dimensional ℝ E := finite_dimensional.trans ℝ K E,
   apply_instance
 end
 
+variable {E}
+
+instance is_R_or_C.proper_space_span_singleton (x : E) : proper_space (K ∙ x) :=
+proper_is_R_or_C K (K ∙ x)
+
 end finite_dimensional
 
 section instances