Lean/Mathlib: goal 'Finset.filter p s = Finset.filter p s' that won't close is a Decidable instance mismatch
If a def is written under open Classical in (or uses Classical.propDecidable) and a lemma about it takes [DecidablePred p], the two Finset.filter terms carry different instances. On Mathlib v4.35.0: rfl fails, and simp [S] leaves the goal Finset.filter p s = Finset.filter p s, which looks reflexive but isn't (check with set_option pp.explicit true). Fixes that work: unfold S; congr, unfold S; convert rfl, unfold S; congr!, or rw [Finset.filter_congr_decidable]. Each closes the goal because Decidable is a subsingleton. The root fix in Mathlib style is to not bake Classical into definitions: take [DecidablePred p] as an argument and use the classical tactic only inside proofs.
Confirmed on Mathlib v4.35.0, with S p s defined via 'by classical exact s.filter p' and also via 'open Classical in': rfl fails; simp [S] leaves the reflexive-looking goal; unfold S; congr, unfold S; convert rfl and unfold S; congr! all close it. One precision: rw [Finset.filter_congr_decidable] also needs 'unfold S' first. Without it, rw matches the visible filter p s on the right-hand side, rewrites it to itself with no error, and leaves ⊢ S p s = filter p s unchanged. So read the list as 'unfold S; then any of …'.
Same issue with
Fintype.cardof a subtype{x // ∀ i : Fin n, P x i}. A general lemma (e.g. Chevalley–Warning's char_dvd_card_solutions_of_fintype_sum_lt) producesSubtype.fintype … Fintype.decidableForallFintype, while your goal elaborates withNat.decidableForallFin, soexactreports an application type mismatch. Fixes that compile on Mathlib v4.35.0:by convert h, orrw [Fintype.card_eq_nat_card] at h ⊢. Nat.card takes no instance argument, so the mismatch goes away for the rest of the proof.