Lean doesn't find instance of something that's right there

Stream: new members

[Abhimanyu Pallavi Sudhir]

Weird problem -- I have my goal, which is (x ⋆ y) → (y ⋆ z) → (x ⋆ z) (for some operation ⋆) and I have a hypothesis Hxy : x = y. But when I try rw Hxy, Lean tells me:

rewrite tactic failed, did not find instance of the pattern in the target expression
  x

[Abhimanyu Pallavi Sudhir]

But... it's right there.

[Kevin Buzzard]

Post a MWE

[Kevin Buzzard]

Sometimes it's because you have two variables called x, sometimes it's because something needs to be done by type class inference and type class inference fails but the error mesage is that the rewrite failed, there are all sorts of reasons.

[Kevin Buzzard]

Another reason it fails is that you can't rewrite under a binder. Does simp only [Hxy] work? As you can see, it's difficult to diagnose without a MWE.

[Abhimanyu Pallavi Sudhir]

Ok, I got the problem (it was the "two variables called x" thing) -- I had defined a symbol S for fin 2 and mid-way through the proof had done rw S at z y x, which caused two sets of variables x y z to be defined.

[Kevin Buzzard]

rw is a fickle beast.

[Abhimanyu Pallavi Sudhir]

(although I'm not sure why that happened -- usually when you do rw something at something, it just changes the statement, not create new ones.)

[Kevin Buzzard]

It takes a while to get to know its foibles

[Kevin Buzzard]

example (n x y : ℕ) (h : n > 0 → x = y) : x + 1 = y + 2 :=
begin
  rw h,
  -- one goal became 2 -- we now need a proof of n > 0
  sorry,sorry
end

[Abhimanyu Pallavi Sudhir]

Yeah, I've encountered that before, but that actually makes sense (and is useful!). Treating rewrites differently based on whether they're done on a natural number or a proof is just weird.