case h_C
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₁
⊢ ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g (↑C a * ↑(monomial s) a_1) = eval₂ f g (↑C a) * ↑f a_1 * Finsupp.prod s fun n e => g n ^ e

case h_add
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 q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g (q * ↑(monomial s) a) = eval₂ f g q * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * ↑(monomial s) a) = eval₂ f g (p + q) * ↑f a * Finsupp.prod s fun n e => g n ^ e

case h_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) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * ↑(monomial s) a) = eval₂ f g (p * X n) * ↑f a * Finsupp.prod s fun n e => g n ^ e
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₁
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
apply MvPolynomial.induction_on p
case h_C
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₁
a' : R
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (↑C a' * ↑(monomial s) a) = eval₂ f g (↑C a') * ↑f a * Finsupp.prod s fun n e => g n ^ e
case h_C
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₁
⊢ ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g (↑C a * ↑(monomial s) a_1) = eval₂ f g (↑C a) * ↑f a_1 * Finsupp.prod s fun n e => g n ^ e
intro a' s a
no goals
case h_C
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₁
a' : R
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (↑C a' * ↑(monomial s) a) = eval₂ f g (↑C a') * ↑f a * Finsupp.prod s fun n e => g n ^ e
simp [C_mul_monomial, eval₂_monomial, f.map_mul]
case h_add
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 q : MvPolynomial σ R
ih_p : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
ih_q : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * ↑(monomial s) a) = eval₂ f g q * ↑f a * Finsupp.prod s fun n e => g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g ((p + q) * ↑(monomial s) a) = eval₂ f g (p + q) * ↑f a * Finsupp.prod s fun n e => g n ^ e
case h_add
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 q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g (q * ↑(monomial s) a) = eval₂ f g q * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * ↑(monomial s) a) = eval₂ f g (p + q) * ↑f a * Finsupp.prod s fun n e => g n ^ e
intro p q ih_p ih_q
no goals
case h_add
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 q : MvPolynomial σ R
ih_p : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
ih_q : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * ↑(monomial s) a) = eval₂ f g q * ↑f a * Finsupp.prod s fun n e => g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g ((p + q) * ↑(monomial s) a) = eval₂ f g (p + q) * ↑f a * Finsupp.prod s fun n e => g n ^ e
simp [add_mul, eval₂_add, ih_p, ih_q]
case h_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
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * ↑(monomial s) a) = eval₂ f g (p * X n) * ↑f a * Finsupp.prod s fun n e => g n ^ e
case h_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) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * ↑(monomial s) a) = eval₂ f g (p * X n) * ↑f a * Finsupp.prod s fun n e => g n ^ e
intro p n ih s a
no goals
case h_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
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * ↑(monomial s) a) = eval₂ f g (p * X n) * ↑f a * Finsupp.prod s fun n e => g n ^ e
exact
  calc
    (p * X n * monomial s a).eval₂ f g = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g :=
      by rw [monomial_single_add, pow_one, mul_assoc]
    _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
      simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
        f.map_one]
no goals
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
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * ↑(monomial s) a) = eval₂ f g (p * ↑(monomial (Finsupp.single n 1 + s)) a)
rw [monomial_single_add, pow_one, mul_assoc]
no goals
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
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * ↑(monomial s) a) = eval₂ f g p * ↑f a * Finsupp.prod s fun n e => g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * ↑(monomial (Finsupp.single n 1 + s)) a) =
    eval₂ f g (p * ↑(monomial (Finsupp.single n 1)) 1) * ↑f a * Finsupp.prod s fun n e => g n ^ e
simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
  f.map_one]