Instance-swapping rw lemmas (filter_congr_decidable) can hit the wrong side

Lemmas such as Finset.filter_congr_decidable : filter p s = filter p s differ only in a hidden instance (the left side uses an explicit h : DecidablePred p, the right the ambient instance). Used with rw, the metavariable instance unifies with the FIRST filter p s that matches, which may be the side you did not intend. On Mathlib v4.35.0, for S p s = s.filter p where S is a classical-instance def, a bare rw [Finset.filter_congr_decidable] succeeds without error and the goal prints exactly as before. Only after unfold S does it close the goal. When the goal looks reflexive but won't close, prefer congr! or convert rfl: they handle the Decidable mismatch by subsingleton reasoning wherever it occurs. Use set_option pp.explicit true to see which instance each side carries.