chore(analysis/inner_product_space/dual): remove unneeded `complete_s…

…pace` assumption in four lemmas (#11578)

We remove the `[complete_space E]` assumption in four lemmas.

src/analysis/inner_product_space/dual.lean

@@ -60,7 +60,50 @@ lemma innerSL_norm [nontrivial E] : ∥(innerSL : E →L⋆[𝕜] E →L[𝕜] 
 show ∥(to_dual_map 𝕜 E).to_continuous_linear_map∥ = 1,
   from linear_isometry.norm_to_continuous_linear_map _
 
-variables (E) [complete_space E]
+variable (𝕜)
+include 𝕜
+lemma ext_inner_left {x y : E} (h : ∀ v, ⟪v, x⟫ = ⟪v, y⟫) : x = y :=
+begin
+  apply (to_dual_map 𝕜 E).map_eq_iff.mp,
+  ext v,
+  rw [to_dual_map_apply, to_dual_map_apply, ←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h v)
+end
+
+lemma ext_inner_right {x y : E} (h : ∀ v, ⟪x, v⟫ = ⟪y, v⟫) : x = y :=
+begin
+  refine ext_inner_left 𝕜 (λ v, _),
+  rw [←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h v)
+end
+omit 𝕜
+variable {𝕜}
+
+lemma ext_inner_left_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
+  (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y :=
+begin
+  apply (to_dual_map 𝕜 E).map_eq_iff.mp,
+  refine (function.injective.eq_iff continuous_linear_map.coe_injective).mp (basis.ext b _),
+  intro i,
+  simp only [to_dual_map_apply, continuous_linear_map.coe_coe],
+  rw [←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h i)
+end
+
+lemma ext_inner_right_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
+  (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y :=
+begin
+  refine ext_inner_left_basis b (λ i, _),
+  rw [←inner_conj_sym],
+  nth_rewrite_rhs 0 [←inner_conj_sym],
+  exact congr_arg conj (h i)
+end
+
+
+variables (𝕜) (E) [complete_space E]
 
 /--
 Fréchet-Riesz representation: any `ℓ` in the dual of a Hilbert space `E` is of the form
@@ -111,7 +154,7 @@ begin
     exact h₄ }
 end
 
-variables {E}
+variables {𝕜} {E}
 
 @[simp] lemma to_dual_apply {x y : E} : to_dual 𝕜 E x y = ⟪x, y⟫ := rfl
 
@@ -122,46 +165,4 @@ begin
   simp only [linear_isometry_equiv.apply_symm_apply],
 end
 
-variable (𝕜)
-include 𝕜
-lemma ext_inner_left {x y : E} (h : ∀ v, ⟪v, x⟫ = ⟪v, y⟫) : x = y :=
-begin
-  apply (to_dual 𝕜 E).map_eq_iff.mp,
-  ext v,
-  rw [to_dual_apply, to_dual_apply, ←inner_conj_sym],
-  nth_rewrite_rhs 0 [←inner_conj_sym],
-  exact congr_arg conj (h v)
-end
-
-lemma ext_inner_right {x y : E} (h : ∀ v, ⟪x, v⟫ = ⟪y, v⟫) : x = y :=
-begin
-  refine ext_inner_left 𝕜 (λ v, _),
-  rw [←inner_conj_sym],
-  nth_rewrite_rhs 0 [←inner_conj_sym],
-  exact congr_arg conj (h v)
-end
-omit 𝕜
-variable {𝕜}
-
-lemma ext_inner_left_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
-  (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y :=
-begin
-  apply (to_dual 𝕜 E).map_eq_iff.mp,
-  refine (function.injective.eq_iff continuous_linear_map.coe_injective).mp (basis.ext b _),
-  intro i,
-  simp only [to_dual_apply, continuous_linear_map.coe_coe],
-  rw [←inner_conj_sym],
-  nth_rewrite_rhs 0 [←inner_conj_sym],
-  exact congr_arg conj (h i)
-end
-
-lemma ext_inner_right_basis {ι : Type*} {x y : E} (b : basis ι 𝕜 E)
-  (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y :=
-begin
-  refine ext_inner_left_basis b (λ i, _),
-  rw [←inner_conj_sym],
-  nth_rewrite_rhs 0 [←inner_conj_sym],
-  exact congr_arg conj (h i)
-end
-
 end inner_product_space