no goals
σ : Type u_4
τ : Type u_2
R : Type u_1
S : Type u_3
T : Type ?u.758101
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑f (↑(bind₁ g) φ) = ↑(eval₂Hom (RingHom.comp f C) fun i => ↑f (g i)) φ
rw [bind₁, map_aeval, algebraMap_eq]