case h
σ : Type u_1
τ : Type ?u.59131
υ : Type ?u.59134
R : Type u_2
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
σ : Type u_1
τ : Type ?u.59131
υ : Type ?u.59134
R : Type u_2
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x
funext i
no goals
case h
σ : Type u_1
τ : Type ?u.59131
υ : Type ?u.59134
R : Type u_2
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
simp only [comap, AlgHom.id_apply, id.def, aeval_X]