-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
S₂ : Type u_2
inst_2 : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p_1 p : MvPolynomial σ R
s : σ
hp :
  (k : (a : S₁) → S₂) (eval₂ f g p) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
mul_X :
  (k : (a : S₁) → S₂) (eval₂ f g p * eval₂ f g (X s)) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X s))
mul_X₁ :
  HMul.hMul (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g (X s)) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X s))
mul_X₂ :
  HMul.hMul (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g (X s)) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g)
      (HMul.hMul (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X s) : MvPolynomial σ S₁))
mul_X₃ :
  HMul.hMul (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g (X s)) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) *
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X s))
mul_X₄ :
  HMul.hMul (α := S₂) (β := S₂) ((k : (a : S₁) → S₂) (eval₂ f g p) : S₂) ((k : (a : S₁) → S₂) (eval₂ f g (X s)) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) *
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) (X s)
mul_X₅ :
  HMul.hMul (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      ((k : (a : S₁) → S₂) (eval₂ f g (X s)) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) *
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) (X s)
mul_X₆ :
  HMul.hMul (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      ((k : (a : S₁) → S₂) (g s) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) *
      eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) (X s)
mul_X₇ :
  HMul.hMul (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      ((k : (a : S₁) → S₂) (g s) : S₂) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) *
      ((⇑k : (a : S₁) → S₂) ∘ g) s
⊢ (k : (a : S₁) → S₂) (eval₂ f g (p * X s)) =
    eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X s))
have mul_X₈ : HMul.hMul (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    ((k : (a : S₁) → S₂) (g s) : S₂) =
  HMul.hMul (β := S₂) (eval₂ k ((⇑k : (a : S₁) → S₂) ∘ g) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    ((k : (a : S₁) → S₂) (g s) : S₂)
Tactic: rw [eval₂_mul, k.map_mul, (map f).map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X, comp_apply]