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