subset_refl and subset_empty_iff

Stream: mathlib4

[Peter Nelson]

Is there a reason that neither of these are simp?

[Johan Commelin]

docs#subset_refl and docs#subset_empty_iff

[Johan Commelin]

Especially the 2nd one seems like a good simp lemma to me.

[Johan Commelin]

@Peter Nelson Please make a PR. And comment !bench on it. Then we can see if there are any bad consequences.

[Peter Nelson]

#15110

[Richard Copley]

A few proofs with non-terminal simp were failing. I pushed fixes for those. Now there is a linter error with Finset.Subset.refl: it is a simp lemma but simp only [@subset_refl] can prove it. What's the best thing to do? Increase the priority of Finset.Subset.refl?

[Kevin Buzzard]

Remove the @[simp] tag from Finset.Subset.refl?

[Richard Copley]

/poll What's the best thing to do?
Increase the priority of Finset.Subset.refl
Remove the @[simp] tag from Finset.Subset.refl

[Damiano Testa]

My rule of thumb is that you should prioritise not changing priorities: if an alternative fix is available, it is almost certainly better.

[Richard Copley]

Thanks, here goes

[Richard Copley]

All checks passed. Still want a !bench? I have a feeling there will be no significant differences