Can I have multiple hypotheses of the same name?

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

It's sometimes tedious to give all hypotheses a decent name (and I don't always like the default names that Lean comes up with.) So it's tempting to reuse names, as in have h := h.1. I expect Lean to use the latest definition whenever a variable occur more than once in the context, and my observation so far is consistent with my expectation. But is that what it really does?

[Kevin Buzzard]

Yes, it uses the one it finds first, which is the one you defined last.

[Kevin Buzzard]

Note though that if you're really done with the old h you can replace h := h.1. You don't really want your local context becoming too big.

[Patrick Lutz]

clear will also remove unwanted hypotheses

[Patrick Lutz]

tactic#clear