-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
C₁ :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add₁ :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X₁ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
C₂ :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add₂ :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X₂ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
C₃ :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add₃ :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X₃ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
C₄ :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add₄ :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X₄ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
add₅ :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
mul_X₅ mul_X₆ :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)

Tactic:
classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]

Premises used: MvPolynomial.coeff_C, apply_ite, MvPolynomial.induction_on, MvPolynomial.coeff_mul_X', MvPolynomial.map_C, RingHom.map_zero, MvPolynomial.coeff_add, MvPolynomial.map, RingHom.map_mul, RingHom.map_add, DFunLike.coe, MvPolynomial.map_X