## Stream: general

### Topic: Sup_range as simp

#### Violeta Hernández (Jul 02 2022 at 21:40):

I wanted to ask for a small RFC here. The theorem docs#Sup_range seems like a perfect candidate for a simp lemma at first glance. However, marking it as simp breaks the proofs of a handful (about half a dozen) simp lemmas about supr that amount to by simp [supr].

#### Violeta Hernández (Jul 02 2022 at 21:41):

You can see the sort of breakage it caused in #14918 (though a few of the changes are due to another lemma I marked as simp)

#### Violeta Hernández (Jul 02 2022 at 21:41):

Question: is this an indication that it shouldn't be simp? Or should I fix the proofs it breaks and mark it as simp?

#### Eric Wieser (Jul 02 2022 at 21:47):

I think we need a mechanism to say  ← foo is a simp lemma; as simp already knows how to reduce simp [foo, ←foo] to a safe application.

#### Violeta Hernández (Jul 02 2022 at 21:54):

How would that work in this case? ←supr would be marked as simp?

#### Eric Wieser (Jul 02 2022 at 22:18):

Either that, or simp could learn that Sup_range is an alias of supr.equations.<something>.symm

#### Eric Rodriguez (Jul 02 2022 at 22:39):

Eric Wieser said:

I think we need a mechanism to say  ← foo is a simp lemma; as simp already knows how to reduce simp [foo, ←foo] to a safe application.

how does it do this?

#### Yury G. Kudryashov (Jul 03 2022 at 12:53):

You can use simp [<- Sup_range]

#### Eric Wieser (Jul 03 2022 at 13:04):

It would be nicer if neither of the two different ways to spell that resulted in an infinite loop!

#### Anne Baanen (Jul 11 2022 at 10:35):

Eric Rodriguez said:

how does it do this?

Here's the relevant code: it looks for ← e where e is a constant or local constant, and removes all other applications of e. Definitely not the best way to do so, but it was the simplest way.

Last updated: Dec 20 2023 at 11:08 UTC