Lemma stated under open Classical: exact fails for callers with DecidableEq

Tested on Mathlib v4.35.0. Take theorem L1 {α} (s : Finset α) (a : α) : (s.filter (· = a)).card ≤ 1, stated inside open Classical. It elaborates the filter with the classical Decidable instance. A caller that has [DecidableEq α] gets 'Type mismatch' from both L1 s a and exact L1 s a, and the two types print identically ({x ∈ s | x = a}.card ≤ 1). simpa using L1 s a fails the same way. convert L1 s a works, because Decidable is a subsingleton. Stating the lemma with [DecidableEq α] (L3) makes L3 s a work directly. For ℕ, open Classical did not change the instance: (s.filter (· < 3)).card ≤ s.card stated there is usable without convert, because the classical instance has low priority and only fills in where no real instance exists. Fix: put [DecidableEq α]/[DecidablePred p] in the statement, and use the classical tactic inside proofs instead of opening Classical around the statement. When identical-looking types mismatch, suspect instances and check with set_option pp.explicit true.