-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p_1 p : MvPolynomial S₂ R
s : S₂
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
mul_X :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p * eval₂ C g (X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
mul_X₁ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
mul_X₂ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
mul_X₃ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      (HMul.hMul (α := MvPolynomial S₂ S₁) (β := MvPolynomial S₂ S₁)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p : MvPolynomial S₂ S₁)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (X s) : MvPolynomial S₂ S₁))
mul_X₄ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      (HMul.hMul (α := MvPolynomial S₂ S₁) (β := MvPolynomial S₂ S₁)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p : MvPolynomial S₂ S₁) (X s))
mul_X₅ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    HMul.hMul (α := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g) (X s))
mul_X₆ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (g s) : MvPolynomial S₃ S₁) =
    HMul.hMul (α := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g) (X s))
mul_X₇ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (g s) : MvPolynomial S₃ S₁) =
    HMul.hMul (α := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      (((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g) s)
mul_X₈ mul_X₉ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (g s) : MvPolynomial S₃ S₁) =
    HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (g s) : MvPolynomial S₃ S₁)
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p * X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)

Tactic:
rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]

Premises used: MvPolynomial.eval₂_X, MvPolynomial.eval₂_mul, MvPolynomial.map, Function.comp_apply, RingHom.map_mul, MvPolynomial.map_X