excessive memory consumption in lemma statement

Stream: new members

[Joachim Breitner]

Hmm, I’m getting

(deterministic) timeout

in one of my proofs, which is rather innocent looking. I bisected the proof lines (by inserting sorrys) to an application of

    refine bsupr_le _,

if I move the sorry above that line, it works.
I tried making that line fully explicit:

    refine @bsupr_le (submonoid M) ι _ (noncomm_pi_coprod ϕ hcomm).mrange (λ i, i ∈ finset.univ) (λ i _, (ϕ i).mrange) _ ,

but that did not help.

I know this is not a #mwe, but maybe any hints so far?

Before some refactoring, the proof worked.

[Eric Rodriguez]

I think if making the line fully explicit didn't help, then I think a mwe or even the full code would be helpful

[Eric Rodriguez]

I'd be tempted to just work round it with a suffices : _, { exact bsupr_le this } instead of bothering figuring out why, though

[Eric Rodriguez]

also, is that first _ an instance search?

[Joachim Breitner]

Hmm, that work-around does not help, it seems

[Joachim Breitner]

That first _ is the complete_lattice instance for submonoid, but passing that explicitly doesn’t help either.

[Kevin Buzzard]

My hint is to stop saying "I know this is not a #mwe" and to let others see the code (e.g. are we on a mathlib branch?) Timeouts are hard to debug and can be caused by several things, but there are experts here.

[Joachim Breitner]

Absolutely right, I was about to do that, just making it a bit more presentable :-)

[Joachim Breitner]

This is the line that causes issues:
https://github.com/leanprover-community/mathlib/pull/11744/files#diff-dbff33c4f941f049b533b60208287dccc7a966ba9123603f9e09b8ea5ab6dbdeR140
(branch joachim/pi_nom, file src/group_theory/noncomm_pi_coprod.lean, lemma noncomm_pi_coprod_mrange).
Help appreciated!

[Joachim Breitner]

Oh, I think I have it

[Joachim Breitner]

Because of the refactoring I no longer have a bsupr, but just a bsupr. So if I use supr_le instead of bsupr_le, it works…

[Joachim Breitner]

:face_palm:

[Kevin Buzzard]

So this is probably one of those situations where what was happening was that Lean was trying to prove that bsupr ... = supr ... and kept unfolding and unfolding and for some reason never gave up and said "wait a minute, this actually doesn't match". I've certainly seen this sort of thing happen before.

[Yaël Dillies]

Also in general bsupr_le, bUnion_subset and a few lemmas around them are particularly brittle because of the precise order of elaboration. What's even more infuriating is that their duals, binfi_le, bInter_subset... don't elaborate the same way because the LHS and RHS are swapped.