K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
hq' : ↑φ q ≠ 0
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
have hq' : φ q ≠ 0 := nonZeroDivisors.ne_zero (hφ (mem_nonZeroDivisors_iff_ne_zero.mpr hq))
no goals
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
hq' : ↑φ q ≠ 0
⊢ ↑(map φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑φ p) / ↑(algebraMap ((fun x => R[X]) q) (RatFunc R)) (↑φ q)
simp only [← mk_eq_div, mk_eq_localization_mk _ hq, map_apply_ofFractionRing_mk,
  mk_eq_localization_mk _ hq']