DependsOn for functions on lists

mathlib's DependsOn f s says a function on Π i, α i is determined by the coordinates in s. A function g : List α → γ is not on a Π-type, but on each fibre Fin n → α the composite g ∘ List.ofFn is, so "g depends only on the positions in K" is ∀ n, DependsOn (g ∘ List.ofFn) (Fin.val ⁻¹' K). List.forall_dependsOn_ofFn_iff unpacks that into the word-pair form consumers use: equal-length lists whose getElem? functions are Set.EqOn on K have equal images. [UPSTREAM] candidate for Mathlib/Logic/Function/DependsOn.lean.

Main results

• List.forall_dependsOn_ofFn_iff: the word-pair form of fibrewise DependsOn.
• Set.EqOn.take_eq, Set.EqOn.drop_eq, Set.EqOn.getElem?_eq: agreement of getElem? on Set.Iic j or Set.Ici j transports prefixes and suffixes, in dot-notation form.

theorem List.forall_dependsOn_ofFn_iff {α : Type u_1} {γ : Type u_2} {K : Set ℕ} (g : List α → γ) : (∀ (n : ℕ), DependsOn (fun (x : Fin n → α) => g (ofFn x)) (Fin.val ⁻¹' K)) ↔ ∀ ⦃u v : List α⦄, u.length = v.length → Set.EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) K → g u = g v

g ∘ List.ofFn depends on the positions in K on every fibre exactly when equal-length lists agreeing on K have equal images under g.

theorem Set.EqOn.getElem?_eq {α : Type u_1} {u v : List α} {s : Set ℕ} {k : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) s) (hk : k ∈ s) : u[k]? = v[k]?

The pointwise application of window agreement, stated in getElem? form so it rewrites cleanly.

theorem Set.EqOn.take_eq {α : Type u_1} {u v : List α} {i j : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) (Iic j)) (hij : i ≤ j + 1) : List.take i u = List.take i v

Agreement on positions up to j transports prefixes of length at most j + 1.

theorem Set.EqOn.drop_eq {α : Type u_1} {u v : List α} {i j : ℕ} (h : EqOn (fun (x : ℕ) => u[x]?) (fun (x : ℕ) => v[x]?) (Ici j)) (hij : j ≤ i) : List.drop i u = List.drop i v

Agreement on positions from j transports suffixes from j on.