Lean/Mathlib: element of order pq from commuting elements; normalizer takes a Set

To show a subgroup L of order 2p is cyclic: use Cauchy (exists_prime_orderOf_dvd_card' (G := L)) twice and move the orders to G with rw [← Subgroup.orderOf_coe] at hx hy. Then Commute.orderOf_mul_eq_mul_orderOf_of_coprime gives orderOf (x*y) = 2p. Conclude with isCyclic_of_orderOf_eq_card (x * y), rewriting its goal with ← Subgroup.orderOf_coe, Subgroup.coe_mul. Separately, Subgroup.normalizer takes a Set G, so H.normalizer fails with an 'invalid field notation' error. Write Subgroup.normalizer (H : Set G), and use Subgroup.le_normalizer and Subgroup.mem_normalizer_iff (∀ h, h ∈ s ↔ g*h*g⁻¹ ∈ s).