∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : Group M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.group f hf one mul inv div npow zpow =
    { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_mul_cancel := ⋯ }