-- Module: Mathlib.Algebra.MvPolynomial.Rename
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)))
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)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p

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]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.monomial_finsupp_sum_index, Finsupp.mapDomain, MvPolynomial.single_eq_monomial, MvPolynomial.eval₂, AddMonoidAlgebra.coeff, MvPolynomial.aeval_def, MvPolynomial.rename, MvPolynomial.algebraMap_eq, Function.comp_apply