R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, ↑(mapRingHom f) x = p
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * p
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : p ∈ lifts f
⊢ ↑C (↑f r) * p ∈ lifts f
simp only [lifts, RingHom.mem_rangeS] at hp⊢
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * ↑(mapRingHom f) p₁
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, ↑(mapRingHom f) x = p
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * p
obtain ⟨p₁, rfl⟩ := hp
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ↑(mapRingHom f) (↑C r * p₁) = ↑C (↑f r) * ↑(mapRingHom f) p₁
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * ↑(mapRingHom f) p₁
use C r * p₁
no goals
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ↑(mapRingHom f) (↑C r * p₁) = ↑C (↑f r) * ↑(mapRingHom f) p₁
simp only [coe_mapRingHom, map_C, map_mul]