-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₂ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
        HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₃ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) n : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₄ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) n) *
      eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1)) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
rw₅ :
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
      (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (HPow.hPow (α := MvPolynomial σ R) (X default) (p + 1))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₆ : HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
    (HPow.hPow (α := R[X]) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (X default)) (p + 1)) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]