Slow SecondCountableEither

Stream: mathlib4

[Patrick Massot]

Some performance issue both people who like to debug those:

import Mathlib.MeasureTheory.Measure.Haar.OfBasis

variable
  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H]


--set_option synthInstance.maxHeartbeats 100000
set_option trace.Meta.synthInstance.instances true in
example : SecondCountableTopologyEither ℝ (H →L[ℝ] E) := by
  infer_instance

[Patrick Massot]

(from the sphere eversion ongoing port)

[Matthew Ballard]

22000 suffices on the toolchain from lean4#2478 but infer_instance is doing tons of work there

[Matthew Ballard]

Does

attribute [-instance] FiniteDimensional.complexToReal

suffice on your toolchain?

[Patrick Massot]

Yes

[Yury G. Kudryashov]

Why do you need FiniteDimensional at all?

[Yury G. Kudryashov]

Does it try the second space first?