simple group of order 60 isomorphic A5

Stream: Is there code for X?

[Yuzi]

is there any lemma about this, thank you

[Edison Xie]

docs#alternatingGroup.isSimpleGroup_five

[Edison Xie]

using docs#Fintype.bijective_iff_injective_and_card should be easy to prove

[Damiano Testa]

Reading the title, I get the impression that they are interested in the opposite implication: if a group is simple and has order 60, then it is isomorphic to A_5.