-- 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 q : MvPolynomial S₂ R
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₁)
hq :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g q) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q) :
      MvPolynomial S₃ S₁)
add :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p + eval₂ C g q) : 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 + q)) :
      MvPolynomial S₃ S₁)
add₁ :
  HAdd.hAdd (α := 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 q) : 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 + q))
add₂ :
  HAdd.hAdd (α := 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 q) : 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 + q))
add₃ :
  HAdd.hAdd (α := 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)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q)) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p + q))
add₄ :
  HAdd.hAdd (α := 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)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q)) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      (HAdd.hAdd (α := 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₁) q : MvPolynomial S₂ S₁))
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p + q)) : 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 + q)) :
      MvPolynomial S₃ S₁)
have add₅ : HAdd.hAdd (α := 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)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q)) =
  HAdd.hAdd (α := 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)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) q))
Tactic: rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]