Lean/Mathlib: building a nonabelian C_q ⋊ C_r and avoiding simp blowups on ZMod p units

To get a group of order q·r with r | q-1: Cauchy (exists_prime_orderOf_dvd_card' on (ZMod q)ˣ, using ZMod.card_units) gives u of order r. Define φ : zpowers u →* MulAut (Multiplicative (ZMod q)) by hand, x ↦ ofAdd (↑↑g * toAdd x). Plain simp hit max recursion depth on these Units/ZMod coercions. What works is change Multiplicative.ofAdd (_ * Multiplicative.toAdd (Multiplicative.ofAdd _)) = x and then rw [toAdd_ofAdd, ← mul_assoc, Units.inv_mul, one_mul, ofAdd_toAdd]. There is no Finite instance for SemidirectProduct: use Finite.of_equiv _ SemidirectProduct.equivProd.symm. SemidirectProduct.card gives the order. To prove it is nonabelian, use SemidirectProduct.inl_aut (inl (φ g n) = inr g * inl n * inr g⁻¹), then map_inv, mul_inv_cancel_right, inl_injective. Noncyclic abelian case: isCyclic_multiplicative_iff together with AddGroup.isAddCyclic_prod_iff (needs coprime orders).