simp trying to synth discrete topology

Stream: mathlib4

[Nailin Guan]

In #21424, after fixing the definition of limit in ProfiniteGrp, a time out was reached at Mathlib/FieldTheory/Galois/Profinite.lean line 306 by simp, which is trying to synth discrete topology when trying to prove a set is open.
I have two questions here:
1: What can be the possible reason causing the change in definition make the simp stop working? However after simp only the lemma that want to apply on it and simp again it worked, as seen in one of the commit.
2: I have another test

set_option trace.Meta.synthInstance true in
set_option trace.profiler true in
example : IsClosed ({1} : Set ℚ) := by
  simp
  sorry

It also tried to synth discrete topology, how can this be resolved? I tried to lower the priority of isOpen_discrete and isClosed_discrete

Maybe it is because I doesn't know how to trace simp process, can anyone help? Thanks.

[Aaron Liu]

You can do set_option trace.Meta.Tactic.simp true to trace simp.

[Aaron Liu]

In this case, it looks like the only lemma that applies is isClosed_discrete, so it tries that and fails.

[Kevin Buzzard]

There's no "a singleton is closed in a Hausdorff space" lemma?

[Aaron Liu]

There is, it just isn't @[simp].
docs#isClosed_singleton, and for Hausdorff spaces, docs#T2Space.t1Space