-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
pos :
  Eq.{u_4 + 1} (α := V)
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : ℕ) ↦ ℕ × ℕ)
          (image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
            (Set.Finite.toFinset (s :=
              Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
                HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                  (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                    ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                          ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                      g)))
              ⋯))
          (@antidiagonal _ Nat.instAddMonoid _),
      HMul.hMul (α := R) (β := R)
          ((PowerSeries.coeff x_1.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 : (a : PowerSeries R) → R) a : R)
          ((PowerSeries.coeff x_1.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 : (a : PowerSeries R) → R) b : R) •
        (x ^ x_1.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)).coeff g)
    (∑
      x_1 ∈
        Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))
⊢ Eq.{u_4 + 1} (α := V)
    (∑
      x_1 ∈
        image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                  ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                        ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                    g)))
            ⋯),
      ∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ x_1,
        HMul.hMul (α := R) (β := R) ((PowerSeries.coeff i.1 : (a : PowerSeries R) → R) a : R)
            ((PowerSeries.coeff i.2 : (a : PowerSeries R) → R) b : R) •
          (x ^ x_1).coeff g)
    (∑
      x_1 ∈
        Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))

Tactic:
rw [sum_sigma']

Premises used: Finset.sum_sigma'