under what condition SL(2, F) is simple

Stream: Is there code for X?

[Yuzi]

im tryin to prove SL(2, F_4) is simple is there lemma in Mathlib4 that i can use

[Kevin Buzzard]

There are many lemmas in mathlib and you can use them all! Which ones do you want to use? Lean does not do magic: which proof are you planning on formalising? You need to know the maths proof first.

[pro-Lie stabilizer]

@Antoine Chambert-Loir proved that A₅ is simple in the paper here.

[Antoine Chambert-Loir]

@Yuzi 1. This group has 60 elements and is isomorphic to the alternating group $\mathfrak A_5$ on 5 letters, and docs#alternatingGroup.isSimpleGroup_five proves that this latter group is simple. You could thus try to establish the isomorphy of those two groups.

2. As suggested by Kevin, there are several approaches. One of them, a classical one due to Iwasawa, is also outlined in the paper pointed out by @Akil Qasim.