Irredundant bases for finite almost simple groups (Lean code)

This is the Lean code accompanying Peiran Wu's PhD thesis "Irredundant bases for finite almost simple groups".
The code formalises Lemma 3.15 as "mlii_eq_of_subsingleton_fixedPoints_stabilizer", which states the exact maximum irredundant base size of a wreath product H wr K in faithful product action, provided each point stabiliser in H has a single fixed point.