fix(analysis/inner_product_space): make type families explicit for `o…

…rthogonal_family` and `is_hilbert_sum` (#18584)

Pretty much every single use of `orthogonal_family` was unable to infer this argument and so used `@`.
`is_hilbert_sum` is changed for consistency.

src/analysis/inner_product_space/basic.lean

@@ -1884,15 +1884,15 @@ product space structure on each of the submodules is important -- for example, w
 their Hilbert sum (`pi_lp V 2`).  For example, given an orthonormal set of vectors `v : ι → E`,
 we have an associated orthogonal family of one-dimensional subspaces of `E`, which it is convenient
 to be able to discuss using `ι → 𝕜` rather than `Π i : ι, span 𝕜 (v i)`. -/
-def orthogonal_family {G : ι → Type*} [Π i, inner_product_space 𝕜 (G i)] (V : Π i, G i →ₗᵢ[𝕜] E) :
+def orthogonal_family (G : ι → Type*) [Π i, inner_product_space 𝕜 (G i)] (V : Π i, G i →ₗᵢ[𝕜] E) :
   Prop :=
 ∀ ⦃i j⦄, i ≠ j → ∀ v : G i, ∀ w : G j, ⟪V i v, V j w⟫ = 0
 
 variables {𝕜} {G : ι → Type*} [Π i, inner_product_space 𝕜 (G i)] {V : Π i, G i →ₗᵢ[𝕜] E}
-  (hV : orthogonal_family 𝕜 V) [dec_V : Π i (x : G i), decidable (x ≠ 0)]
+  (hV : orthogonal_family 𝕜 G V) [dec_V : Π i (x : G i), decidable (x ≠ 0)]
 
 lemma orthonormal.orthogonal_family {v : ι → E} (hv : orthonormal 𝕜 v) :
-  @orthogonal_family 𝕜 _ _ _ _ (λ i : ι, 𝕜) _
+  orthogonal_family 𝕜 (λ i : ι, 𝕜)
     (λ i, linear_isometry.to_span_singleton 𝕜 E (hv.1 i)) :=
 λ i j hij a b, by simp [inner_smul_left, inner_smul_right, hv.2 hij]
 
@@ -1956,7 +1956,7 @@ end
 /-- The composition of an orthogonal family of subspaces with an injective function is also an
 orthogonal family. -/
 lemma orthogonal_family.comp {γ : Type*} {f : γ → ι} (hf : function.injective f) :
-  orthogonal_family 𝕜 (λ g : γ, (V (f g) : G (f g) →ₗᵢ[𝕜] E)) :=
+  orthogonal_family 𝕜 (λ g, G (f g)) (λ g, V (f g)) :=
 λ i j hij v w, hV (hf.ne hij) v w
 
 lemma orthogonal_family.orthonormal_sigma_orthonormal {α : ι → Type*} {v_family : Π i, (α i) → G i}
@@ -2055,7 +2055,7 @@ omit hV
 elements each from a different subspace in the family is linearly independent. In particular, the
 pairwise intersections of elements of the family are 0. -/
 lemma orthogonal_family.independent {V : ι → submodule 𝕜 E}
-  (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  (hV : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   complete_lattice.independent V :=
 begin
   classical,
@@ -2075,7 +2075,7 @@ end
 
 include dec_ι
 lemma direct_sum.is_internal.collected_basis_orthonormal {V : ι → submodule 𝕜 E}
-  (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ))
+  (hV : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ))
   (hV_sum : direct_sum.is_internal (λ i, V i))
   {α : ι → Type*}
   {v_family : Π i, basis (α i) 𝕜 (V i)} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
@@ -2366,8 +2366,7 @@ begin
 end
 
 lemma submodule.orthogonal_family_self :
-  @orthogonal_family 𝕜 E _ _ _ (λ b, ((cond b K Kᗮ : submodule 𝕜 E) : Type*)) _
-  (λ b, (cond b K Kᗮ).subtypeₗᵢ)
+  orthogonal_family 𝕜 (λ b, ↥(cond b K Kᗮ)) (λ b, (cond b K Kᗮ).subtypeₗᵢ)
 | tt tt := absurd rfl
 | tt ff := λ _ x y, submodule.inner_right_of_mem_orthogonal x.prop y.prop
 | ff tt := λ _ x y, submodule.inner_left_of_mem_orthogonal y.prop x.prop

src/analysis/inner_product_space/l2_space.lean

@@ -16,7 +16,7 @@ dependent functions `f : Π i, G i` for which `∑' i, ‖f i‖ ^ 2`, the sum o
 summable.  This construction is sometimes called the *Hilbert sum* of the family `G`.  By choosing
 `G` to be `ι → 𝕜`, the Hilbert space `ℓ²(ι, 𝕜)` may be seen as a special case of this construction.
 
-We also define a *predicate* `is_hilbert_sum 𝕜 E V`, where `V : Π i, G i →ₗᵢ[𝕜] E`, expressing that
+We also define a *predicate* `is_hilbert_sum 𝕜 G V`, where `V : Π i, G i →ₗᵢ[𝕜] E`, expressing that
 `V` is an `orthogonal_family` and that the associated map `lp G 2 →ₗᵢ[𝕜] E` is surjective.
 
 ## Main definitions
@@ -28,7 +28,7 @@ We also define a *predicate* `is_hilbert_sum 𝕜 E V`, where `V : Π i, G i →
 
 * `is_hilbert_sum`: Given a Hilbert space `E`, a family `G` of inner product
   spaces and a family `V : Π i, G i →ₗᵢ[𝕜] E` of isometric embeddings of the `G i` into `E`,
-  `is_hilbert_sum 𝕜 E V` means that `V` is an `orthogonal_family` and that the above
+  `is_hilbert_sum 𝕜 G V` means that `V` is an `orthogonal_family` and that the above
   linear isometry is surjective.
 
 * `is_hilbert_sum.linear_isometry_equiv`: If a Hilbert space `E` is a Hilbert sum of the
@@ -167,7 +167,7 @@ end lp
 /-! ### Identification of a general Hilbert space `E` with a Hilbert sum -/
 
 namespace orthogonal_family
-variables {V : Π i, G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 V)
+variables {V : Π i, G i →ₗᵢ[𝕜] E} (hV : orthogonal_family 𝕜 G V)
 
 include cplt hV
 
@@ -253,7 +253,7 @@ end orthogonal_family
 
 section is_hilbert_sum
 
-variables (𝕜 E) (V : Π i, G i →ₗᵢ[𝕜] E) (F : ι → submodule 𝕜 E)
+variables (𝕜 G) (V : Π i, G i →ₗᵢ[𝕜] E) (F : ι → submodule 𝕜 E)
 include cplt
 
 /-- Given a family of Hilbert spaces `G : ι → Type*`, a Hilbert sum of `G` consists of a Hilbert
@@ -263,17 +263,17 @@ space `E` and an orthogonal family `V : Π i, G i →ₗᵢ[𝕜] E` such that t
 Keeping in mind that `lp G 2` is "the" external Hilbert sum of `G : ι → Type*`, this is analogous
 to `direct_sum.is_internal`, except that we don't express it in terms of actual submodules. -/
 @[protect_proj] structure is_hilbert_sum : Prop := of_surjective ::
-(orthogonal_family : orthogonal_family 𝕜 V)
+(orthogonal_family : orthogonal_family 𝕜 G V)
 (surjective_isometry : function.surjective (orthogonal_family.linear_isometry))
 
-variables {𝕜 E V}
+variables {𝕜 G V}
 
 /-- If `V : Π i, G i →ₗᵢ[𝕜] E` is an orthogonal family such that the supremum of the ranges of
 `V i` is dense, then `(E, V)` is a Hilbert sum of `G`. -/
 lemma is_hilbert_sum.mk [Π i, complete_space $ G i]
-  (hVortho : orthogonal_family 𝕜 V)
+  (hVortho : orthogonal_family 𝕜 G V)
   (hVtotal : ⊤ ≤ (⨆ i, (V i).to_linear_map.range).topological_closure) :
-  is_hilbert_sum 𝕜 E V :=
+  is_hilbert_sum 𝕜 G V :=
 { orthogonal_family := hVortho,
   surjective_isometry :=
   begin
@@ -284,16 +284,16 @@ lemma is_hilbert_sum.mk [Π i, complete_space $ G i]
 
 /-- This is `orthogonal_family.is_hilbert_sum` in the case of actual inclusions from subspaces. -/
 lemma is_hilbert_sum.mk_internal [Π i, complete_space $ F i]
-  (hFortho : @orthogonal_family 𝕜 E _ _ _ (λ i, F i) _ (λ i, (F i).subtypeₗᵢ))
+  (hFortho : orthogonal_family 𝕜 (λ i, F i) (λ i, (F i).subtypeₗᵢ))
   (hFtotal : ⊤ ≤ (⨆ i, (F i)).topological_closure) :
-  @is_hilbert_sum _ 𝕜 _ E _ _ (λ i, F i) _ (λ i, (F i).subtypeₗᵢ) :=
+  is_hilbert_sum 𝕜 (λ i, F i) (λ i, (F i).subtypeₗᵢ) :=
 is_hilbert_sum.mk hFortho (by simpa [subtypeₗᵢ_to_linear_map, range_subtype] using hFtotal)
 
 /-- *A* Hilbert sum `(E, V)` of `G` is canonically isomorphic to *the* Hilbert sum of `G`,
 i.e `lp G 2`.
 
 Note that this goes in the opposite direction from `orthogonal_family.linear_isometry`. -/
-noncomputable def is_hilbert_sum.linear_isometry_equiv (hV : is_hilbert_sum 𝕜 E V) :
+noncomputable def is_hilbert_sum.linear_isometry_equiv (hV : is_hilbert_sum 𝕜 G V) :
   E ≃ₗᵢ[𝕜] lp G 2 :=
 linear_isometry_equiv.symm $
 linear_isometry_equiv.of_surjective
@@ -302,31 +302,31 @@ hV.orthogonal_family.linear_isometry hV.surjective_isometry
 /-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`. -/
 protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply
-  (hV : is_hilbert_sum 𝕜 E V) (w : lp G 2) :
+  (hV : is_hilbert_sum 𝕜 G V) (w : lp G 2) :
   hV.linear_isometry_equiv.symm w = ∑' i, V i (w i) :=
 by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.linear_isometry_apply]
 
 /-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
 a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`, and this
 sum indeed converges. -/
 protected lemma is_hilbert_sum.has_sum_linear_isometry_equiv_symm
-  (hV : is_hilbert_sum 𝕜 E V) (w : lp G 2) :
+  (hV : is_hilbert_sum 𝕜 G V) (w : lp G 2) :
   has_sum (λ i, V i (w i)) (hV.linear_isometry_equiv.symm w) :=
 by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.has_sum_linear_isometry]
 
 /-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
 `lp G 2`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
 associated element in `E`. -/
 @[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply_single
-  (hV : is_hilbert_sum 𝕜 E V) {i : ι} (x : G i) :
+  (hV : is_hilbert_sum 𝕜 G V) {i : ι} (x : G i) :
   hV.linear_isometry_equiv.symm (lp.single 2 i x) = V i x :=
 by simp [is_hilbert_sum.linear_isometry_equiv, orthogonal_family.linear_isometry_apply_single]
 
 /-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
 `lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
 elements of `E`. -/
 @[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_symm_apply_dfinsupp_sum_single
-  (hV : is_hilbert_sum 𝕜 E V) (W₀ : Π₀ (i : ι), G i) :
+  (hV : is_hilbert_sum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
   hV.linear_isometry_equiv.symm (W₀.sum (lp.single 2)) = (W₀.sum (λ i, V i)) :=
 by simp [is_hilbert_sum.linear_isometry_equiv,
   orthogonal_family.linear_isometry_apply_dfinsupp_sum_single]
@@ -335,7 +335,7 @@ by simp [is_hilbert_sum.linear_isometry_equiv,
 `lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
 elements of `E`. -/
 @[simp] protected lemma is_hilbert_sum.linear_isometry_equiv_apply_dfinsupp_sum_single
-  (hV : is_hilbert_sum 𝕜 E V) (W₀ : Π₀ (i : ι), G i) :
+  (hV : is_hilbert_sum 𝕜 G V) (W₀ : Π₀ (i : ι), G i) :
   (hV.linear_isometry_equiv (W₀.sum (λ i, V i)) : Π i, G i) = W₀ :=
 begin
   rw ← hV.linear_isometry_equiv_symm_apply_dfinsupp_sum_single,
@@ -348,19 +348,17 @@ end
 the family of linear isometries `λ i, λ k, k • v i`. -/
 lemma orthonormal.is_hilbert_sum {v : ι → E} (hv : orthonormal 𝕜 v)
   (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) :
-  @is_hilbert_sum _ 𝕜 _ _ _ _ (λ i : ι, 𝕜) _
-    (λ i, linear_isometry.to_span_singleton 𝕜 E (hv.1 i)) :=
+  is_hilbert_sum 𝕜 (λ i : ι, 𝕜) (λ i, linear_isometry.to_span_singleton 𝕜 E (hv.1 i)) :=
 is_hilbert_sum.mk hv.orthogonal_family
 begin
   convert hsp,
   simp [← linear_map.span_singleton_eq_range, ← submodule.span_Union],
 end
 
 lemma submodule.is_hilbert_sum_orthogonal (K : submodule 𝕜 E) [hK : complete_space K] :
-  @is_hilbert_sum _ 𝕜 _ E _ _ (λ b, ((cond b K Kᗮ : submodule 𝕜 E) : Type*)) _
-  (λ b, (cond b K Kᗮ).subtypeₗᵢ) :=
+  is_hilbert_sum 𝕜 (λ b, ↥(cond b K Kᗮ)) (λ b, (cond b K Kᗮ).subtypeₗᵢ) :=
 begin
-  haveI : Π b, complete_space ((cond b K Kᗮ : submodule 𝕜 E) : Type*),
+  haveI : Π b, complete_space ↥(cond b K Kᗮ),
   { intro b,
     cases b;
     exact orthogonal.complete_space K <|> assumption },

src/analysis/inner_product_space/pi_L2.lean

@@ -142,7 +142,7 @@ lemma euclidean_space.inner_eq_star_dot_product (x y : euclidean_space 𝕜 ι)
 from `E` to `pi_Lp 2` of the subspaces equipped with the `L2` inner product. -/
 def direct_sum.is_internal.isometry_L2_of_orthogonal_family
   [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V)
-  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   E ≃ₗᵢ[𝕜] pi_Lp 2 (λ i, V i) :=
 begin
   let e₁ := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ i, V i),
@@ -160,7 +160,7 @@ end
 
 @[simp] lemma direct_sum.is_internal.isometry_L2_of_orthogonal_family_symm_apply
   [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V)
-  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ))
+  (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ))
   (w : pi_Lp 2 (λ i, V i)) :
   (hV.isometry_L2_of_orthogonal_family hV').symm w = ∑ i, (w i : E) :=
 begin
@@ -592,7 +592,7 @@ variables {A : ι → submodule 𝕜 E}
 of the components of the direct sum, the disjoint union of these orthonormal bases is an
 orthonormal basis for `M`. -/
 noncomputable def direct_sum.is_internal.collected_orthonormal_basis
-  (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, A i) _ (λ i, (A i).subtypeₗᵢ))
+  (hV : orthogonal_family 𝕜 (λ i, A i) (λ i, (A i).subtypeₗᵢ))
   [decidable_eq ι] (hV_sum : direct_sum.is_internal (λ i, A i)) {α : ι → Type*}
   [Π i, fintype (α i)] (v_family : Π i, orthonormal_basis (α i) 𝕜 (A i)) :
   orthonormal_basis (Σ i, α i) 𝕜 E :=
@@ -602,7 +602,7 @@ by simpa using hV.orthonormal_sigma_orthonormal
 
 lemma direct_sum.is_internal.collected_orthonormal_basis_mem [decidable_eq ι]
   (h : direct_sum.is_internal A) {α : ι → Type*}
-  [Π i, fintype (α i)] (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, A i) _ (λ i, (A i).subtypeₗᵢ))
+  [Π i, fintype (α i)] (hV : orthogonal_family 𝕜 (λ i, A i) (λ i, (A i).subtypeₗᵢ))
   (v : Π i, orthonormal_basis (α i) 𝕜 (A i)) (a : Σ i, α i) :
   h.collected_orthonormal_basis hV v a ∈ A a.1 :=
 by simp [direct_sum.is_internal.collected_orthonormal_basis]
@@ -687,15 +687,15 @@ variables {n : ℕ} (hn : finrank 𝕜 E = n) [decidable_eq ι]
 /-- Exhibit a bijection between `fin n` and the index set of a certain basis of an `n`-dimensional
 inner product space `E`.  This should not be accessed directly, but only via the subsequent API. -/
 @[irreducible] def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv
-  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   (Σ i, fin (finrank 𝕜 (V i))) ≃ fin n :=
 let b := hV.collected_orthonormal_basis hV' (λ i, (std_orthonormal_basis 𝕜 (V i))) in
 fintype.equiv_fin_of_card_eq $ (finite_dimensional.finrank_eq_card_basis b.to_basis).symm.trans hn
 
 /-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct
 sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. -/
 @[irreducible] def direct_sum.is_internal.subordinate_orthonormal_basis
-  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   orthonormal_basis (fin n) 𝕜 E :=
 ((hV.collected_orthonormal_basis hV' (λ i, (std_orthonormal_basis 𝕜 (V i)))).reindex
   (hV.sigma_orthonormal_basis_index_equiv hn hV'))
@@ -704,13 +704,13 @@ sum has an orthonormal basis indexed by `fin n` and subordinate to that direct s
 sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. This function
 provides the mapping by which it is subordinate. -/
 @[irreducible] def direct_sum.is_internal.subordinate_orthonormal_basis_index
-  (a : fin n) (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) : ι :=
+  (a : fin n) (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) : ι :=
 ((hV.sigma_orthonormal_basis_index_equiv hn hV').symm a).1
 
 /-- The basis constructed in `orthogonal_family.subordinate_orthonormal_basis` is subordinate to
 the `orthogonal_family` in question. -/
 lemma direct_sum.is_internal.subordinate_orthonormal_basis_subordinate
-  (a : fin n) (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  (a : fin n) (hV' : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   (hV.subordinate_orthonormal_basis hn hV' a) ∈
   V (hV.subordinate_orthonormal_basis_index hn a hV') :=
 by simpa only [direct_sum.is_internal.subordinate_orthonormal_basis,

src/analysis/inner_product_space/projection.lean

@@ -1155,7 +1155,7 @@ variables {ι : Type*}
 they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
 orthogonal complement. -/
 lemma orthogonal_family.is_internal_iff_of_is_complete [decidable_eq ι]
-  {V : ι → submodule 𝕜 E} (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ))
+  {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ))
   (hc : is_complete (↑(supr V) : set E)) :
   direct_sum.is_internal V ↔ (supr V)ᗮ = ⊥ :=
 begin
@@ -1168,7 +1168,7 @@ end
 they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
 orthogonal complement. -/
 lemma orthogonal_family.is_internal_iff [decidable_eq ι] [finite_dimensional 𝕜 E]
-  {V : ι → submodule 𝕜 E} (hV : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
+  {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ i, V i) (λ i, (V i).subtypeₗᵢ)) :
   direct_sum.is_internal V ↔ (supr V)ᗮ = ⊥ :=
 begin
   haveI h := finite_dimensional.proper_is_R_or_C 𝕜 ↥(supr V),

src/analysis/inner_product_space/spectrum.lean

@@ -76,7 +76,7 @@ end
 
 /-- The eigenspaces of a self-adjoint operator are mutually orthogonal. -/
 lemma orthogonal_family_eigenspaces :
-  @orthogonal_family 𝕜 _ _ _ _ (λ μ, eigenspace T μ) _ (λ μ, (eigenspace T μ).subtypeₗᵢ) :=
+  orthogonal_family 𝕜 (λ μ, eigenspace T μ) (λ μ, (eigenspace T μ).subtypeₗᵢ) :=
 begin
   rintros μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩,
   by_cases hv' : v = 0,
@@ -88,8 +88,7 @@ begin
 end
 
 lemma orthogonal_family_eigenspaces' :
-  @orthogonal_family 𝕜 _ _ _ _ (λ μ : eigenvalues T, eigenspace T μ) _
-    (λ μ, (eigenspace T μ).subtypeₗᵢ) :=
+  orthogonal_family 𝕜 (λ μ : eigenvalues T, eigenspace T μ) (λ μ, (eigenspace T μ).subtypeₗᵢ) :=
 hT.orthogonal_family_eigenspaces.comp subtype.coe_injective
 
 /-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner