case hf
σ : Type u_3
τ : Type u_4
R : Type u_2
S : Type ?u.645310
T : Type ?u.645313
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ↑(AlgHom.comp (bind₁ f) (rename g)) (X i) = ↑(bind₁ (f ∘ g)) (X i)
σ : Type u_3
τ : Type u_4
R : Type u_2
S : Type ?u.645310
T : Type ?u.645313
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : τ → MvPolynomial υ R
g : σ → τ
⊢ AlgHom.comp (bind₁ f) (rename g) = bind₁ (f ∘ g)
ext1 i
no goals
case hf
σ : Type u_3
τ : Type u_4
R : Type u_2
S : Type ?u.645310
T : Type ?u.645313
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ↑(AlgHom.comp (bind₁ f) (rename g)) (X i) = ↑(bind₁ (f ∘ g)) (X i)
simp