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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = ↑(eval₂Hom (RingHom.id S₁) g) (↑(eval₂Hom (RingHom.comp C f) X) p)
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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = ↑(eval g) (↑(map f) p)
unfold map eval
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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = ↑(eval₂Hom (RingHom.id S₁) g) (↑(eval₂Hom (RingHom.comp C f) X) p)
simp only [coe_eval₂Hom]
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  ↑(eval₂Hom (RingHom.id S₁) g) (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (↑(eval₂Hom (RingHom.id S₁) g) ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
have h := eval₂_comp_left (eval₂Hom (RingHom.id S₁) g) (C.comp f) X p
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  ↑(eval₂Hom (RingHom.id S₁) g) (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (↑(eval₂Hom (RingHom.id S₁) g) ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
dsimp [-eval₂_id] at 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p)
rw [h]
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ f = RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ g = eval₂ (RingHom.id S₁) g ∘ X
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ eval₂ f g p = eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
a : R
⊢ ↑f a = ↑(RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ f = RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
a : R
⊢ ↑f a = ↑(RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) a
simp only [coe_eval₂Hom, RingHom.id_apply, comp_apply, eval₂_C, 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
n : σ
⊢ g n = (eval₂ (RingHom.id S₁) g ∘ 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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
⊢ g = eval₂ (RingHom.id S₁) g ∘ X
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₁
g : σ → S₁
p : MvPolynomial σ R
h :
  eval₂ (RingHom.id S₁) g (eval₂ (RingHom.comp C f) X p) =
    eval₂ (RingHom.comp (eval₂Hom (RingHom.id S₁) g) (RingHom.comp C f)) (eval₂ (RingHom.id S₁) g ∘ X) p
n : σ
⊢ g n = (eval₂ (RingHom.id S₁) g ∘ X) n
simp only [comp_apply, eval₂_X]