Zulip Chat Archive

In mathlib4#1786 I had to manually replace map₂ with Filter.map₂ on line 155 because Lean was treating map₂ as if it was Filter.NeBot.map₂ while inside of the Filter namespace. Is this expected behavior?

Adam Topaz (Jan 23 2023 at 17:27):

Specifically, the issue was (map₂ m f g).NeBot

Yury G. Kudryashov (Jan 23 2023 at 17:51):

It happens if you're proving NeBot.*. It seems that Lean opens NeBot in this case.

Yury G. Kudryashov (Jan 23 2023 at 17:51):

I added some protected as a workaround.

Yury G. Kudryashov (Jan 23 2023 at 17:52):

BTW, I have some golfs for proofs in this file, see #18258.

Yaël Dillies (Jan 23 2023 at 17:54):

This lemma should be protected anyway, indeed.

Yury G. Kudryashov (Jan 23 2023 at 17:55):

Another change of behavior: if you prove Function.Commute.blah, you can't use h.blah to call an existing Function.Semiconj.blah because it'll try Function.Commute.blah first and complain about a cyclic proof.

Yury G. Kudryashov (Jan 23 2023 at 17:55):

That's why I added Function.Commute.semiconj while porting order.filter.basic.

Yury G. Kudryashov (Jan 23 2023 at 17:58):

I guess, I'll have to drop #18258 and redo it in Lean 4 later.

Eric Wieser (Jan 23 2023 at 18:09):

Yury G. Kudryashov said:

you can't use h.blah to call an existing Function.Semiconj.blah because it'll try Function.Commute.blah first and complain about a cyclic proof.

Sure you can, use nonrec