[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial σ R
⊢ ↑(expand 1) f = f
[PROOFSTEP]
simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_id,
  AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ expand 1 = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 f
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ
⊢ ↑(expand 1) (X f) = ↑(AlgHom.id R (MvPolynomial σ R)) (X f)
[PROOFSTEP]
rw [expand_one_apply, AlgHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ AlgHom.comp (expand p) (bind₁ f) = bind₁ fun i => ↑(expand p) (f i)
[PROOFSTEP]
apply algHom_ext
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
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)
[PROOFSTEP]
intro i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
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)
[PROOFSTEP]
simp only [AlgHom.comp_apply, bind₁_X_right]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(expand p) (↑(bind₁ f) φ) = ↑(bind₁ fun i => ↑(expand p) (f i)) φ
[PROOFSTEP]
rw [← AlgHom.comp_apply, expand_comp_bind₁]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(expand p) φ) = ↑(expand p) (↑(map f) φ)
[PROOFSTEP]
simp [expand, map_bind₁]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(rename f) (↑(expand p) φ) = ↑(expand p) (↑(rename f) φ)
[PROOFSTEP]
simp [expand, bind₁_rename, rename_bind₁, Function.comp]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
⊢ AlgHom.comp (rename f) (expand p) = AlgHom.comp (expand p) (rename f)
[PROOFSTEP]
ext1 φ
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : σ
⊢ ↑(AlgHom.comp (rename f) (expand p)) (X φ) = ↑(AlgHom.comp (expand p) (rename f)) (X φ)
[PROOFSTEP]
simp only [rename_expand, AlgHom.comp_apply]
