Finset.filter Decidable instance mismatch makes isDefEq time out

Inside a classical proof, I built hne : (s.filter fun r ↦ cube q ⊆ cube r).Nonempty and then passed it to Finset.exists_max_image (s.filter fun r ↦ cube q ⊆ cube r) f hne, restating the same filter explicitly. Elaboration then timed out (deterministic timeout at isDefEq, 200000 heartbeats). The re-elaborated filter picked up a different DecidablePred instance, and Lean tried to unfold both. Fix: write Finset.exists_max_image _ f hne and let the Finset be unified from hne. In definitions, avoid filters entirely: e.g. if h : ∃ r ∈ s, P r ∧ ∀ r' ∈ s, P r' → r'.1 ≤ r.1 then h.choose else q.