-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
h :
  ∀ (n : τ →₀ ℕ),
    Eq.{u_6 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries τ R) → R)
          ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
        R)
      ((coeff n : (a : MvPowerSeries τ R) → R) (subst (X ∘ f) p) : R)
h₁ :
  ∀ (n : τ →₀ ℕ),
    Eq.{u_6 + 1} (α := R)
      (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
      (∑
        i ∈
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
              HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
                ((coeff n : (a : MvPowerSeries τ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                  R))
            ⋯,
        HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (i.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
h₂ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n),
    Eq.{u_6 + 1} (α := R)
      (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
      (∑
        i ∈
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
              HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
                ((coeff n : (a : MvPowerSeries τ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                  R))
            ⋯,
        HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (i.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
h₃ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n),
    Set.Finite.toFinset (s :=
        Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
            ((coeff n : (a : MvPowerSeries τ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
              R))
        ⋯ ⊆
      Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯
h₄ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n),
    ∀
      x ∈
        Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯ \
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
              HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
                ((coeff n : (a : MvPowerSeries τ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                  R))
            ⋯,
      Eq.{u_6 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
h₅ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n)
    (x : σ →₀ ℕ)
    (hx :
      x ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯),
    HSMul.hSMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R) =
      (coeff x : (a : MvPowerSeries σ R) → R) p
h₆ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n),
    ∀
      x ∈
        Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯ \
          Set.Finite.toFinset (s :=
            Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
              HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
                ((coeff n : (a : MvPowerSeries τ R) → R)
                    (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                  R))
            ⋯,
      Eq.{u_6 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
h₇ h₈ :
  ∀ (n : τ →₀ ℕ)
    (this :
      ∀ (d : σ →₀ ℕ)
        (hd :
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
                R) ≠
            0),
        mapDomain f d = n)
    (x : σ →₀ ℕ)
    (hx :
      x ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯),
    HSMul.hSMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R) =
      (coeff x : (a : MvPowerSeries σ R) → R) p
⊢ Eq (α := MvPowerSeries τ R) ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R)
    (subst (X ∘ f) p : MvPowerSeries τ R)

Tactic:
classical
  ext n
  rw [coeff_rename, coeff_subst (HasSubst.X_comp _) p n, finsum_eq_sum _
    (coeff_subst_finite (HasSubst.X_comp _) p n)]
  have (d : σ →₀ ℕ) (hd : (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0) :
      mapDomain f d = n := by
    simp_rw [← monomial_mapDomain_apply_one] at hd
    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm
  refine (Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm
  · exact Set.Finite.toFinset_mono this
  · simp +contextual [← monomial_mapDomain_apply_one]
  · simp only [Set.Finite.mem_toFinset] at hx
    simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

Premises used: Set.Finite.mem_toFinset, MvPowerSeries.coeff_monomial_same, MvPowerSeries.coeff_rename, Eq.symm, MvPowerSeries.monomial_mapDomain_apply_one, Finset.sum_subset_zero_on_sdiff