ext bug

Stream: lean4

[Jon Eugster]

Adam Topaz said:

ext needs some love. I realized today that ext A B doesn't work (sometimes? maybe all the time?) and often an additional intro B is needed.

Could you send a reference/mwe where ext didn't work for you, please? I did encounter the same bug a while ago and figured out how to fix it, but my MWE back then was not considered valid, as it was rather a badly shaped ext-lemma. Therefore I never PRed that fix.