Tactic `split` not working

Stream: lean4

[Ilmārs Cīrulis]

Here - last split not working.

Is it real bug? Or do I misunderstand something?

[Ilmārs Cīrulis]

Will try to make it smaller or #mwe

[Damiano Testa]

Lessness said:

Will try to make it smaller or #mwe

You could try using extract_goal at the position where the problem is and see if that minimises it for you.

[Ilmārs Cīrulis]

extract_goal doesn't help, sadly, because everything works with the extracted theorem. :\

[Sébastien Gouëzel]

If you do rw [Eq.comm] before your split (to put the term you want to split on on the left hand side of the equality), then it works.

[Ilmārs Cīrulis]

Thank you, that solves my problem and I can continue proving.

[Ilmārs Cīrulis]

Lessness said:

Will try to make it smaller or #mwe

Removed anything unnecessary and put few more sorry in some places. Now it's about 50 lines, most of them definitions.