Lemma about Finite Linear Ordered type

Stream: Is there code for X?

[Edison Xie]

Is this lemma already somewhere in Mathlib? A more important question is that do we allow lemmas with proof to be only by grind in mathlib?

import Mathlib

example {ι} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrderBot ι] [LocallyFiniteOrderTop ι]
    [DecidableEq ι] (i : ι) : (Finset.Iio i) ∪ (Finset.Ioi i) = Finset.univ \ {i} := by
  grind

[Edison Xie]

ps : looks like we don't have a lot about Finset.Iio?

[Artie Khovanov]

I don't know the answer to your first question, but the answer to your second one is yes, of course.

[Bhavik Mehta]

We have https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Interval/Finset/Basic.html#Finset.Ioi_disjUnion_Iio, and I think it ought to come with a ∪ version. But the right hand side should be written with compl rather than univ \

[Ruben Van de Velde]

I saw something like this just now

[Ruben Van de Velde]

docs#Iio_union_Ioi

[Ruben Van de Velde]

Ah, for Set only

[Bhavik Mehta]

Right, we should add the Finset version too. If either of you wants to make a little PR for that I'm happy to merge it quickly

[Miyahara Kō]

FYI, {i}ᶜ is preferable to Finset.univ \ {i}.

[Miyahara Kō]

When it is used as simp or grind lemmas. (even if it isn't used as simp or grind lemma)

[Edison Xie]

Miyahara Kō said:

FYI, {i}ᶜ is preferable to Finset.univ \ {i}.

What are the benefits of using compl?

[Miyahara Kō]

1. There are far more Finset lemmas for sᶜ than ones for Finset.univ \ s.
2. Rewriting x ∈ sᶜ to x ∉ s requires only one lemma(docs#Finset.mem_compl), rewriting x ∈ Finset.univ \ s to x ∉ s requires three lemmas(docs#Finset.mem_sdiff, docs#Finset.mem_univ, docs#true_and).
3. It is consistent with the Set lemma (docs#Set.Iio_union_Ioi).