HepLean Documentation

Init.Data.List.Nat.Find

theorem List.findIdx?_eq_some_le_of_findIdx?_eq_some {α : Type u_1} {xs : List α} {p q : αBool} (w : ∀ (x : α), x xsp x = trueq x = true) {i : Nat} (h : List.findIdx? p xs = some i) :
∃ (j : Nat), j i List.findIdx? q xs = some j