nextOr_eq_nextOr_of_mem_of_ne — Mathlib

English

If nextOr xs x d ≠ d, then x belongs to xs.

Русский

Если nextOr xs x d не равно d, то x принадлежит xs.

LaTeX

$$$nextOr\\ xs\\ x\\ d \\ne d\\Rightarrow x\\in xs$$$

Lean4

/-- `nextOr` does not depend on the default value, if the next value appears. -/
theorem nextOr_eq_nextOr_of_mem_of_ne (xs : List α) (x d d' : α) (x_mem : x ∈ xs)
    (x_ne : x ≠ xs.getLast (ne_nil_of_mem x_mem)) : nextOr xs x d = nextOr xs x d' :=
  by
  induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at x_mem x_ne
    contradiction
  by_cases h : x = y
  · rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
  · rw [nextOr, nextOr, IH]
    · simpa [h] using x_mem
    · simpa using x_ne

Похожие утверждения