mem_of_nextOr_ne — Mathlib

English

If xs.nextOr x d ≠ d, then x ∈ xs.

Русский

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

LaTeX

$$$Ne (xs.nextOr x d) \\, d\\Rightarrow x\\in xs$$$

Lean4

theorem mem_of_nextOr_ne {xs : List α} {x d : α} (h : nextOr xs x d ≠ d) : x ∈ xs :=
  by
  induction xs with
  | nil => simp at h
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at h
  · by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

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