no goals
σ : Type u_3
τ : Type ?u.691562
R : Type u_4
S : Type u_1
T : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* MvPolynomial σ T
g : R →+* S
φ : MvPolynomial σ R
⊢ ↑(bind₂ f) (↑(map g) φ) = ↑(bind₂ (RingHom.comp f g)) φ
simp [bind₂]