no goals
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
conv_lhs =>
  rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← RingHom.map_mul, ←
    RingHom.map_mul]