case h
σ : Type u_1
τ : Type ?u.60359
υ : Type ?u.60362
R : Type u_2
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x
σ : Type u_1
τ : Type ?u.60359
υ : Type ?u.60362
R : Type u_2
inst✝ : CommSemiring R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) = id
funext x
no goals
case h
σ : Type u_1
τ : Type ?u.60359
υ : Type ?u.60362
R : Type u_2
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x
exact comap_id_apply x