R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree (map f p) = 0 then 0 else coeff (map f p) (natDegree (map f p) - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ nextCoeff (map f p) = ↑f (nextCoeff p)
unfold nextCoeff
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree p = 0 then 0 else coeff (map f p) (natDegree p - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree (map f p) = 0 then 0 else coeff (map f p) (natDegree (map f p) - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
rw [natDegree_map_eq_of_injective hf]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree p = 0 then 0 else coeff (map f p) (natDegree p - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
split_ifs <;> simp [*]