(p, q).snd

Stream: Is there code for X?

[Winston Yin]

Silly question: is there a rw lemma for (p, q).snd = q?

[Kevin Buzzard]

This is rfl and sometimes the lemma doesn't exist in this situation.

[Kevin Buzzard]

You can always use change instead of rewriting (or dsimp only)

[Winston Yin]

Hmm I'm writing a proof with a lot of (...., (......, ........).snd).snd, and a simple rw would be quite nice

[Yaël Dillies]

Why not just dsimp?

[Winston Yin]

Isn't non terminal dsimp frowned upon

[Winston Yin]

And what if I only want to dsimp a particular expression, not the whole goal?

[Yaël Dillies]

No! simp and dsimp are two very different things

[Yaël Dillies]

It's rare that you would want to do that, but if you do you can rw (by dsimp : something= something_else)

[Kevin Buzzard]

I would say that non-terminal dsimp is frowned upon, but I suggested dsimp only which is fine (as is simp only [foo, bar, baz])

[Yaël Dillies]

How so? There are many less opportunities for a dsimp call to break and whatever happens you're guaranteed than where it breaks the goal is definitionally equal to what you had before.

[Yaël Dillies]

Also note that squeeze_dsimp is botched so your dsimp only suggestion isn't viable.

[Winston Yin]

dsimp only thankfully simplified exact the expression I need to simplify