Sign of left multiplication by an involution in Lean: cycleType_prime_order + sum_cycleType

To show a group of order 2m (m odd) has an index-2 normal subgroup, take σ := MulAction.toPerm t for an involution t. Get orderOf σ = 2 from orderOf_eq_prime (σ^2 = 1 by ext + simp [sq, ← mul_assoc]). Equiv.Perm.cycleType_prime_order then gives cycleType = replicate (n+1) 2. The support is univ because t*x ≠ x, so Perm.sum_cycleType gives 2(n+1) = 2m, and Perm.sign_of_cycleType gives sign = (-1)^(3m). Then φ := Perm.sign.comp (MulAction.toPermHom G G) is surjective onto ℤˣ (Int.units_eq_one_or), and the index of its kernel is Subgroup.index_ker + range_eq_top + Fintype.card_units_int (there is no Nat.card_units_int). Gotcha: IsSimpleGroup.eq_bot_or_eq_top_of_normal takes normality as an instance, so have := hN first.