## Stream: general

### Topic: squeeze_dsimp?

#### Scott Morrison (May 03 2019 at 18:15):

Is there any prospect, @Simon Hudon, of writing a squeeze_dsimp? I would find this very useful when debugging dsimp, simp, dsimp, simp fiascos.

#### Scott Morrison (May 03 2019 at 18:20):

A related thing that would be really useful would be a method for diagnosing the need for erw instead of rw.

#### Scott Morrison (May 03 2019 at 18:21):

Very often, erw can be replaced with a change ..., rw (i.e. change by hand the defeq thing that erw is finding, that rw can't). It would be lovely to be told what the required change ... actually is.

#### Scott Morrison (May 03 2019 at 18:21):

Because often this is actually a missing refl-lemma..

#### Simon Hudon (May 03 2019 at 18:27):

Two interesting projects. I can look into them.

#### Simon Hudon (May 03 2019 at 18:28):

For the erw one, maybe I can do it by applying erw, then rw <- with the same lemma. I'll see.

#### Simon Hudon (May 03 2019 at 18:28):

What do you want it to be called?

#### Johan Commelin (May 03 2019 at 18:28):

I like the convention of tagging a ? onto the name

#### Johan Commelin (May 03 2019 at 18:29):

But for things in core that is hard...

#### Simon Hudon (May 03 2019 at 18:29):

We'd need to change core for that. I'm trying to make 3.5.0c backward compatible so for now, I'm not moving tactics from mathlib to core or even adding tactics that are needed in mathlib.

I understand

#### Johan Commelin (May 03 2019 at 18:31):

Even though foo? should of course never appear in mathlib. These tactics are for debugging/optimizing proofs only.

#### Johan Commelin (May 03 2019 at 18:31):

Anyway... in that case I would suggest squeeze_erw etc

#### Simon Hudon (May 03 2019 at 18:43):

:+1:

Last updated: May 15 2021 at 00:39 UTC