K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x * q) = ↑(algebraMap K[X] (RatFunc K)) (p * denom x) ↔
    x * ↑(algebraMap K[X] (RatFunc K)) q = ↑(algebraMap K[X] (RatFunc K)) p
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ num x * q = p * denom x ↔ x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x * q) = ↑(algebraMap K[X] (RatFunc K)) (p * denom x) ↔
    ↑(algebraMap K[X] (RatFunc K)) (num x) / ↑(algebraMap K[X] (RatFunc K)) (denom x) *
        ↑(algebraMap K[X] (RatFunc K)) q =
      ↑(algebraMap K[X] (RatFunc K)) p
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x * q) = ↑(algebraMap K[X] (RatFunc K)) (p * denom x) ↔
    x * ↑(algebraMap K[X] (RatFunc K)) q = ↑(algebraMap K[X] (RatFunc K)) p
conv_rhs => rw [← num_div_denom x]
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom x) ≠ 0
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x * q) = ↑(algebraMap K[X] (RatFunc K)) (p * denom x) ↔
    ↑(algebraMap K[X] (RatFunc K)) (num x) / ↑(algebraMap K[X] (RatFunc K)) (denom x) *
        ↑(algebraMap K[X] (RatFunc K)) q =
      ↑(algebraMap K[X] (RatFunc K)) p
rw [RingHom.map_mul, RingHom.map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ←
  mul_assoc, ← div_eq_mul_inv, div_eq_iff]
no goals
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom x) ≠ 0
exact algebraMap_ne_zero (denom_ne_zero x)