σ : Type u_3
τ : Type ?u.579799
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) f) (↑(map g) ∘ X) φ = eval₂ (RingHom.comp (map g) f) X φ
σ : Type u_3
τ : Type ?u.579799
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ ↑(map g) (↑(bind₂ f) φ) = ↑(bind₂ (RingHom.comp (map g) f)) φ
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
case e_g.h
σ : Type u_3
τ : Type ?u.579799
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (↑(map g) ∘ X) x✝ = X x✝
σ : Type u_3
τ : Type ?u.579799
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) f) (↑(map g) ∘ X) φ = eval₂ (RingHom.comp (map g) f) X φ
congr 1 with : 1
no goals
case e_g.h
σ : Type u_3
τ : Type ?u.579799
R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (↑(map g) ∘ X) x✝ = X x✝
simp only [Function.comp_apply, map_X]