Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yakov Pechersky

! This file was ported from Lean 3 source module data.list.cycle
! leanprover-community/mathlib commit 7413128c3bcb3b0818e3e18720abc9ea3100fb49
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Multiset.Sort
import Mathlib.Data.Fintype.List
import Mathlib.Data.List.Rotate

/-!
# Cycles of a list

Lists have an equivalence relation of whether they are rotational permutations of one another.
This relation is defined as `IsRotated`.

Based on this, we define the quotient of lists by the rotation relation, called `Cycle`.

We also define a representation of concrete cycles, available when viewing them in a goal state or
via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
is different.

-/

namespace List

variable {α: Type ?u.2α : Type _: Type (?u.2+1)Type _} [DecidableEq: Sort ?u.5 → Sort (max1?u.5)DecidableEq α: Type ?u.2α]

/-- Return the `z` such that `x :: z :: _` appears in `xs`, or `default` if there is no such `z`. -/
def nextOr: List α → α → α → αnextOr : ∀ (_: List α_ : List: Type ?u.27 → Type ?u.27List α: Type ?u.14α) (_: α_ _: α_ : α: Type ?u.14α), α: Type ?u.14α
| [], _, default: αdefault => default: αdefault
| [_], _, default: αdefault => default: αdefault
-- Handles the not-found and the wraparound case
| y: αy :: z: αz :: xs: List αxs, x: αx, default: αdefault => if x: αx = y: αy then z: αz else nextOr: List α → α → α → αnextOr (z: αz :: xs: List αxs) x: αx default: αdefault
#align list.next_or List.nextOr: {α : Type u_1} → [inst : DecidableEq α] → List α → α → α → αList.nextOr

@[simp]
theorem nextOr_nil: ∀ (x d : α), nextOr [] x d = dnextOr_nil (x: αx d: αd : α: Type ?u.807α) : nextOr: {α : Type ?u.824} → [inst : DecidableEq α] → List α → α → α → αnextOr []: List ?m.828[] x: αx d: αd = d: αd :=
rfl: ∀ {α : Sort ?u.873} {a : α}, a = arfl
#align list.next_or_nil List.nextOr_nil: ∀ {α : Type u_1} [inst : DecidableEq α] (x d : α), nextOr [] x d = dList.nextOr_nil

@[simp]
theorem nextOr_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y d : α), nextOr [y] x d = dnextOr_singleton (x: αx y: αy d: αd : α: Type ?u.924α) : nextOr: {α : Type ?u.943} → [inst : DecidableEq α] → List α → α → α → αnextOr [y: αy] x: αx d: αd = d: αd :=
rfl: ∀ {α : Sort ?u.995} {a : α}, a = arfl
#align list.next_or_singleton List.nextOr_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y d : α), nextOr [y] x d = dList.nextOr_singleton

@[simp]
theorem nextOr_self_cons_cons: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x y d : α), nextOr (x :: y :: xs) x d = ynextOr_self_cons_cons (xs: List αxs : List: Type ?u.1064 → Type ?u.1064List α: Type ?u.1052α) (x: αx y: αy d: αd : α: Type ?u.1052α) : nextOr: {α : Type ?u.1074} → [inst : DecidableEq α] → List α → α → α → αnextOr (x: αx :: y: αy :: xs: List αxs) x: αx d: αd = y: αy :=
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1127} {t e : α}, (if c then t else e) = tif_pos rfl: ∀ {α : Sort ?u.1130} {a : α}, a = arfl
#align list.next_or_self_cons_cons List.nextOr_self_cons_cons: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x y d : α), nextOr (x :: y :: xs) x d = yList.nextOr_self_cons_cons

theorem nextOr_cons_of_ne: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → nextOr (y :: xs) x d = nextOr xs x dnextOr_cons_of_ne (xs: List αxs : List: Type ?u.1211 → Type ?u.1211List α: Type ?u.1199α) (y: αy x: αx d: αd : α: Type ?u.1199α) (h: x ≠ yh : x: αx ≠ y: αy) :
nextOr: {α : Type ?u.1225} → [inst : DecidableEq α] → List α → α → α → αnextOr (y: αy :: xs: List αxs) x: αx d: αd = nextOr: {α : Type ?u.1270} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d: αd := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αy, x, d: αh: x ≠ ynextOr (y :: xs) x d = nextOr xs x dcases' xs: List αxs with z: ?m.1308z zs: List ?m.1308zsα: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ ynilnextOr [y] x d = nextOr [] x dα: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ yz: αzs: List αconsnextOr (y :: z :: zs) x d = nextOr (z :: zs) x d
α: Type u_1inst✝: DecidableEq αxs: List αy, x, d: αh: x ≠ ynextOr (y :: xs) x d = nextOr xs x d·α: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ ynilnextOr [y] x d = nextOr [] x d α: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ ynilnextOr [y] x d = nextOr [] x dα: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ yz: αzs: List αconsnextOr (y :: z :: zs) x d = nextOr (z :: zs) x drflGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αy, x, d: αh: x ≠ ynextOr (y :: xs) x d = nextOr xs x d·α: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ yz: αzs: List αconsnextOr (y :: z :: zs) x d = nextOr (z :: zs) x d α: Type u_1inst✝: DecidableEq αy, x, d: αh: x ≠ yz: αzs: List αconsnextOr (y :: z :: zs) x d = nextOr (z :: zs) x dexact if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1378} {t e : α}, (if c then t else e) = eif_neg h: x ≠ yhGoals accomplished! 🐙
#align list.next_or_cons_of_ne List.nextOr_cons_of_ne: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → nextOr (y :: xs) x d = nextOr xs x dList.nextOr_cons_of_ne

/-- `nextOr` does not depend on the default value, if the next value appears. -/
theorem nextOr_eq_nextOr_of_mem_of_ne: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x d d' : α) (x_mem : x ∈ xs),
x ≠ getLast xs (_ : xs ≠ []) → nextOr xs x d = nextOr xs x d'nextOr_eq_nextOr_of_mem_of_ne (xs: List αxs : List: Type ?u.1433 → Type ?u.1433List α: Type ?u.1421α) (x: αx d: αd d': αd' : α: Type ?u.1421α) (x_mem: x ∈ xsx_mem : x: αx ∈ xs: List αxs)
(x_ne: x ≠ getLast xs (_ : ?m.1481 ≠ [])x_ne : x: αx ≠ xs: List αxs.getLast: {α : Type ?u.1473} → (as : List α) → as ≠ [] → αgetLast (ne_nil_of_mem: ∀ {α : Type ?u.1478} {a : α} {l : List α}, a ∈ l → l ≠ []ne_nil_of_mem x_mem: x ∈ xsx_mem)) : nextOr: {α : Type ?u.1497} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d: αd = nextOr: {α : Type ?u.1539} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d': αd' := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'induction' xs: List αxs with y: ?m.1580y ys: List ?m.1580ys IH: ?m.1581 ysIHα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])x_mem: x ∈ []x_ne: x ≠ getLast [] (_ : [] ≠ [])nilnextOr [] x d = nextOr [] x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αys: List αIH: ∀ (x_mem : x ∈ ys), x ≠ getLast ys (_ : ys ≠ []) → nextOr ys x d = nextOr ys x d'x_mem: x ∈ y :: ysx_ne: x ≠ getLast (y :: ys) (_ : y :: ys ≠ [])consnextOr (y :: ys) x d = nextOr (y :: ys) x d'
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'·α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])x_mem: x ∈ []x_ne: x ≠ getLast [] (_ : [] ≠ [])nilnextOr [] x d = nextOr [] x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])x_mem: x ∈ []x_ne: x ≠ getLast [] (_ : [] ≠ [])nilnextOr [] x d = nextOr [] x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αys: List αIH: ∀ (x_mem : x ∈ ys), x ≠ getLast ys (_ : ys ≠ []) → nextOr ys x d = nextOr ys x d'x_mem: x ∈ y :: ysx_ne: x ≠ getLast (y :: ys) (_ : y :: ys ≠ [])consnextOr (y :: ys) x d = nextOr (y :: ys) x d'cases x_mem: x ∈ []x_memGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'cases' ys: List ?m.1580ys with z: ?m.1682z zs: List ?m.1682zsα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αIH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'x_mem: x ∈ [y]x_ne: x ≠ getLast [y] (_ : [y] ≠ [])cons.nilnextOr [y] x d = nextOr [y] x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])cons.consnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'·α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αIH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'x_mem: x ∈ [y]x_ne: x ≠ getLast [y] (_ : [y] ≠ [])cons.nilnextOr [y] x d = nextOr [y] x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αIH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'x_mem: x ∈ [y]x_ne: x ≠ getLast [y] (_ : [y] ≠ [])cons.nilnextOr [y] x d = nextOr [y] x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])cons.consnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'simp at x_mem: x ∈ [y]x_mem x_ne: x ≠ getLast [y] (_ : [y] ≠ [])x_neα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αIH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'x_ne: ¬x = yx_mem: x = ycons.nilnextOr [y] x d = nextOr [y] x d'
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y: αIH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'x_mem: x ∈ [y]x_ne: x ≠ getLast [y] (_ : [y] ≠ [])cons.nilnextOr [y] x d = nextOr [y] x d'contradictionGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'by_cases h: ?m.2095h : x: αx = y: ?m.1580yα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'·α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'rw [α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'h: ?m.2088h,α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) y d = nextOr (y :: z :: zs) y d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr_self_cons_cons: ∀ {α : Type ?u.2110} [inst : DecidableEq α] (xs : List α) (x y d : α), nextOr (x :: y :: xs) x d = ynextOr_self_cons_cons,α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposz = nextOr (y :: z :: zs) y d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr_self_cons_cons: ∀ {α : Type ?u.2317} [inst : DecidableEq α] (xs : List α) (x y d : α), nextOr (x :: y :: xs) x d = ynextOr_self_cons_consα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: x = yposz = z]Goals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem: x ∈ xsx_ne: x ≠ getLast xs (_ : xs ≠ [])nextOr xs x d = nextOr xs x d'·α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'rw [α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr: {α : Type ?u.3799} → [inst : DecidableEq α] → List α → α → α → αnextOr,α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg(if x = y then z else nextOr (z :: zs) x d) = nextOr (y :: z :: zs) x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr: {α : Type ?u.4283} → [inst : DecidableEq α] → List α → α → α → αnextOr,α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg(if x = y then z else nextOr (z :: zs) x d) = if x = y then z else nextOr (z :: zs) x d' α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'IH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'IHα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg(if x = y then z else nextOr (z :: zs) x d') = if x = y then z else nextOr (z :: zs) x d'α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_memx ∈ z :: zsα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])]α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_memx ∈ z :: zsα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'.α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_memx ∈ z :: zs α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_memx ∈ z :: zsα: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])simpa [h: ?m.2095h] using x_mem: x ∈ y :: z :: zsx_memGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = ynegnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'.α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ []) α: Type u_1inst✝: DecidableEq αxs: List αx, d, d': αx_mem✝: x ∈ xsx_ne✝: x ≠ getLast xs (_ : xs ≠ [])y, z: αzs: List αIH: ∀ (x_mem : x ∈ z :: zs), x ≠ getLast (z :: zs) (_ : z :: zs ≠ []) → nextOr (z :: zs) x d = nextOr (z :: zs) x d'x_mem: x ∈ y :: z :: zsx_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])h: ¬x = yneg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])simpa using x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])x_neGoals accomplished! 🐙
#align list.next_or_eq_next_or_of_mem_of_ne List.nextOr_eq_nextOr_of_mem_of_ne: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x d d' : α) (x_mem : x ∈ xs),
x ≠ getLast xs (_ : xs ≠ []) → nextOr xs x d = nextOr xs x d'List.nextOr_eq_nextOr_of_mem_of_ne

theorem mem_of_nextOr_ne: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, nextOr xs x d ≠ d → x ∈ xsmem_of_nextOr_ne {xs: List αxs : List: Type ?u.18059 → Type ?u.18059List α: Type ?u.18047α} {x: αx d: αd : α: Type ?u.18047α} (h: nextOr xs x d ≠ dh : nextOr: {α : Type ?u.18068} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d: αd ≠ d: αd) : x: αx ∈ xs: List αxs := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: nextOr xs x d ≠ dx ∈ xsinduction' xs: List αxs with y: ?m.18245y ys: List ?m.18245ys IH: ?m.18246 ysIHα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dh: nextOr [] x d ≠ dnilx ∈ []α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy: αys: List αIH: nextOr ys x d ≠ d → x ∈ ysh: nextOr (y :: ys) x d ≠ dconsx ∈ y :: ys
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: nextOr xs x d ≠ dx ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dh: nextOr [] x d ≠ dnilx ∈ [] α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dh: nextOr [] x d ≠ dnilx ∈ []α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy: αys: List αIH: nextOr ys x d ≠ d → x ∈ ysh: nextOr (y :: ys) x d ≠ dconsx ∈ y :: yssimp at h: nextOr [] x d ≠ dhGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: nextOr xs x d ≠ dx ∈ xscases' ys: List ?m.18245ys with z: ?m.18414z zs: List ?m.18414zsα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy: αIH: nextOr [] x d ≠ d → x ∈ []h: nextOr [y] x d ≠ dcons.nilx ∈ [y]α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zs
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: nextOr xs x d ≠ dx ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy: αIH: nextOr [] x d ≠ d → x ∈ []h: nextOr [y] x d ≠ dcons.nilx ∈ [y] α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy: αIH: nextOr [] x d ≠ d → x ∈ []h: nextOr [y] x d ≠ dcons.nilx ∈ [y]α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zssimp at h: nextOr [y] x d ≠ dhGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: nextOr xs x d ≠ dx ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zs α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zsby_cases hx: ?m.18546hx : x: αx = y: ?m.18245yα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: x = yposx ∈ y :: z :: zsα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zs
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: x = yposx ∈ y :: z :: zs α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: x = yposx ∈ y :: z :: zsα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zssimp [hx: ?m.18546hx]Goals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dcons.consx ∈ y :: z :: zs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zs α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zsrw [α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zsnextOr_cons_of_ne: ∀ {α : Type ?u.28202} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → nextOr (y :: xs) x d = nextOr xs x dnextOr_cons_of_ne _: List ?m.28203_ _: ?m.28203_ _: ?m.28203_ _: ?m.28203_ hx: ?m.18553hxα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zs]α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zs at h: nextOr (y :: z :: zs) x d ≠ dhα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zs
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: nextOr xs x d ≠ dy, z: αzs: List αIH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsh: nextOr (y :: z :: zs) x d ≠ dhx: ¬x = ynegx ∈ y :: z :: zssimpa [hx: ¬x = yhx] using IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zsIH h: nextOr (z :: zs) x d ≠ dhGoals accomplished! 🐙
#align list.mem_of_next_or_ne List.mem_of_nextOr_ne: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, nextOr xs x d ≠ d → x ∈ xsList.mem_of_nextOr_ne

theorem nextOr_concat: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} (d : α), ¬x ∈ xs → nextOr (xs ++ [x]) x d = dnextOr_concat {xs: List αxs : List: Type ?u.41495 → Type ?u.41495List α: Type ?u.41483α} {x: αx : α: Type ?u.41483α} (d: αd : α: Type ?u.41483α) (h: ¬x ∈ xsh : x: αx ∉ xs: List αxs) : nextOr: {α : Type ?u.41520} → [inst : DecidableEq α] → List α → α → α → αnextOr (xs: List αxs ++ [x: αx]) x: αx d: αd = d: αd := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: ¬x ∈ xsnextOr (xs ++ [x]) x d = dinduction' xs: List αxs with z: ?m.41643z zs: List ?m.41643zs IH: ?m.41644 zsIHα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsh: ¬x ∈ []nilnextOr ([] ++ [x]) x d = dα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zsconsnextOr (z :: zs ++ [x]) x d = d
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: ¬x ∈ xsnextOr (xs ++ [x]) x d = d·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsh: ¬x ∈ []nilnextOr ([] ++ [x]) x d = d α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsh: ¬x ∈ []nilnextOr ([] ++ [x]) x d = dα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zsconsnextOr (z :: zs ++ [x]) x d = dsimpGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh: ¬x ∈ xsnextOr (xs ++ [x]) x d = d·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zsconsnextOr (z :: zs ++ [x]) x d = d α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zsconsnextOr (z :: zs ++ [x]) x d = dobtain ⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs⟨hz: ¬x = zhz⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs, hzs: ¬x ∈ zshzs⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs⟩ := not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_or.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt mem_cons: ∀ {α : Type ?u.41818} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ lmem_cons.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: ¬x ∈ z :: zsh)α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (z :: zs ++ [x]) x d = d
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zsconsnextOr (z :: zs ++ [x]) x d = drw [α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (z :: zs ++ [x]) x d = dcons_append: ∀ {α : Type ?u.41871} (a : α) (as bs : List α), a :: as ++ bs = a :: (as ++ bs)cons_append,α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (z :: (zs ++ [x])) x d = d α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (z :: zs ++ [x]) x d = dnextOr_cons_of_ne: ∀ {α : Type ?u.41884} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → nextOr (y :: xs) x d = nextOr xs x dnextOr_cons_of_ne _: List ?m.41885_ _: ?m.41885_ _: ?m.41885_ _: ?m.41885_ hz: ¬x = zhz,α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (zs ++ [x]) x d = d α: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.intronextOr (z :: zs ++ [x]) x d = dIH: ?m.41644 zsIH hzs: ¬x ∈ zshzsα: Type u_1inst✝: DecidableEq αxs: List αx, d: αh✝: ¬x ∈ xsz: αzs: List αIH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = dh: ¬x ∈ z :: zshz: ¬x = zhzs: ¬x ∈ zscons.introd = d]Goals accomplished! 🐙
#align list.next_or_concat List.nextOr_concat: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} (d : α), ¬x ∈ xs → nextOr (xs ++ [x]) x d = dList.nextOr_concat

theorem nextOr_mem: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, d ∈ xs → nextOr xs x d ∈ xsnextOr_mem {xs: List αxs : List: Type ?u.41949 → Type ?u.41949List α: Type ?u.41937α} {x: αx d: αd : α: Type ?u.41937α} (hd: d ∈ xshd : d: αd ∈ xs: List αxs) : nextOr: {α : Type ?u.42002} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d: αd ∈ xs: List αxs := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xsrevert hd: d ∈ xshdα: Type u_1inst✝: DecidableEq αxs: List αx, d: αd ∈ xs → nextOr xs x d ∈ xs
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xssuffices ∀ (xs': List αxs' : List: Type ?u.42134 → Type ?u.42134List α: Type u_1α) (_: ∀ (x : α), x ∈ xs → x ∈ xs'_ : ∀ x: ?m.42138x ∈ xs: List αxs, x: ?m.42138x ∈ xs': List αxs') (_: d ∈ xs'_ : d: αd ∈ xs': List αxs'), nextOr: {α : Type ?u.42235} → [inst : DecidableEq α] → List α → α → α → αnextOr xs: List αxs x: αx d: αd ∈ xs': List αxs' by
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αd ∈ xs → nextOr xs x d ∈ xsexact this: ∀ (xs' : List α), (∀ (x : α), x ∈ xs → x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs'this xs: List αxs fun _: ?m.42351_ => id: ∀ {α : Sort ?u.42353}, α → αidGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xsintro xs': List αxs' hxs': ∀ (x : α), x ∈ xs → x ∈ xs'hxs' hd: d ∈ xs'hdα: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs': ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'nextOr xs x d ∈ xs'
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xsinduction' xs: List αxs with y: ?m.42394y ys: List ?m.42394ys ih: ?m.42395 ysihα: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'hxs': ∀ (x : α), x ∈ [] → x ∈ xs'nilnextOr [] x d ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y: αys: List αih: (∀ (x : α), x ∈ ys → x ∈ xs') → nextOr ys x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: ys → x ∈ xs'consnextOr (y :: ys) x d ∈ xs'
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'hxs': ∀ (x : α), x ∈ [] → x ∈ xs'nilnextOr [] x d ∈ xs' α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'hxs': ∀ (x : α), x ∈ [] → x ∈ xs'nilnextOr [] x d ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y: αys: List αih: (∀ (x : α), x ∈ ys → x ∈ xs') → nextOr ys x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: ys → x ∈ xs'consnextOr (y :: ys) x d ∈ xs'exact hd: d ∈ xs'hdGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xscases' ys: List ?m.42394ys with z: ?m.42454z zs: List ?m.42454zsα: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y: αih: (∀ (x : α), x ∈ [] → x ∈ xs') → nextOr [] x d ∈ xs'hxs': ∀ (x : α), x ∈ [y] → x ∈ xs'cons.nilnextOr [y] x d ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'cons.consnextOr (y :: z :: zs) x d ∈ xs'
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y: αih: (∀ (x : α), x ∈ [] → x ∈ xs') → nextOr [] x d ∈ xs'hxs': ∀ (x : α), x ∈ [y] → x ∈ xs'cons.nilnextOr [y] x d ∈ xs' α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y: αih: (∀ (x : α), x ∈ [] → x ∈ xs') → nextOr [] x d ∈ xs'hxs': ∀ (x : α), x ∈ [y] → x ∈ xs'cons.nilnextOr [y] x d ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'cons.consnextOr (y :: z :: zs) x d ∈ xs'exact hd: d ∈ xs'hdGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xsrw [α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'cons.consnextOr (y :: z :: zs) x d ∈ xs'nextOr: {α : Type ?u.43037} → [inst : DecidableEq α] → List α → α → α → αnextOrα: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'cons.cons(if x = y then z else nextOr (z :: zs) x d) ∈ xs']α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'cons.cons(if x = y then z else nextOr (z :: zs) x d) ∈ xs'
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xssplit_ifs with hα: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: x = ycons.cons.inlz ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: ¬x = ycons.cons.inrnextOr (z :: zs) x d ∈ xs'
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: x = ycons.cons.inlz ∈ xs' α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: x = ycons.cons.inlz ∈ xs'α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: ¬x = ycons.cons.inrnextOr (z :: zs) x d ∈ xs'exact hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'hxs' _: α_ (mem_cons_of_mem: ∀ {α : Type ?u.43418} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: lmem_cons_of_mem _: ?m.43419_ (mem_cons_self: ∀ {α : Type ?u.43428} (a : α) (l : List α), a ∈ a :: lmem_cons_self _: ?m.43429_ _: List ?m.43429_))Goals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αxs: List αx, d: αhd: d ∈ xsnextOr xs x d ∈ xs·α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: ¬x = ycons.cons.inrnextOr (z :: zs) x d ∈ xs' α: Type u_1inst✝: DecidableEq αxs: List αx, d: αxs': List αhxs'✝: ∀ (x : α), x ∈ xs → x ∈ xs'hd: d ∈ xs'y, z: αzs: List αih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'h: ¬x = ycons.cons.inrnextOr (z :: zs) x d ∈ xs'exact ih: (∀ (x : α), x ∈ z :: zs → x ∈ xs') → nextOr (z :: zs) x d ∈ xs'ih fun _: ?m.43433_ h: ?m.43436h => hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'hxs' _: α_ (mem_cons_of_mem: ∀ {α : Type ?u.43439} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: lmem_cons_of_mem _: ?m.43440_ h: ?m.43436h)Goals accomplished! 🐙
#align list.next_or_mem List.nextOr_mem: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, d ∈ xs → nextOr xs x d ∈ xsList.nextOr_mem

/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the next
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

For example:
* `next [1, 2, 3] 2 _ = 3`
* `next [1, 2, 3] 3 _ = 1`
* `next [1, 2, 3, 2, 4] 2 _ = 3`
* `next [1, 2, 3, 2] 2 _ = 3`
* `next [1, 1, 2, 3, 2] 1 _ = 1`
-/
def next: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext (l: List αl : List: Type ?u.43562 → Type ?u.43562List α: Type ?u.43550α) (x: αx : α: Type ?u.43550α) (h: x ∈ lh : x: αx ∈ l: List αl) : α: Type ?u.43550α :=
nextOr: {α : Type ?u.43600} → [inst : DecidableEq α] → List α → α → α → αnextOr l: List αl x: αx (l: List αl.get: {α : Type ?u.43680} → (as : List α) → Fin (length as) → αget ⟨0: ?m.436910, length_pos_of_mem: ∀ {α : Type ?u.43701} {a : α} {l : List α}, a ∈ l → 0 < length llength_pos_of_mem h: x ∈ lh⟩)
#align list.next List.next: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αList.next

/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the previous
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

* `prev [1, 2, 3] 2 _ = 1`
* `prev [1, 2, 3] 1 _ = 3`
* `prev [1, 2, 3, 2, 4] 2 _ = 1`
* `prev [1, 2, 3, 4, 2] 2 _ = 1`
* `prev [1, 1, 2] 1 _ = 2`
-/
def prev: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αprev : ∀ (l: List αl : List: Type ?u.43889 → Type ?u.43889List α: Type ?u.43876α) (x: αx : α: Type ?u.43876α) (_h: x ∈ l_h : x: αx ∈ l: List αl), α: Type ?u.43876α
| [], _, h: x✝ ∈ []h => byGoals accomplished! 🐙 α: Type ?u.43876inst✝: DecidableEq αx✝: αh: x✝ ∈ []αsimp at h: x✝ ∈ []hGoals accomplished! 🐙
| [y: αy], _, _ => y: αy
| y: αy :: z: αz :: xs: List αxs, x: αx, h: x ∈ y :: z :: xsh =>
if hx: ?m.44069hx : x: αx = y: αy then getLast: {α : Type ?u.44071} → (as : List α) → as ≠ [] → αgetLast (z: αz :: xs: List αxs) (cons_ne_nil: ∀ {α : Type ?u.44075} (a : α) (l : List α), a :: l ≠ []cons_ne_nil _: ?m.44076_ _: List ?m.44076_)
else if x: αx = z: αz then y: αy else prev: (l : List α) → (x : α) → x ∈ l → αprev (z: αz :: xs: List αxs) x: αx (byGoals accomplished! 🐙 α: Type ?u.43876inst✝: DecidableEq αy, z: αxs: List αx: αh: x ∈ y :: z :: xshx: ¬x = yx ∈ z :: xssimpa [hx: ¬x = yhx] using h: x ∈ y :: z :: xshGoals accomplished! 🐙)
#align list.prev List.prev: {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αList.prev

variable (l: List αl : List: Type ?u.84305 → Type ?u.84305List α: Type ?u.58478α) (x: αx : α: Type ?u.84991α)

@[simp]
theorem next_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), next [y] x h = ynext_singleton (x: αx y: αy : α: Type ?u.58478α) (h: x ∈ [y]h : x: αx ∈ [y: αy]) : next: {α : Type ?u.58533} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext [y: αy] x: αx h: x ∈ [y]h = y: αy :=
rfl: ∀ {α : Sort ?u.58584} {a : α}, a = arfl
#align list.next_singleton List.next_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), next [y] x h = yList.next_singleton

@[simp]
theorem prev_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), prev [y] x h = yprev_singleton (x: αx y: αy : α: Type ?u.58651α) (h: x ∈ [y]h : x: αx ∈ [y: αy]) : prev: {α : Type ?u.58706} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αprev [y: αy] x: αx h: x ∈ [y]h = y: αy :=
rfl: ∀ {α : Sort ?u.58757} {a : α}, a = arfl
#align list.prev_singleton List.prev_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), prev [y] x h = yList.prev_singleton

theorem next_cons_cons_eq': ∀ (y z : α) (h : x ∈ y :: z :: l), x = y → next (y :: z :: l) x h = znext_cons_cons_eq' (y: αy z: αz : α: Type ?u.58814α) (h: x ∈ y :: z :: lh : x: αx ∈ y: αy :: z: αz :: l: List αl) (hx: x = yhx : x: αx = y: αy) :
next: {α : Type ?u.58873} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext (y: αy :: z: αz :: l: List αl) x: αx h: x ∈ y :: z :: lh = z: αz := byGoals accomplished! 🐙 α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = ynext (y :: z :: l) x h = zrw [α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = ynext (y :: z :: l) x h = znext: {α : Type ?u.59143} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext,α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = ynextOr (y :: z :: l) x (get (y :: z :: l) { val := 0, isLt := (_ : 0 < length (y :: z :: l)) }) = z α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = ynext (y :: z :: l) x h = znextOr: {α : Type ?u.59641} → [inst : DecidableEq α] → List α → α → α → αnextOr,α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = y(if x = y then z else nextOr (z :: l) x (get (y :: z :: l) { val := 0, isLt := (_ : 0 < length (y :: z :: l)) })) = z α: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = ynext (y :: z :: l) x h = zif_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.59642} {t e : α}, (if c then t else e) = tif_pos hx: x = yhxα: Type u_1inst✝: DecidableEq αl: List αx, y, z: αh: x ∈ y :: z :: lhx: x = yz = z]Goals accomplished! 🐙
#align list.next_cons_cons_eq' List.next_cons_cons_eq': ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l),
x = y → next (y :: z :: l) x h = zList.next_cons_cons_eq'

@[simp]
theorem next_cons_cons_eq: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x z : α) (h : x ∈ x :: z :: l), next (x :: z :: l) x h = znext_cons_cons_eq (z: αz : α: Type ?u.59679α) (h: x ∈ x :: z :: lh : x: αx ∈ x: αx :: z: αz :: l: List αl) : next: {α : Type ?u.59732} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext (x: αx :: z: αz :: l: List αl) x: αx h: x ∈ x :: z :: lh = z: αz :=
next_cons_cons_eq': ∀ {α : Type ?u.59782} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l),
x = y → next (y :: z :: l) x h = znext_cons_cons_eq' l: List αl x: αx x: αx z: αz h: x ∈ x :: z :: lh rfl: ∀ {α : Sort ?u.59822} {a : α}, a = arfl
#align list.next_cons_cons_eq List.next_cons_cons_eq: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x z : α) (h : x ∈ x :: z :: l), next (x :: z :: l) x h = zList.next_cons_cons_eq

theorem next_ne_head_ne_getLast: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α),
x ∈ l →
∀ (y : α) (h : x ∈ y :: l) (hy : x ≠ y),
x ≠ getLast (y :: l) (_ : y :: l ≠ []) → next (y :: l) x h = next l x (_ : x ∈ l)next_ne_head_ne_getLast (h: x ∈ lh : x: αx ∈ l: List αl) (y: αy : α: Type ?u.59864α) (h: x ∈ y :: lh : x: αx ∈ y: αy :: l: List αl) (hy: x ≠ yhy : x: αx ≠ y: αy)
(hx: x ≠ getLast (y :: l) (_ : ?m.59945 :: ?m.59946 ≠ [])hx : x: αx ≠ getLast: {α : Type ?u.59939} → (as : List α) → as ≠ [] → αgetLast (y: αy :: l: List αl) (cons_ne_nil: ∀ {α : Type ?u.59943} (a : α) (l : List α), a :: l ≠ []cons_ne_nil _: ?m.59944_ _: List ?m.59944_)) :
next: {α : Type ?u.59958} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext (y: αy :: l: List αl) x: αx h: x ∈ y :: lh = next: {α : Type ?u.60002} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext l: List αl x: αx (byGoals accomplished! 🐙 α: Type ?u.59864inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x ∈ lsimpa [hy: x ≠ yhy] using h: x ∈ y :: lhGoals accomplished! 🐙) := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)rw [α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)next: {α : Type ?u.64673} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext,α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])nextOr (y :: l) x (get (y :: l) { val := 0, isLt := (_ : 0 < length (y :: l)) }) = next l x (_ : x ∈ l) α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)next: {α : Type ?u.64841} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext,α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])nextOr (y :: l) x (get (y :: l) { val := 0, isLt := (_ : 0 < length (y :: l)) }) =   nextOr l x (get l { val := 0, isLt := (_ : 0 < length l) }) α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)nextOr_cons_of_ne: ∀ {α : Type ?u.64842} [inst : DecidableEq α] (xs : List α) (y x d : α), x ≠ y → nextOr (y :: xs) x d = nextOr xs x dnextOr_cons_of_ne _: List ?m.64843_ _: ?m.64843_ _: ?m.64843_ _: ?m.64843_ hy: x ≠ yhy,α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])nextOr l x (get (y :: l) { val := 0, isLt := (_ : 0 < length (y :: l)) }) =   nextOr l x (get l { val := 0, isLt := (_ : 0 < length l) }) α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)nextOr_eq_nextOr_of_mem_of_ne: ∀ {α : Type ?u.64879} [inst : DecidableEq α] (xs : List α) (x d d' : α) (x_mem : x ∈ xs),
x ≠ getLast xs (_ : xs ≠ []) → nextOr xs x d = nextOr xs x d'nextOr_eq_nextOr_of_mem_of_neα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])nextOr l x ?d' = nextOr l x (get l { val := 0, isLt := (_ : 0 < length l) })α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])d'αα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ lα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ [])]α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ lα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ [])
α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)·α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ l α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ lα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ [])rwa [α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ lgetLast_cons: ∀ {α : Type ?u.65061} {a : α} {l : List α} (h : l ≠ []), getLast (a :: l) (_ : a :: l ≠ []) = getLast l hgetLast_consα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hx: x ≠ getLast l ?x_memx_memx ∈ lα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_meml ≠ []]α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hx: x ≠ getLast l ?x_memx_memx ∈ lα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_meml ≠ [] at hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hxα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_meml ≠ []
α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_memx ∈ lexact ne_nil_of_mem: ∀ {α : Type ?u.65090} {a : α} {l : List α}, a ∈ l → l ≠ []ne_nil_of_mem (α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_meml ≠ []byGoals accomplished! 🐙 α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])?m.65092 ∈ lassumptionGoals accomplished! 🐙)Goals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])next (y :: l) x h = next l x (_ : x ∈ l)·α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ []) α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ [])rwa [α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nex ≠ getLast l (_ : l ≠ [])getLast_cons: ∀ {α : Type ?u.65104} {a : α} {l : List α} (h : l ≠ []), getLast (a :: l) (_ : a :: l ≠ []) = getLast l hgetLast_consα: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hx: x ≠ getLast l ?x_nex_nex ≠ getLast l (_ : l ≠ [])α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nel ≠ []]α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hx: x ≠ getLast l ?x_nex_nex ≠ getLast l (_ : l ≠ [])α: Type u_1inst✝: DecidableEq αl: List αx: αh✝: x ∈ ly: αh: x ∈ y :: lhy: x ≠ yhx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])x_nel ≠ [] at hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])hxGoals accomplished! 🐙
#align list.next_ne_head_ne_last List.next_ne_head_ne_getLast: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α),
x ∈ l →
∀ (y : α) (h : x ∈ y :: l) (hy : x ≠ y),
x ≠ getLast (y :: l) (_ : y :: l ≠ []) → next (y :: l) x h = next l x (_ : x ∈ l)List.next_ne_head_ne_getLast

theorem next_cons_concat: ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y : α),
x ≠ y → ¬x ∈ l → ∀ (h : optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])), next (y :: l ++ [x]) x h = ynext_cons_concat (y: αy : α: Type ?u.65160α) (hy: x ≠ yhy : x: αx ≠ y: αy) (hx: ¬x ∈ lhx : x: αx ∉ l: List αl)
(h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])h : x: αx ∈ y: αy :: l: List αl ++ [x: αx] := mem_append_right: ∀ {α : Type ?u.65262} {a : α} (l₁ : List α) {l₂ : List α}, a ∈ l₂ → a ∈ l₁ ++ l₂mem_append_right _: List ?m.65263_ (mem_singleton_self: ∀ {α : Type ?u.65279} (a : α), a ∈ [a]mem_singleton_self x: αx)) :
next: {α : Type ?u.65284} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext (y: αy :: l: List αl ++ [x: αx]) x: αx h: optParam (x ∈ y :: l ++ [x]) (_ : ?m.65264 ∈ ?m.65265 ++ ?m.65266)h = y: αy := byGoals accomplished! 🐙
α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])next (y :: l ++ [x]) x h = yrw [α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])next (y :: l ++ [x]) x h = ynext: {α : Type ?u.65582} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → αnext,α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])nextOr (y :: l ++ [x]) x (get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) }) = y α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])next (y :: l ++ [x]) x h = ynextOr_concat: ∀ {α : Type ?u.65583} [inst : DecidableEq α] {xs : List α} {x : α} (d : α), ¬x ∈ xs → nextOr (xs ++ [x]) x d = dnextOr_concatα: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = yα: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])h¬x ∈ y :: l]α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = yα: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])h¬x ∈ y :: l
α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])next (y :: l ++ [x]) x h = y·α: Type u_1inst✝: DecidableEq αl: List αx, y: αhy: x ≠ yhx: ¬x ∈ lh: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y ```