-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
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))
⊢ 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₁)
have 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))
Tactic: rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]