Help requested for !4#2458 (GroupTheory.Perm.Sign)

Stream: mathlib4

[Arien Malec]

I'm down to a single issue for !4#2458 that I've stared at until I'm crosseyed.

Quotient.inductionOn₂ seems to be wanting to swap the order of parameters in ways that just don't seem to make sense...

Needs a new pair of eyes for someone who wants a puzzle...

[Adam Topaz]

is signAux3_symm_trans_trans the issue?

[Adam Topaz]

I see other errors as well...

[Adam Topaz]

oh wait I didn't pull :)

[Adam Topaz]

Sorry it turns out I can't play with this right now.

[Eric Wieser]

I'll have a look at it when I'm next at lean

[Matthew Ballard]

It was getting the motive a little mixed up. I pushed a fix but it needs to be cleaned up

[Eric Wieser]

I reverted that fixed and pushed what seems like a simpler one

[Arien Malec]

Nice - I learned a few tricks from this.

[Eric Wieser]

The old spelling was pretty weird, and I'm somewhat surprised the elaborator was clever enough for it to work