leanprover-community/NNG4

at h

Closed this issue · 1 comments

jariji commented

https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/2

Rewrite zero_add at h twice, to change h into the goal.

Not sure we've heard about at yet.

joneugster commented

Thanks! Already fixed a week ago, will be online in the next update. The first hint now says:

You can use rw [zero_add] at h to rewrite at h instead
of at the goal.