Zulip Chat Archive

Stream: general

Topic: Don't close the goal automatically

Johannes C. Mayer (Nov 22 2021 at 13:35):

Is there some way to prevent the rw, simp, unfload, conv mode, and other tactics like this from closing the goal automatically? E.g. here it is closed by rw:

example (x : ) (h₁ : x = 5) : x = 5 :=
  rw h₁,

I know that I can use change, or dsimp like below if x is a constant. But that does not work in the above example.

def x :  := 5

example : x = 5 :=
  change x = 5 with 5 = 5,

Sometimes I just want to look at the effectively solved statement that is trivially true, to better understand why it actually is now true (in these examples it is of course completely obvious but if the statement is more complex it might not be that easy).

Kevin Buzzard (Nov 22 2021 at 14:44):

You could write your own rw' tactic which does rw but doesn't try refl at the end! This is what I did in the natural number game. But basically yours is a very minority use case -- most people just want to close goals quickly.

Johannes C. Mayer (Nov 22 2021 at 15:50):

Ah, ok thanks. I might look into that. I was wondering why it works differently in the natural number game.

Kevin Buzzard (Nov 22 2021 at 16:48):

NNG is Lean for beginners. mathlib is Lean in expert mode :-)

Last updated: Aug 03 2023 at 10:10 UTC