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.