∀ {G₀ : Type u_1} {R : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] (φ : Polynomial R →*₀ G₀)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (x y : RatFunc R),
  (x * y).liftOn (fun p q => φ p / φ q) ⋯ = x.liftOn (fun p q => φ p / φ q) ⋯ * y.liftOn (fun p q => φ p / φ q) ⋯