propose on a product space

Stream: mathlib4

[Floris van Doorn]

In the following code, the first example doesn't give any suggestions, while the second example gives some useful suggestions.

import Mathlib.Topology.SubsetProperties
import Mathlib.Tactic.Propose

example [TopologicalSpace X] [CompactSpace X] (K : Set (X × X)) (hK : IsClosed K) : False := by
  propose using hK -- no suggestions

example [TopologicalSpace X] [CompactSpace X] (K : Set X) (hK : IsClosed K) : False := by
  propose using hK -- multiple suggestions