Don't close the goal automatically

Stream: general

[Johannes C. Mayer]

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 :=
begin
  rw h₁,
end

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 :=
begin
  change x = 5 with 5 = 5,
  refl,
end

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]

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]

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

[Kevin Buzzard]

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