-- Mathlib/Data/Sign.lean
theorem exists_signed_sum' {α : Type u_1} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ)
    (n : ℕ) (h : (∑ i ∈ s, (f i).natAbs) ≤ n) :
    ∃ (β : Type u_1) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
      (∀ b, g b ∉ s → sgn b = 0) ∧
        Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then (sgn i : ℤ) else 0) = f a

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
    Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0

Tactic:
rintro (b | b) hb

Result:
case intro.intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inl b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0

case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i ∈ s, (f i).natAbs)
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inr b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0

Proof state:
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i ∈ s, (f i).natAbs)
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inr b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inl b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0

Tactic:
cases hb (hg _)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∃ β x sgn g,
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a

Tactic:
refine
  ⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
    Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)),
      ?_, by simp [hβ, h], fun a ha => by simp [hf _ ha]⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
    Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0

Proof state:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card (β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)) = n

Tactic:
simp [hβ, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs),
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) i = a then ↑(Sum.elim sgn 0 i) else 0) =
    f a

Tactic:
simp [hf _ ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
⊢ ∃ β x sgn g,
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a

Tactic:
obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∃ β x sgn g,
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a