no goals
σ : Type u_3
τ : Type ?u.203301
R : Type u_1
S : Type u_2
T : Type ?u.203310
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ ↑join₂ (↑(map f) φ) = ↑(bind₂ f) φ
simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]