Finset.range = Finset.Iio

Stream: Is there code for X?

[Terence Tao]

The following simple fact does not currently seem to be in Mathlib. Is it worth adding it (possibly even as a simp lemma)?

import Mathlib

example : Finset.range = Finset.Iio := by
  ext n m
  simp only [Finset.mem_range, Finset.mem_Iio]

[Yury G. Kudryashov]

See docs#Nat.Iio_eq_range

[Terence Tao]

OK, I have no idea how I missed that. Thanks.

EDIT: I reconstructed how I got here. I started withexample (n:ℕ) : Finset.range n = Finset.Iio n, which for some reason does not close by exact?, hint, or apply?, though aesop can handle it. Then I decided to delete the variable n without rechecking whether it now closed.

[Yury G. Kudryashov]

I think that we should drop Finset.range and use Finset.Iio, but I'm too lazy to do the refactor.

[Yaël Dillies]

The refactor already exists secretly: It's #11633

[Yaël Dillies]

Don't really have time to revive it at the moment, maybe in a few weeks

[Yury G. Kudryashov]

I used @loogle Finset.range, Finset.Iio

[loogle]

:search: Nat.Iio_eq_range

[Terence Tao]

I had searched within Mathlib for range Iio with no hits, but somehow it had not occurred to me to search for Iio range :laughing:

[Sébastien Gouëzel]

Do you know loogle? See https://loogle.lean-lang.org/?q=Finset.range%2C+Finset.Iio for instance.