-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
C :
  ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          ((monomial s : (a : R) → MvPolynomial σ R) a_1 : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) ((f : (a : R) → S₁) a_1 : S₁) *
        s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) q ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g q) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) (p + q)
                ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g (p + q)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) (p * X n)
              ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g (p * X n)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
add₁ :
  ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) q ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g q) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g
              (HMul.hMul (β := MvPolynomial σ R) (p + q)
                ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
            HMul.hMul (β := S₁) (eval₂ f g (p + q)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
mul_X₁ mul_X₂ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g
            (HMul.hMul (β := MvPolynomial σ R) (p * X n)
              ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
          HMul.hMul (β := S₁) (eval₂ f g (p * X n)) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e

Tactic:
classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    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]

Premises used: add_mul, MvPolynomial.C_mul_monomial, MvPolynomial.induction_on, MvPolynomial.eval₂_add, MvPolynomial.eval₂_monomial, RingHom.map_mul