Help with Mathlib.Order.Interval.Finset.Defs

Stream: mathlib4

[Kim Morrison]

docs#WithTop.locallyFiniteOrder uses in its proofs deprecated lemmas such as docs#WithTop.some_le_some. Would anyone be interested in cleaning this up so we can finish removing the deprecated lemmas?

[Kim Morrison]

Pinging @Yaël Dillies as the author of the file, but Yael is often very busy so hopefully anyone interested will take a look!

[Ruben Van de Velde]

I've got half a fix

[Ruben Van de Velde]

So is it unsafe to tag deprecated lemmas with simp, because we won't notice they're used?

[Ruben Van de Velde]

#22477

[Ruben Van de Velde]

@Kim Morrison with a bit of luck, that'll build now. I have no more time right now, so feel free to take over

[Kim Morrison]

Ruben Van de Velde said:

So is it unsafe to tag deprecated lemmas with simp, because we won't notice they're used?

Yes, ideally @[simp] would be removed at the same time lemmas are deprecated. This is something for reviewers to watch out for.

We could, in fact, lint for this. Any takers? :-)

[Paul Lezeau]

Kim Morrison said:

Ruben Van de Velde said:

So is it unsafe to tag deprecated lemmas with simp, because we won't notice they're used?

Yes, ideally @[simp] would be removed at the same time lemmas are deprecated. This is something for reviewers to watch out for.

We could, in fact, lint for this. Any takers? :-)

I’d be happy to look into this :-)