case h
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2847427
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
r : R
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (↑(C R) r)) = ↑(coeff S n✝) (↑(C ((fun x => S) r)) (↑f r))
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2847427
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
r : R
⊢ ↑(map f) (↑(C R) r) = ↑(C ((fun x => S) r)) (↑f r)
ext
no goals
case h
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2847427
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
r : R
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (↑(C R) r)) = ↑(coeff S n✝) (↑(C ((fun x => S) r)) (↑f r))
simp [coeff_C, apply_ite f]