nextOr_mem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nextOr_mem {xs : List α} {x d : α} (hd : d ∈ xs) : nextOr xs x d ∈ xs :=
  by
  revert hd
  suffices ∀ xs' : List α, (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs' by exact this xs fun _ => id
  intro xs' hxs' hd
  induction xs with
  | nil => exact hd
  | cons y ys ih => ?_
  rcases ys with - | ⟨z, zs⟩
  · exact hd
  rw [nextOr]
  split_ifs with h
  · exact hxs' _ (mem_cons_of_mem _ mem_cons_self)
  · exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)

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