no goals
α✝ : Type ?u.148808
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u_1
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : card t = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b in t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card { x // x ∈ t } = ∑ a in s, Int.natAbs (f a)
simp [ht]