rw at * changes recursion hypothesis

Stream: lean4

[Joachim Breitner]

Consider this minimal example:

lemma a_lemma : 1 = 2 := sorry

example : 1 = 3 -> 1 = 3 := by
  intro h
  rewrite [a_lemma] at *

Before the rewrite, the tactic state is

h: 1 = 3
⊢ 1 =

afterwards it is

_example: 2 = 3 → 2 = 3
h: 2 = 3
⊢ 2 = 3

So it seems that there is a (hidden) hypothesis example, presumably there in case I choose to make the proof recursive, that rewrite stumbles over, changes, and thus makes visible.

Is there an easy way I can tell rewrite [] at … to not rewrite this “hidden” hypothesis?

[Joachim Breitner]

It seems there is a nonrec modifier that I just stumbled over by accident :-). That might be a work-around for me for now, but if I want to bundle my tactic expression into something reusable, it would be better to not require the user to do that.

[Kevin Buzzard]

I discovered this independently last week and it was one of the reasons that I switched to giving a demo in front of hundreds of mathematicians from lean 4 to lean 3; I wanted to rw continuous_def at * to change hypotheses of continunity to the open set definition but I decided that the arrival of this random new hypothesis was confusing.

[Jannis Limperg]

lean4#2219