Problem with `EuclideanSpace ℂ ι` as `InnerProductSpace ℝ`

Stream: mathlib4

[Xavier Roblot]

import Mathlib

variable {ι : Type*} [Fintype ι]

example :
    (InnerProductSpace.complexToReal : InnerProductSpace ℝ (EuclideanSpace ℂ ι))
      = (PiLp.innerProductSpace _ : InnerProductSpace ℝ (EuclideanSpace ℂ ι)) := rfl -- fails

example :
    (InnerProductSpace.complexToReal : InnerProductSpace ℝ (EuclideanSpace ℂ ι))
      = (PiLp.innerProductSpace _ : InnerProductSpace ℝ (EuclideanSpace ℂ ι)) := by
  unfold InnerProductSpace.complexToReal PiLp.innerProductSpace
  congr!
  simp [real_inner_eq_re_inner] -- succeeds

This is causing some problems when trying to work with EuclideanSpace ℂ ι as an InnerProductSpace ℝ. For example, when I try to construct an orthonormal basis of EuclideanSpace ℂ ι using #12242, I get the error message:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  InnerProductSpace.complexToReal
inferred
  PiLp.innerProductSpace fun x ↦ ℂ

What is the best way to fix that?
(I guess the best fix would be for the rfl above to work, but I don't know how to do that.)

[Yaël Dillies]

Hmm, that looks bad

[Yaël Dillies]

docs#InnerProductSpace.complexToReal, docs#PiLp.innerProductSpace

[Yaël Dillies]

It boils down to re (sum i, inner (x i) (y i)) = sum i, re (inner (x i) (y i)) not being defeq

[Yaël Dillies]

Can we hope to make re (sum i in s, f i) = sum i in s, re (f i) defeq in general? I doubt so

[Xavier Roblot]

But then it means that docs#InnerProductSpace.complexToReal should not be an instance?

[Xavier Roblot]

#12840 : Change docs#InnerProductSpace.complexToReal to a def and add the instance

instance : InnerProductSpace ℝ ℂ := innerProductSpace.complexToReal

[Eric Wieser]

Most of these complexToReal instances are sort of bad, but the convenience usually outweighs this. This seems like an example where it doesn't

[Kevin Buzzard]

Given that mathlib compiles without it, I agree!