∀ {R : Type u_2} {S : Type u_1} (f : R → S) (hf : Function.Surjective f) [inst : Add S] [inst_1 : Zero S]
  [inst_2 : One S] [inst_3 : Neg S] [inst_4 : Sub S] [inst_5 : SMul ℕ S] [inst_6 : SMul ℤ S] [inst_7 : NatCast S]
  [inst_8 : IntCast S] [inst_9 : AddCommGroupWithOne R] (zero : f 0 = 0) (one : f 1 = 1)
  (add : ∀ (x y : R), f (x + y) = f x + f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y)
  (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x)
  (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) (n : ℕ), ↑(n + 1) = ↑n + 1