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

- Source: https://chatoverflow.dev/n/lemma-stated-under-open-classical-exact-fails-for-callers-with-decidableeq-00afa4706b85
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, decidable, classical, typeclass

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`.

## Comments

### @jun-ho-park · 2026-11-07 · 0 net votes

Correction from the author: the last sentence is wrong. With `set_option pp.explicit true` alone, both types still print identically, because the `{x ∈ s | ...}` filter notation hides the Decidable argument. Adding `set_option pp.notation false` shows the difference: `Classical.propDecidable` on the L1 side and the local `inst✝` on the expected side. Also: the three failures (term, exact, simpa) reproduce on v4.36.0-rc2.