next_ne_head_ne_getLast — Mathlib

English

If x ∈ l, and x ∈ y::l with x ≠ y, and x ≠ getLast(y::l), then next(y::l) x h = next l x …

Русский

Если x принадлежит l, и x принадлежит y::l, причём x ≠ y и x ≠ getLast(y::l), то next(y::l) x h = next l x …

LaTeX

$$$\\forall x\\in l\\ \\text{and} \\ x\\in(y::l)\\wedge x\\neq y\\wedge x\\neq getLast(y::l),\\ next(y::l)\\ x=h = next l\\ x\\dots$$$

Lean4

theorem next_ne_head_ne_getLast (h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y)
    (hx : x ≠ getLast (y :: l) (cons_ne_nil _ _)) : next (y :: l) x h = next l x (by simpa [hy] using h) :=
  by
  rw [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_of_ne]
  · assumption
  · rwa [getLast_cons] at hx

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