case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
by_cases hq : q = 0
no goals
case pos
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
no goals
case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
  ofFractionRing_smul]