(Another) proof of alternating group A_n is simple

Stream: mathlib4

[Wang Jingting]

I just finished this proof about the alternating group $A_n$ is simple, which I'm quite happy about since it's only ~200 lines on top of current mathlib. (~100 lines if you can tolerate decide running for 5 minutes :)
But anyway, I remember someone has told me that @Antoine Chambert-Loir has a proof of this a long time ago, and by checking recent PRs, I found @Miyahara Kō is also PRing a proof of this.

(sadly zulip complained about the code being so long, so I cannot directly paste it here)
An_simple.lean

Are there any suggestions on what parts (if any) of this proof is worth of opening a PR?
Some of the things I find useful are:

1. the list of possible cycleType for a permutation in $S_n$ (so that people can enumerate over it and reduce to some representatives of conjugacy classes).
2. some API lemmas for Equiv.Perm.viaEmbeddingHom.
3. a lemma about existence of embedding between Fintype such that the image contains a certain subset.

Another interesting observation: It seems to me that #16482 and #25299 are making the same changes?

[Wang Jingting]

Edit: In #20538 the change from #16482 is reverted without noticing, then people realized decide is stuck there again, and made PR #25299, perhaps we could have an implementation note there?

[Antoine Chambert-Loir]

About 1, what is the relation with docs#Equiv.Perm.CycleType.count_def ?

[Wang Jingting]

Antoine Chambert-Loir said:

About 1, what is the relation with docs#Equiv.Perm.CycleType.count_def ?

I think they're pretty much unrelated (?) The lemma I proved here is about giving us a concrete list of possible cycleType that we can enumerate through (e.g. rcases). For example, the list of possible cycleType for permutations in $S_5$ is [{5}, {4}, {3, 2}, {3}, {2, 2}, {2}, {}], so we can claim every element is conjugate to a representative of each conjugate class.
and the lemma you referred to seems to be about how many times n appeared in the cycleType of a certain permutations?

[Miyahara Kō]

Having looked at your proof, it seems that its length is not very different from mine.
I have been busy with work over the past two months and have left the pull requests unattended, but I may be able to get back to them soon — or I may not.
Therefore, I think it would be better to split things into appropriately small pull requests and adopt whichever proof gets merged into the master branch more quickly.
Also, regardless of which proof is ultimately adopted, the lemmas concerning viaEmbeddingHom and Fintype will be useful, so I think it would be best to start with pull requests for those first.

[Antoine Chambert-Loir]

Antoine Chambert-Loir said:

About 1, what is the relation with docs#Equiv.Perm.CycleType.count_def ?

Sorry, I meant docs#Equiv.Perm.card_of_cycleType_mul_eq