case h
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2938579
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) X) = ↑(coeff S n✝) X
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2938579
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
⊢ ↑(map f) X = X
ext
no goals
case h
R : Type u_2
inst✝² : Semiring R
S : Type u_1
T : Type ?u.2938579
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) X) = ↑(coeff S n✝) X
simp [coeff_X, apply_ite f]