Amenable Groups in Lean