case e_f
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ RingHom.comp (map g) (RingHom.comp C f) = RingHom.comp C (RingHom.comp g f)

case e_g
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ ↑(map g) ∘ X = fun n => X n
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) (RingHom.comp C f)) (↑(map g) ∘ X) p = ↑(map (RingHom.comp g f)) p
congr
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
a : R
⊢ ↑(RingHom.comp (map g) (RingHom.comp C f)) a = ↑(RingHom.comp C (RingHom.comp g f)) a
case e_f
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ RingHom.comp (map g) (RingHom.comp C f) = RingHom.comp C (RingHom.comp g f)
ext1 a
no goals
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
a : R
⊢ ↑(RingHom.comp (map g) (RingHom.comp C f)) a = ↑(RingHom.comp C (RingHom.comp g f)) a
simp only [map_C, comp_apply, RingHom.coe_comp]
case e_g.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
n : σ
⊢ (↑(map g) ∘ X) n = X n
case e_g
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ ↑(map g) ∘ X = fun n => X n
ext1 n
no goals
case e_g.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
n : σ
⊢ (↑(map g) ∘ X) n = X n
simp only [map_X, comp_apply]