simp unfolding `has_mem` for filters

Stream: general

[Yury G. Kudryashov]

simp only with no lemmas unfolds s ∈ f to s in f.sets. How can I prevent this?

[Mario Carneiro]

what does simplify.rewrite say?

[Yury G. Kudryashov]

#mwe:

import order.filter.basic

open filter

set_option trace.simplify.rewrite true
example (f₁ f₂ : filter ℕ) (s : set ℕ) : s ∈ f₁ ⊔ f₂ := by { simp only [mem_sup_sets],  }

Output:

6:62: 0. [simplify.rewrite] [filter.mem_sup_sets]: s ∈ (f₁ ⊔ f₂).sets ==> s ∈ f₁ ∧ s ∈ f₂

[Yury G. Kudryashov]

Tactic state after simp shows .sets

[Mario Carneiro]

By process of elimination, setting {proj := ff} turns off the behavior

[Mario Carneiro]

The problem is that filter.has_mem is marked @[reducible]

[Yury G. Kudryashov]

I'll try to remove this.