ZFSet.IsFinite carries no @[expose] upstream (ZFLean.Functions), so a downstream obtain/cases on an IsFinite hypothesis fails ("not an inductive datatype") — the same problem Value.ofInt has with the private-bodied ZFSet.ZFInt, same escape hatch: import all exposes the body privately. Kept to this one small file rather than reaching for import all inside Value.lean directly, so the exposure's blast radius (every private declaration of ZFLean.Functions, not just IsFinite) stays contained — Value.lean and everything downstream only ever sees the ordinary, already-exposed conclusion below.

theorem ZFSet.IsFinite.exists_witness {x : ZFSet.{u_1}} (h : x.IsFinite) : ∃ (n : ZFNat) (f : ZFSet.{u_1}) (hf : f ∈ x.funs ↑n), f.IsInjective ⋯

Unpacks x.IsFinite into its witnesses directly — same content IsFinite already carries, just through a statement whose own head is a plain ∃ (not a private-bodied def), so callers outside this file can obtain it normally.

noncomputable def ZFSet.sumUpTo (x f : ZFSet.{u_1}) (g : ZFSet.{u_1} → ℕ) (n : ZFNat) : ℕ

Sums g across the (at most) n-many elements of x that f (an injective total function into the ordinal n) accounts for, by recursion on n — Bags.tla's own DSum algorithm, adapted so f never gets restricted to a smaller domain: it stays fixed, and the recursion instead sweeps through which part of the codomain has been accounted for so far, adding g of whichever element of x (unique, by injectivity) f sends to the ordinal being peeled off.

Equations

• x.sumUpTo f g n = ZFSet.ZFNat.rec n 0 fun (k : ZFSet.ZFNat) (ih : ℕ) => if h : ∃ a ∈ x, a.pair ↑k ∈ f then ih + g h.choose else ih

theorem ZFSet.sumUpTo_zero {x f : ZFSet.{u_1}} {g : ZFSet.{u_1} → ℕ} : x.sumUpTo f g 0 = 0

sumUpTo _ _ _ 0 = 0 — nothing has been swept yet.

theorem ZFSet.sumUpTo_succ {x f : ZFSet.{u_1}} {g : ZFSet.{u_1} → ℕ} {k : ZFNat} : x.sumUpTo f g k.succ = if h : ∃ a ∈ x, a.pair ↑k ∈ f then x.sumUpTo f g k + g h.choose else x.sumUpTo f g k

sumUpTo's defining unfold at a successor: one more step of the codomain sweep.

theorem ZFSet.sumUpTo_insert_aux {x a f : ZFSet.{u_1}} {g : ZFSet.{u_1} → ℕ} (ha : a ∉ x) (hfunc : ∀ a' ∈ insert a x, ∀ (b1 b2 : ZFSet.{u_1}), a'.pair b1 ∈ f → a'.pair b2 ∈ f → b1 = b2) (hinj : ∀ a1 ∈ insert a x, ∀ a2 ∈ insert a x, ∀ (b : ZFSet.{u_1}), a1.pair b ∈ f → a2.pair b ∈ f → a1 = a2) (n : ZFNat) : (insert a x).sumUpTo f g n = x.sumUpTo f g n + if ∃ b ∈ ↑n, a.pair b ∈ f then g a else 0

Auxiliary form of sumUpTo_insert: tracks whether the sweep up to n has reached a's own slot yet, rather than assuming it has — the base case (n = 0) then needs no contradiction, and the successor case's two sub-cases (a's slot is the one just swept, or isn't) both reduce to this same statement one step down, rather than needing a separate "hasn't reached yet" lemma.

Takes plain pairwise injectivity and single-valuedness on insert a x, not an IsFunc-into-n witness — totality into a specific n doesn't carry from n + 1 down to n (an element could map to exactly the top slot n, so f restricted need not still be total into n), but neither of these depends on n at all, so the induction's ih applies unconditionally. Single-valuedness matters here specifically: without it a could pair with more than one b, and its g-value would get counted once per such b instead of exactly once.

theorem ZFSet.sumUpTo_insert {x a f : ZFSet.{u_1}} {g : ZFSet.{u_1} → ℕ} {n : ZFNat} (ha : a ∉ x) (hf : f ∈ (insert a x).funs ↑n) (hfinj : f.IsInjective ⋯) : (insert a x).sumUpTo f g n = g a + x.sumUpTo f g n

sumUpTo_insert_aux without the "has the sweep reached a yet" guard: given f genuinely total on insert a x into n (not just injective), a's slot is always reached by the time the sweep finishes, so the if always resolves true. This is sumUpTo's actual correctness statement — matches what a caller building an EvalBuiltin rule from an IsFinite witness (exists_witness, always total) will have in hand, without needing to separately show a's slot falls within range.

noncomputable def ZFSet.IsFinite.sum {x : ZFSet.{u_1}} (h : x.IsFinite) (g : ZFSet.{u_1} → ℕ) : ℕ

The sum of g across every element of x, given x finite. IsFinite erases its witness (a bare ∃), so n/f come out via Classical.choose, not obtain — destructuring a Prop to build ℕ data is exactly what Exists.casesOn refuses.

Equations

• h.sum g = x.sumUpTo ⋯.choose g ⋯.choose

theorem ZFSet.sumUpTo_congr {x f : ZFSet.{u_1}} {g₁ g₂ : ZFSet.{u_1} → ℕ} {n : ZFNat} (h : ∀ a ∈ x, g₁ a = g₂ a) : x.sumUpTo f g₁ n = x.sumUpTo f g₂ n

sumUpTo only ever calls g at elements of x (sumUpTo_succ's own h.choose ∈ x), so two gs agreeing there sum the same — the sweep itself (x/f/n) is untouched.

theorem ZFSet.IsFinite.sum_congr {x : ZFSet.{u_1}} (hx : x.IsFinite) {g₁ g₂ : ZFSet.{u_1} → ℕ} (h : ∀ a ∈ x, g₁ a = g₂ a) : hx.sum g₁ = hx.sum g₂

IsFinite.sum at two gs agreeing on x — sumUpTo_congr through the fixed witness enumeration IsFinite.sum itself uses.