∀ (G : Type u_2) [inst : Group G] [h : IsCyclic G] (a : (ZMod (Nat.card G))ˣ) (a_1 : G),
  (MulEquiv.symm ((IsCyclic.mulAutMulEquiv G).symm a)) a_1 =
    (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a⁻¹ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a_1)))