no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.269321
T : Type ?u.269324
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ ↑(aeval id) (↑(rename f) p) = ↑(aeval f) p
rw [aeval_rename, Function.comp.left_id]