case hf
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.129297
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ ∀ (i : σ), ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.129297
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ AlgHom.comp (expand p) (bind₁ f) = bind₁ fun i => ↑(expand p) (f i)
apply algHom_ext
case hf
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.129297
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
case hf
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.129297
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ ∀ (i : σ), ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
intro i
no goals
case hf
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.129297
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
simp only [AlgHom.comp_apply, bind₁_X_right]