-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f) : R)
h₁ :
  ∀ (n : σ →₀ ℕ),
    HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
      (coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f)
h₂ :
  ∀ (n : σ →₀ ℕ),
    HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
      ∑
        i ∈
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
              HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
                ((coeff n : (a : MvPowerSeries σ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
                  R))
            ⋯,
        HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (i.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
            R)
h₃ :
  ∀ (n : σ →₀ ℕ),
    HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
      ∑
        d ∈
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
              HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
                ((coeff n : (a : MvPowerSeries σ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                  R))
            ⋯,
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R)
h₄ :
  ∀ (n : σ →₀ ℕ),
    HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
      HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R)
ext :
  ∀ (n b : σ →₀ ℕ),
    b ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯ →
      b ≠ n →
        HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R) =
          0
ext₁ :
  ∀
    n ∉
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        ⋯,
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R) =
      0
ext₂ :
  ∀ (n b : σ →₀ ℕ),
    b ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯ →
      b ≠ n →
        HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R) =
          0
ext₃ ext₄ :
  ∀
    n ∉
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        ⋯,
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R) =
      0
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f

Tactic:
classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn

Premises used: Pi.smul_apply', MvPowerSeries.coeff_subst, MulZeroClass.mul_zero, MvPowerSeries.coeff_rescale, MvPowerSeries.coeff_monomial, MvPowerSeries.HasSubst.smul_X, mul_comm, MvPowerSeries.monomial_eq, smul_eq_mul