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