The range of Function.updateFinset

Updating x on a finite set s reaches exactly the functions that agree with x off s, so quantifying over the values on s is quantifying over those functions.

theorem Function.mem_range_updateFinset_iff {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] {x x' : (i : ι) → π i} {s : Finset ι} : x' ∈ Set.range (updateFinset x s) ↔ ∀ i ∉ s, x' i = x i