!4#3898 simp failure

Stream: mathlib4

[Kevin Buzzard]

This is !4#3898 and CategoryTheory.Sites.CoverLifting, on the way to Copenhagen. I've got the file compiling apart from one failing simp proof, where I can't get a rewrite to work because of motive is not type correct issues. I've documented what I know here but I don't know how to make any more progress. Any help appreciated! If we can get this file working then category_theory.sites.dense_subsite, an explicit target for Copenhagen (and the first thing on the port progress list) is unblocked.

[Mauricio Collares]

Will push a dumb workaround, one sec

[Kevin Buzzard]

I'm intrigued :-) Thanks a lot for dealing with all my problems over the last day or so!

[Mauricio Collares]

I think what confused me the most about this issue is that rw [pulledbackFamily_apply, pulledbackFamily_apply] creates two new side goals identical to the last goal created by the earlier convert, which didn't happen in Lean 3. So a lot of valid ways to finish the proof were rejected (with "goals accomplished" and a red squiggle) because of the leftover side goals.

[Kevin Buzzard]

Yeah, if you switch the last two goals with swap then this doesn't happen. It's something to do with the metavariable? I was also confused by this!

[Kevin Buzzard]

Oh the remaining goal somehow disappears and becomes a subgoal after the rewrite? Yeah that is really bewildering. Thanks so much though!

[Mauricio Collares]

It doesn't disappear per se, but when you solve the rw subgoal the outer goal is also solved automatically.

[Mauricio Collares]

Probably swapping the goals (as you suggested) is more intuitive

[Kevin Buzzard]

OK this is now ready for review.