case h_C
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (↑C a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (↑C a)

case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)

case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
apply induction_on p
no goals
case h_C
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (↑C a)) =
      eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (↑C a)
simp
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p q : MvPolynomial σ R
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
hq :
  Polynomial.eval x (eval₂ f g q) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)
intro p q hp hq
no goals
case h_add
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p q : MvPolynomial σ R
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
hq :
  Polynomial.eval x (eval₂ f g q) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p + q)
simp [hp, hq]
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
n : σ
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
⊢ Polynomial.eval x (eval₂ f g (p * X n)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
intro p n hp
no goals
case h_X
R : Type u_1
S : Type u_2
σ : Type u_3
x : S
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
n : σ
hp :
  Polynomial.eval x (eval₂ f g p) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) p
⊢ Polynomial.eval x (eval₂ f g (p * X n)) =
    eval₂ (RingHom.comp (Polynomial.evalRingHom x) f) (fun s => Polynomial.eval x (g s)) (p * X n)
simp [hp]