∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (n : ℕ) (a : (Monoid.PushoutI.con φ).Quotient),
  DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a