Completeness of direct sums of Hilbert spaces?

Stream: Is there code for X?

[Scott Morrison]

Does anyone have code for the second example here:

import analysis.inner_product_space.pi_L2

noncomputable theory

variables (𝕜 : Type*) [is_R_or_C 𝕜] (H : Type*)

example [inner_product_space 𝕜 H] (ι : Type*) [fintype ι] :
  inner_product_space 𝕜 (pi_Lp 2 (λ i : ι, H)) := by apply_instance
example [inner_product_space 𝕜 H] [complete_space H] (ι : Type*) [fintype ι] :
  complete_space (pi_Lp 2 (λ i : ι, H)) := by apply_instance

[Heather Macbeth]

Does docs#Pi.complete do it?

[Heather Macbeth]

It seems so.

example [inner_product_space 𝕜 H] [complete_space H] (ι : Type*) [fintype ι] :
  complete_space (pi_Lp 2 (λ i : ι, H)) := Pi.complete (λ i : ι, H)

In the case of infinitely many Hilbert spaces, there's also docs#lp.complete_space

[Heather Macbeth]

I think the failure of apply_instance here is just the general wonkiness of typeclass inference for pi-types.