Rewriting with an homogeneous heterogeneous equality

Stream: new members

[Valentin Robert]

Hello,

I have a goal that is essentially:

H : foo p
E : p ≅ p'
---
foo p'

I believe p and p' live at the same type, in fact I am able to introduce eq_of_heq E : p = p', but I'm not sure how to use it to rewrite either my goal or my H hypothesis so that they agree.

[Adam Topaz]

Can you provide a #mwe ?

[Eric Wieser]

Is this lean 4?

[Kevin Buzzard]

In general I'm guessing this goal is not true, eg if foo X is X = p

[Mario Carneiro]

If you can prove p = p' then it should be true, and rwa [<- eq_of_heq E] should be the proof, unless there is something funny going on with hidden dependent arguments

[Mario Carneiro]

Oh, I was curious about the odd notation and it turns out that HEq has gone from having no notation to having two: a ~= b (which renders like a ≃ b in my programmer font) and a ≅ b both mean HEq a b now in lean 4

[Mario Carneiro]

or maybe I just missed it. git blame says it's been like that for 10 months