The row of an entry in a list of rows

The index of the first row containing an entry, rows.findIdx? (fun row => a ∈ row), does not change when every entry is relabelled by an injective map. Similarly, the first occurrence index of a member of a list is preserved by a map that is injective on the list.

theorem List.idxOf_map_eq_of_injectiveOn {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (w : List α) (f : α → β) (hf : ∀ ⦃x y : α⦄, x ∈ w → y ∈ w → f x = f y → x = y) {x : α} (hx : x ∈ w) : idxOf (f x) (map f w) = idxOf x w

A map that is injective on a list preserves the first occurrence index of each member.

theorem List.findIdx?_mem_map_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (rows : List (List α)) (a : α) : findIdx? (fun (row : List β) => decide (f a ∈ row)) (map (map f) rows) = findIdx? (fun (row : List α) => decide (a ∈ row)) rows

Relabelling the entries of a list of rows by an injective map does not move the row in which an entry first appears.