case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) = ↑φ p / ↑φ 0

case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) = ↑φ p / ↑φ q
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) = ↑φ p / ↑φ q
rcases eq_or_ne q 0 with (rfl | hq)
no goals
case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) = ↑φ p / ↑φ q
simp only [← mk_eq_div, mk_eq_localization_mk _ hq,
  liftMonoidWithZeroHom_apply_ofFractionRing_mk]
no goals
case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) 0) = ↑φ p / ↑φ 0
simp only [div_zero, map_zero]