case refine'_1
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ card (Finset.sigma univ fun a => range (Int.natAbs (f ↑a))) = ∑ a in s, Int.natAbs (f a)

case refine'_2
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ (a : α),
    a ∈ s →
      (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
          if (fun a => ↑a.fst) b = a then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
        f a
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧
      card t = ∑ a in s, Int.natAbs (f a) ∧ ∀ (a : α), a ∈ s → (∑ b in t, if g b = a then ↑(sgn b) else 0) = f a
refine'
  ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
    fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, _, _⟩
no goals
case refine'_1
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ card (Finset.sigma univ fun a => range (Int.natAbs (f ↑a))) = ∑ a in s, Int.natAbs (f a)
simp [sum_attach (f := fun a => (f a).natAbs)]
case refine'_2
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
      if (fun a => ↑a.fst) b = x then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
    f x
case refine'_2
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ (a : α),
    a ∈ s →
      (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
          if (fun a => ↑a.fst) b = a then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
        f a
intro x hx
no goals
case refine'_2
α✝ : Type ?u.131858
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
      if (fun a => ↑a.fst) b = x then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
    f x
simp [sum_sigma, hx, ← Int.sign_eq_sign, Int.sign_mul_abs, mul_comm (|f _|),
  sum_attach (s := s) (f := fun y => if y = x then f y else 0)]