∀ {K : Type u_2} {L : Type u_1} [inst : Zero K] [inst_1 : Add K] [inst_2 : Neg K] [inst_3 : Sub K] [inst_4 : One K]
  [inst_5 : Mul K] [inst_6 : Inv K] [inst_7 : Div K] [inst_8 : SMul ℕ K] [inst_9 : SMul ℤ K] [inst_10 : Pow K ℕ]
  [inst_11 : Pow K ℤ] [inst_12 : NatCast K] [inst_13 : IntCast K] [inst_14 : RatCast K] (f : K → L)
  (hf : Function.Injective f) [inst_15 : DivisionRing L] (zero : f 0 = 0) (one : f 1 = 1)
  (add : ∀ (x y : K), f (x + y) = f x + f y) (mul : ∀ (x y : K), f (x * y) = f x * f y) (neg : ∀ (x : K), f (-x) = -f x)
  (sub : ∀ (x y : K), f (x - y) = f x - f y) (inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : K), f (x / y) = f x / f y) (nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x)
  (zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x) (npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n),
  (∀ (q : ℚ), f ↑q = ↑q) → ∀ (q : ℚ), f ↑q = f (↑q.num / ↑q.den)