-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (subst
          (HSMul.hSMul (β := MvPowerSeries σ R) a
            ((Polynomial.aeval p : (a : Polynomial R) → MvPowerSeries σ R) Polynomial.X : MvPowerSeries σ R))
          f) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₃ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₄ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) p)
          f) :
      R)
rw₅ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst (fun (s : Unit) ↦ HPow.hPow (β := ℕ) a 1 • p) f) :
      R)
rw₆ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (MvPowerSeries.subst (fun (x : Unit) ↦ a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst (fun (s : Unit) ↦ HPow.hPow (β := ℕ) a 1 • p) f) :
      R)
rw₇ rw₈ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (MvPowerSeries.subst (fun (x : Unit) ↦ a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (MvPowerSeries.subst (fun (s : Unit) ↦ a • p) f) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)

Tactic:
rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]

Premises used: PowerSeries.subst, Polynomial.coe_X, MvPowerSeries.rescale_homogeneous_eq_smul, PowerSeries.subst_coe, pow_one, MvPowerSeries.rescale_eq_subst, PowerSeries.subst_smul, Polynomial.aeval_X