case h
σ : Type u_1
R : Type u_3
S : Type u_2
T : Type ?u.869997
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ ↑(coeff S m) (↑(map σ f) (↑(monomial R n) a)) = ↑(coeff S m) (↑(monomial S n) (↑f a))
σ : Type u_1
R : Type u_3
S : Type u_2
T : Type ?u.869997
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
a : R
⊢ ↑(map σ f) (↑(monomial R n) a) = ↑(monomial S n) (↑f a)
ext m
no goals
case h
σ : Type u_1
R : Type u_3
S : Type u_2
T : Type ?u.869997
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ ↑(coeff S m) (↑(map σ f) (↑(monomial R n) a)) = ↑(coeff S m) (↑(monomial S n) (↑f a))
simp [coeff_monomial, apply_ite f]