-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
h :
  Eq.{u_4 + 1} (α := R)
    (∑
      p_1 ∈
        Set.Finite.toFinset (s :=
          {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
            mapDomain f p.1 = x ∧ p.2 ∈ @antidiagonal _ Finsupp.instAddMonoid _ p.1})
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.2}) ⋯,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) q : R))
h₁ :
  Eq.{u_4 + 1} (α := R)
    (∑
      p_1 ∈
        Set.Finite.toFinset (s :=
          {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
            mapDomain f p.1 = x ∧ p.2 ∈ @antidiagonal _ Finsupp.instAddMonoid _ p.1})
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
    (∑
      p_1 ∈
        Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
h₂ :
  Eq.{u_4 + 1} (α := R)
    (∑
      p_1 ∈
        image
          (fun (x : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))) ↦
            match (motive :=
              Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)) x with
            | (fst, b) => (b.1 + b.2, b))
          (Set.Finite.toFinset (s :=
            {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
              p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
                p.2 ∈
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                    Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
            ⋯),
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
    (∑
      p_1 ∈
        Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
h₃ h₄ :
  Eq.{u_4 + 1} (α := R)
    (∑
      x ∈
        Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯,
      HMul.hMul (α := R) (β := R)
        ((coeff
                (match (motive :=
                      Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
                      x with
                    | (fst, b) => (b.1 + b.2, b)).2.1 :
              (a : MvPowerSeries σ R) → R)
            p :
          R)
        ((coeff
                (match (motive :=
                      Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
                      x with
                    | (fst, b) => (b.1 + b.2, b)).2.2 :
              (a : MvPowerSeries σ R) → R)
            q :
          R))
    (∑
      p_1 ∈
        Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff p_1.2.1 : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff p_1.2.2 : (a : MvPowerSeries σ R) → R) q : R))
⊢ Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯,
      ∑ p_1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
        HMul.hMul (α := R) (β := R) ((coeff p_1.1 : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff p_1.2 : (a : MvPowerSeries σ R) → R) q : R))
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.2}) ⋯,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) q : R))

Tactic:
rw [← sum_finset_product' (renameFunAux f x).toFinset _ _ (by simp),
    ← sum_finset_product' (renameFunAux' f x).toFinset _ _ (by simp),
    ← renameFunAuxImage f x, sum_image fun _ ↦ by simp; grind]

Premises used: _private.0.MvPowerSeries.renameFunAux', _private.0.MvPowerSeries.renameFunAux, _private.0.MvPowerSeries.renameFunAuxImage, Set.Finite.toFinset, Finset.sum_image, Finset.sum_finset_product'