-- 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 :
  Set.MapsTo (fun (x : ℕ × ℕ) ↦ Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x)
    (↑(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)))
          ⋯) :
      Set (ℕ × ℕ))
    (↑(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 _)) :
      Set ((_ : ℕ) × ℕ × ℕ))
pos₁ :
  ∀ (i : (_ : ℕ) × ℕ × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ × ℕ))
        (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 _))
        i →
      i ∉
          (fun (x : ℕ × ℕ) ↦ Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x) ''
            (↑(Set.Finite.toFinset (s :=
                  Function.support.{0, u_4} (M := V) fun (a_2 : ℕ × ℕ) ↦
                    HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.2 : (a : PowerSeries R) → R) b : R)
                      (HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.1 : (a : PowerSeries R) → R) a : R)
                        ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.1 : V⟦Γ⟧)
                              ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.2 : V⟦Γ⟧)).coeff
                          g)))
                  ⋯) :
              Set (ℕ × ℕ)) →
        HMul.hMul (α := R) (β := R)
              ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 : (a : PowerSeries R) → R) a : R)
              ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 : (a : PowerSeries R) → R) b : R) •
            (x ^ i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)).coeff g =
          0
⊢ 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)))

Tactic:
refine (Finset.sum_of_injOn (fun x => ⟨x.1 + x.2, x⟩) (fun _ _ _ _ => by simp) ?_ ?_
      (fun _ _ => by simp [smul_smul, mul_comm, pow_add])).symm

Premises used: Finset.sum_of_injOn, Eq.symm