-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₃ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₄ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₅ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f n)) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₆ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ (monomial (Finsupp.single (f n) e) : (a : R) → MvPolynomial τ R) 1 :
          MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₇ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      (monomial (s.sum fun (a : σ) ↦ Finsupp.single (f a)) : (a : R) → MvPolynomial τ R) a)
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₈ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    Finsupp.single (s.sum fun (a : σ) ↦ Finsupp.single (f a)) a)
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]