Timeout in hasIntegral_iff

Stream: mathlib4

[Emilie (Shad Amethyst)]

I'm suddenly getting a timeout by the instance solver in hasIntegral_iff in Mathlib.Analysis.BoxIntegral.Basic, in my branch adri326/rubin: https://github.com/leanprover-community/mathlib4/actions/runs/7595165373/job/20687438795#step:12:2129

The CI worked in the previous commit, and I only introduced one instance for Infinite X in the offending commit

Taking a closer look at the theorem in question, it contains a tail simp call which can easily be replaced with a simp only, which solves the timeout. The trace is unfortunately unreadable with simp alone.
Increasing the maximum number of heartbeats makes the theorem pass, although it takes ~4s to do so.
When using simp only, it drops to 0.2s and doesn't require the number of heartbeats to be increased.

Is this worth opening a PR for? I can always remove the new instance introduced by my offending commit, but I doubt that this complex simp call won't get over the threshold again in the future as new instances get introduced here and there if it is left as-is.

[Emilie (Shad Amethyst)]

Ah well I'm getting another timeout in Counterexamples/Phillips.lean this time, over a tail simpa this time

[Emilie (Shad Amethyst)]

Ah, this one leads to a small MWE:

import Mathlib.Topology.ContinuousFunction.Bounded

open Topology
open Set BoundedContinuousFunction

class NoIsolatedPoints (α : Type*) [TopologicalSpace α] :=
  not_isolated' : ∀ p : α, Filter.NeBot (𝓝[≠] p)

instance {α : Type*} [TopologicalSpace α] [T1Space α] [NoIsolatedPoints α] [Nonempty α] : Infinite α := sorry

theorem causes_timeout {α : Type*} [TopologicalSpace α] [DiscreteTopology α] : Nontrivial (α →ᵇ ℝ) := by
  infer_instance

[Yury G. Kudryashov]

Did you try setting priority of the new instance to (a) 100; (b) 50?