-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 ((_ : ℕ) × ℕ × ℕ))
⊢ 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)))
have 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)))
            sorry))
        (@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)))
                sorry) :
            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
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