-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
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))
⊢ 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))
have 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}) sorry ×ˢ
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) sorry})
        sorry,
    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}) sorry ×ˢ
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) sorry})
        sorry,
    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))
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]