case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), 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 : α), a ∈ s → (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
⊢ ∃ β x sgn g,
    (∀ (b : β), ¬g b ∈ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ (a : α), a ∈ s → (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i))),
    ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) b ∈ s → Sum.elim sgn 0 b = 0
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), 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 : α), a ∈ s → (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
refine'
  ⟨Sum β (Fin (n - ∑ i in 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]⟩
case intro.intro.intro.intro.intro.intro.inl
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inl b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0

case intro.intro.intro.intro.intro.intro.inr
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i in s, Int.natAbs (f i))
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inr b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0
case intro.intro.intro.intro.intro.intro
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i))),
    ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) b ∈ s → Sum.elim sgn 0 b = 0
rintro (b | b) hb
no goals
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card (β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i))) = n
simp [hβ, h]
no goals
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i : β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i)),
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) i = a then ↑(Sum.elim sgn 0 i)
      else 0) =
    f a
simp [hf _ ha]
no goals
case intro.intro.intro.intro.intro.intro.inl
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inl b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0
cases hb (hg _)
no goals
case intro.intro.intro.intro.intro.intro.inr
α✝ : Type ?u.152227
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i in s, Int.natAbs (f i))
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inr b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0
rfl