/-
Copyright (c) 2021 Yakov Pechersky. All rights reserved.
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.27
List α: 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 = d
nextOr_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 = a
rfl
#align list.next_or_nil List.nextOr_nil: ∀ {α : Type u_1} [inst : DecidableEq α] (x d : α), nextOr [] x d = d
List.nextOr_nil

@[simp]
theorem nextOr_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y d : α), nextOr [y] x d = d
nextOr_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 = a
rfl
#align list.next_or_singleton List.nextOr_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y d : α), nextOr [y] x d = d
List.nextOr_singleton

@[simp]
theorem nextOr_self_cons_cons: ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x y d : α), nextOr (x :: y :: xs) x d = y
nextOr_self_cons_cons (xs: List α
xs : List: Type ?u.1064 → Type ?u.1064
List α: 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) = t
if_pos rfl: ∀ {α : Sort ?u.1130} {a : α}, a = a
rfl
#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 = y
List.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 d
nextOr_cons_of_ne (xs: List α
xs : List: Type ?u.1211 → Type ?u.1211
List α: Type ?u.1199
α) (y: α
y x: α
x d: α
d : α: Type ?u.1199
α) (h: x ≠ y
h : 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 := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

y, x, d: α

h: x ≠ y

nextOr (y :: xs) x d = nextOr xs x dcases' xs: List α
xs with z: ?m.1308
z zs: List ?m.1308
zsα: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

nilnextOr [y] x d = nextOr [] x d
α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

z: α

zs: List α

consnextOr (y :: z :: zs) x d = nextOr (z :: zs) x d
  α: Type u_1

inst✝: DecidableEq α

xs: List α

y, x, d: α

h: x ≠ y

nextOr (y :: xs) x d = nextOr xs x d·α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

nilnextOr [y] x d = nextOr [] x d α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

nilnextOr [y] x d = nextOr [] x d
α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

z: α

zs: List α

consnextOr (y :: z :: zs) x d = nextOr (z :: zs) x drfl
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

y, x, d: α

h: x ≠ y

nextOr (y :: xs) x d = nextOr xs x d·α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

z: α

zs: List α

consnextOr (y :: z :: zs) x d = nextOr (z :: zs) x d α: Type u_1

inst✝: DecidableEq α

y, x, d: α

h: x ≠ y

z: α

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) = e
if_neg h: x ≠ y
h
Goals 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 d
List.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.1433
List α: Type ?u.1421
α) (x: α
x d: α
d d': α
d' : α: Type ?u.1421
α) (x_mem: x ∈ xs
x_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 ∈ xs
x_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' := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'induction' xs: List α
xs with y: ?m.1580
y ys: List ?m.1580
ys IH: ?m.1581 ys
IHα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_ne✝: x ≠ getLast xs (_ : xs ≠ [])

x_mem: x ∈ []

x_ne: x ≠ getLast [] (_ : [] ≠ [])

nilnextOr [] x d = nextOr [] x d'
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: ys

x_ne: x ≠ getLast (y :: ys) (_ : y :: ys ≠ [])

consnextOr (y :: ys) x d = nextOr (y :: ys) x d'
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_ne✝: x ≠ getLast xs (_ : xs ≠ [])

x_mem: x ∈ []

x_ne: x ≠ getLast [] (_ : [] ≠ [])

nilnextOr [] x d = nextOr [] x d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_ne✝: x ≠ getLast xs (_ : xs ≠ [])

x_mem: x ∈ []

x_ne: x ≠ getLast [] (_ : [] ≠ [])

nilnextOr [] x d = nextOr [] x d'
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: ys

x_ne: x ≠ getLast (y :: ys) (_ : y :: ys ≠ [])

consnextOr (y :: ys) x d = nextOr (y :: ys) x d'cases x_mem: x ∈ []
x_mem
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'cases' ys: List ?m.1580
ys with z: ?m.1682
z zs: List ?m.1682
zsα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

cons.consnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_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_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_ne✝: x ≠ getLast xs (_ : xs ≠ [])

y: α

IH: ∀ (x_mem : x ∈ []), x ≠ getLast [] (_ : [] ≠ []) → nextOr [] x d = nextOr [] x d'

x_ne: ¬x = y

x_mem: x = y

cons.nilnextOr [y] x d = nextOr [y] x d'
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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'contradiction
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'by_cases h: ?m.2095
h : x: α
x = y: ?m.1580
yα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'rw [α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'h: ?m.2088
h,α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (y :: z :: zs) y d = nextOr (y :: z :: zs) y d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (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 = y
nextOr_self_cons_cons,α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posz = nextOr (y :: z :: zs) y d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posnextOr (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 = y
nextOr_self_cons_consα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: x = y

posz = z]
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem: x ∈ xs

x_ne: x ≠ getLast xs (_ : xs ≠ [])

nextOr xs x d = nextOr xs x d'·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'rw [α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr: {α : Type ?u.3799} → [inst : DecidableEq α] → List α → α → α → α
nextOr,α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg(if x = y then z else nextOr (z :: zs) x d) = nextOr (y :: z :: zs) x d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'nextOr: {α : Type ?u.4283} → [inst : DecidableEq α] → List α → α → α → α
nextOr,α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg(if x = y then z else nextOr (z :: zs) x d) = if x = y then z else nextOr (z :: zs) x d' α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (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_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg(if x = y then z else nextOr (z :: zs) x d') = if x = y then z else nextOr (z :: zs) x d'
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_memx ∈ z :: zs
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])]α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_memx ∈ z :: zs
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'.α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_memx ∈ z :: zs α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_memx ∈ z :: zs
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])simpa [h: ?m.2095
h] using x_mem: x ∈ y :: z :: zs
x_mem
Goals accomplished! 🐙
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

negnextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'.α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ []) α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d, d': α

x_mem✝: x ∈ xs

x_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 :: zs

x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])

h: ¬x = y

neg.x_nex ≠ getLast (z :: zs) (_ : z :: zs ≠ [])simpa using x_ne: x ≠ getLast (y :: z :: zs) (_ : y :: z :: zs ≠ [])
x_ne
Goals 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 ∈ xs
mem_of_nextOr_ne {xs: List α
xs : List: Type ?u.18059 → Type ?u.18059
List α: Type ?u.18047
α} {x: α
x d: α
d : α: Type ?u.18047
α} (h: nextOr xs x d ≠ d
h : nextOr: {α : Type ?u.18068} → [inst : DecidableEq α] → List α → α → α → α
nextOr xs: List α
xs x: α
x d: α
d ≠ d: α
d) : x: α
x ∈ xs: List α
xs := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: nextOr xs x d ≠ d

x ∈ xsinduction' xs: List α
xs with y: ?m.18245
y ys: List ?m.18245
ys IH: ?m.18246 ys
IHα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

h: nextOr [] x d ≠ d

nilx ∈ []
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y: α

ys: List α

IH: nextOr ys x d ≠ d → x ∈ ys

h: nextOr (y :: ys) x d ≠ d

consx ∈ y :: ys
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: nextOr xs x d ≠ d

x ∈ xs·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

h: nextOr [] x d ≠ d

nilx ∈ [] α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

h: nextOr [] x d ≠ d

nilx ∈ []
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y: α

ys: List α

IH: nextOr ys x d ≠ d → x ∈ ys

h: nextOr (y :: ys) x d ≠ d

consx ∈ y :: yssimp at h: nextOr [] x d ≠ d
h
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: nextOr xs x d ≠ d

x ∈ xscases' ys: List ?m.18245
ys with z: ?m.18414
z zs: List ?m.18414
zsα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y: α

IH: nextOr [] x d ≠ d → x ∈ []

h: nextOr [y] x d ≠ d

cons.nilx ∈ [y]
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zs
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: nextOr xs x d ≠ d

x ∈ xs·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y: α

IH: nextOr [] x d ≠ d → x ∈ []

h: nextOr [y] x d ≠ d

cons.nilx ∈ [y] α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y: α

IH: nextOr [] x d ≠ d → x ∈ []

h: nextOr [y] x d ≠ d

cons.nilx ∈ [y]
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zssimp at h: nextOr [y] x d ≠ d
h
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: nextOr xs x d ≠ d

x ∈ xs·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zs α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zsby_cases hx: ?m.18546
hx : x: α
x = y: ?m.18245
yα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: x = y

posx ∈ y :: z :: zs
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zs
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zs·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: x = y

posx ∈ y :: z :: zs α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: x = y

posx ∈ y :: z :: zs
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zssimp [hx: ?m.18546
hx]
Goals accomplished! 🐙
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

cons.consx ∈ y :: z :: zs·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zs α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zsrw [α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ 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 d
nextOr_cons_of_ne _: List ?m.28203
_ _: ?m.28203
_ _: ?m.28203
_ _: ?m.28203
_ hx: ?m.18553
hxα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zs]α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zs at h: nextOr (y :: z :: zs) x d ≠ d
hα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zs
      α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: nextOr xs x d ≠ d

y, z: α

zs: List α

IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs

h: nextOr (y :: z :: zs) x d ≠ d

hx: ¬x = y

negx ∈ y :: z :: zssimpa [hx: ¬x = y
hx] using IH: nextOr (z :: zs) x d ≠ d → x ∈ z :: zs
IH h: nextOr (z :: zs) x d ≠ d
h
Goals 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 ∈ xs
List.mem_of_nextOr_ne

theorem nextOr_concat: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x : α} (d : α), ¬x ∈ xs → nextOr (xs ++ [x]) x d = d
nextOr_concat {xs: List α
xs : List: Type ?u.41495 → Type ?u.41495
List α: Type ?u.41483
α} {x: α
x : α: Type ?u.41483
α} (d: α
d : α: Type ?u.41483
α) (h: ¬x ∈ xs
h : x: α
x ∉ xs: List α
xs) : nextOr: {α : Type ?u.41520} → [inst : DecidableEq α] → List α → α → α → α
nextOr (xs: List α
xs ++ [x: α
x]) x: α
x d: α
d = d: α
d := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: ¬x ∈ xs

nextOr (xs ++ [x]) x d = dinduction' xs: List α
xs with z: ?m.41643
z zs: List ?m.41643
zs IH: ?m.41644 zs
IHα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

h: ¬x ∈ []

nilnextOr ([] ++ [x]) x d = d
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

consnextOr (z :: zs ++ [x]) x d = d
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: ¬x ∈ xs

nextOr (xs ++ [x]) x d = d·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

h: ¬x ∈ []

nilnextOr ([] ++ [x]) x d = d α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

h: ¬x ∈ []

nilnextOr ([] ++ [x]) x d = d
α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

consnextOr (z :: zs ++ [x]) x d = dsimp
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h: ¬x ∈ xs

nextOr (xs ++ [x]) x d = d·α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

consnextOr (z :: zs ++ [x]) x d = d α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

consnextOr (z :: zs ++ [x]) x d = dobtain ⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs
⟨hz: ¬x = z
hz⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs
, hzs: ¬x ∈ zs
hzs⟨hz, hzs⟩: ¬x = z ∧ ¬x ∈ zs
⟩ := not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬q
not_or.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt mem_cons: ∀ {α : Type ?u.41818} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
mem_cons.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: ¬x ∈ z :: zs
h)α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.intronextOr (z :: zs ++ [x]) x d = d
    α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

consnextOr (z :: zs ++ [x]) x d = drw [α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.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_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.intronextOr (z :: (zs ++ [x])) x d = d α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.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 d
nextOr_cons_of_ne _: List ?m.41885
_ _: ?m.41885
_ _: ?m.41885
_ _: ?m.41885
_ hz: ¬x = z
hz,α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.intronextOr (zs ++ [x]) x d = d α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.intronextOr (z :: zs ++ [x]) x d = dIH: ?m.41644 zs
IH hzs: ¬x ∈ zs
hzsα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

h✝: ¬x ∈ xs

z: α

zs: List α

IH: ¬x ∈ zs → nextOr (zs ++ [x]) x d = d

h: ¬x ∈ z :: zs

hz: ¬x = z

hzs: ¬x ∈ zs

cons.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 = d
List.nextOr_concat

theorem nextOr_mem: ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, d ∈ xs → nextOr xs x d ∈ xs
nextOr_mem {xs: List α
xs : List: Type ?u.41949 → Type ?u.41949
List α: Type ?u.41937
α} {x: α
x d: α
d : α: Type ?u.41937
α} (hd: d ∈ xs
hd : d: α
d ∈ xs: List α
xs) : nextOr: {α : Type ?u.42002} → [inst : DecidableEq α] → List α → α → α → α
nextOr xs: List α
xs x: α
x d: α
d ∈ xs: List α
xs := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xsrevert hd: d ∈ xs
hdα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

d ∈ xs → nextOr xs x d ∈ xs
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xssuffices ∀ (xs': List α
xs' : List: Type ?u.42134 → Type ?u.42134
List α: Type u_1
α) (_: ∀ (x : α), x ∈ xs → x ∈ xs'
_ : ∀ x: ?m.42138
x ∈ xs: List α
xs, x: ?m.42138
x ∈ 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_1

inst✝: 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}, α → α
id
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xsintro xs': List α
xs' hxs': ∀ (x : α), x ∈ xs → x ∈ xs'
hxs' hd: d ∈ xs'
hdα: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

xs': List α

hxs': ∀ (x : α), x ∈ xs → x ∈ xs'

hd: d ∈ xs'

nextOr xs x d ∈ xs'
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xsinduction' xs: List α
xs with y: ?m.42394
y ys: List ?m.42394
ys ih: ?m.42395 ys
ihα: Type u_1

inst✝: 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_1

inst✝: 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_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xs·α: Type u_1

inst✝: 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_1

inst✝: 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_1

inst✝: 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'
hd
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xscases' ys: List ?m.42394
ys with z: ?m.42454
z zs: List ?m.42454
zsα: Type u_1

inst✝: 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_1

inst✝: 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_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xs·α: Type u_1

inst✝: 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_1

inst✝: 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_1

inst✝: 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'
hd
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xsrw [α: Type u_1

inst✝: 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_1

inst✝: 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_1

inst✝: 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_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xssplit_ifs with hα: Type u_1

inst✝: 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 = y

cons.cons.inlz ∈ xs'
α: Type u_1

inst✝: 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 = y

cons.cons.inrnextOr (z :: zs) x d ∈ xs'
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xs·α: Type u_1

inst✝: 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 = y

cons.cons.inlz ∈ xs' α: Type u_1

inst✝: 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 = y

cons.cons.inlz ∈ xs'
α: Type u_1

inst✝: 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 = y

cons.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 :: l
mem_cons_of_mem _: ?m.43419
_ (mem_cons_self: ∀ {α : Type ?u.43428} (a : α) (l : List α), a ∈ a :: l
mem_cons_self _: ?m.43429
_ _: List ?m.43429
_))
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

xs: List α

x, d: α

hd: d ∈ xs

nextOr xs x d ∈ xs·α: Type u_1

inst✝: 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 = y

cons.cons.inrnextOr (z :: zs) x d ∈ xs' α: Type u_1

inst✝: 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 = y

cons.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.43436
h => hxs': ∀ (x : α), x ∈ y :: z :: zs → x ∈ xs'
hxs' _: α
_ (mem_cons_of_mem: ∀ {α : Type ?u.43439} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
mem_cons_of_mem _: ?m.43440
_ h: ?m.43436
h)
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 ∈ xs
List.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.43562
List α: Type ?u.43550
α) (x: α
x : α: Type ?u.43550
α) (h: x ∈ l
h : 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.43691
0, length_pos_of_mem: ∀ {α : Type ?u.43701} {a : α} {l : List α}, a ∈ l → 0 < length l
length_pos_of_mem h: x ∈ l
h⟩)
#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.43889
List α: Type ?u.43876
α) (x: α
x : α: Type ?u.43876
α) (_h: x ∈ l
_h : x: α
x ∈ l: List α
l), α: Type ?u.43876
α
  | [], _, h: x✝ ∈ []
h => by
Goals accomplished! 🐙 α: Type ?u.43876

inst✝: DecidableEq α

x✝: α

h: x✝ ∈ []

αsimp at h: x✝ ∈ []
h
Goals accomplished! 🐙
  | [y: α
y], _, _ => y: α
y
  | y: α
y :: z: α
z :: xs: List α
xs, x: α
x, h: x ∈ y :: z :: xs
h =>
    if hx: ?m.44069
hx : 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 (by
Goals accomplished! 🐙 α: Type ?u.43876

inst✝: DecidableEq α

y, z: α

xs: List α

x: α

h: x ∈ y :: z :: xs

hx: ¬x = y

x ∈ z :: xssimpa [hx: ¬x = y
hx] using h: x ∈ y :: z :: xs
h
Goals 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.84305
List α: 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 = y
next_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 = a
rfl
#align list.next_singleton List.next_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), next [y] x h = y
List.next_singleton

@[simp]
theorem prev_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), prev [y] x h = y
prev_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 = a
rfl
#align list.prev_singleton List.prev_singleton: ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), prev [y] x h = y
List.prev_singleton

theorem next_cons_cons_eq': ∀ (y z : α) (h : x ∈ y :: z :: l), x = y → next (y :: z :: l) x h = z
next_cons_cons_eq' (y: α
y z: α
z : α: Type ?u.58814
α) (h: x ∈ y :: z :: l
h : x: α
x ∈ y: α
y :: z: α
z :: l: List α
l) (hx: x = y
hx : 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 :: l
h = z: α
z := by
Goals accomplished! 🐙 α: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

next (y :: z :: l) x h = zrw [α: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

next (y :: z :: l) x h = znext: {α : Type ?u.59143} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → α
next,α: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

nextOr (y :: z :: l) x (get (y :: z :: l) { val := 0, isLt := (_ : 0 < length (y :: z :: l)) }) = z α: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

next (y :: z :: l) x h = znextOr: {α : Type ?u.59641} → [inst : DecidableEq α] → List α → α → α → α
nextOr,α: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: 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_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

next (y :: z :: l) x h = zif_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.59642} {t e : α}, (if c then t else e) = t
if_pos hx: x = y
hxα: Type u_1

inst✝: DecidableEq α

l: List α

x, y, z: α

h: x ∈ y :: z :: l

hx: x = y

z = 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 = z
List.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 = z
next_cons_cons_eq (z: α
z : α: Type ?u.59679
α) (h: x ∈ x :: z :: l
h : 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 :: l
h = 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 = z
next_cons_cons_eq' l: List α
l x: α
x x: α
x z: α
z h: x ∈ x :: z :: l
h rfl: ∀ {α : Sort ?u.59822} {a : α}, a = a
rfl
#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 = z
List.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 ∈ l
h : x: α
x ∈ l: List α
l) (y: α
y : α: Type ?u.59864
α) (h: x ∈ y :: l
h : x: α
x ∈ y: α
y :: l: List α
l) (hy: x ≠ y
hy : 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 :: l
h = next: {α : Type ?u.60002} → [inst : DecidableEq α] → (l : List α) → (x : α) → x ∈ l → α
next l: List α
l x: α
x (by
Goals accomplished! 🐙 α: Type ?u.59864

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x ∈ lsimpa [hy: x ≠ y
hy] using h: x ∈ y :: l
h
Goals accomplished! 🐙) := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

next (y :: l) x h = next l x (_ : x ∈ l)rw [α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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 d
nextOr_cons_of_ne _: List ?m.64843
_ _: ?m.64843
_ _: ?m.64843
_ _: ?m.64843
_ hy: x ≠ y
hy,α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

nextOr l x ?d' = nextOr l x (get l { val := 0, isLt := (_ : 0 < length l) })
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

d'α
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_memx ∈ l
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nex ≠ getLast l (_ : l ≠ [])]α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_memx ∈ l
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nex ≠ getLast l (_ : l ≠ [])
  α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

next (y :: l) x h = next l x (_ : x ∈ l)·α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_memx ∈ l α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_memx ∈ l
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nex ≠ getLast l (_ : l ≠ [])rwa [α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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 h
getLast_consα: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

hx: x ≠ getLast l ?x_mem

x_memx ∈ l
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_meml ≠ []]α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

hx: x ≠ getLast l ?x_mem

x_memx ∈ l
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_meml ≠ [] at hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])
hxα: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_meml ≠ []
    α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_meml ≠ []by
Goals accomplished! 🐙 α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

?m.65092 ∈ lassumption
Goals accomplished! 🐙)
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

next (y :: l) x h = next l x (_ : x ∈ l)·α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nex ≠ getLast l (_ : l ≠ []) α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nex ≠ getLast l (_ : l ≠ [])rwa [α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: 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 h
getLast_consα: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

hx: x ≠ getLast l ?x_ne

x_nex ≠ getLast l (_ : l ≠ [])
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nel ≠ []]α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx✝: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

hx: x ≠ getLast l ?x_ne

x_nex ≠ getLast l (_ : l ≠ [])
α: Type u_1

inst✝: DecidableEq α

l: List α

x: α

h✝: x ∈ l

y: α

h: x ∈ y :: l

hy: x ≠ y

hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])

x_nel ≠ [] at hx: x ≠ getLast (y :: l) (_ : y :: l ≠ [])
hx
Goals 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 = y
next_cons_concat (y: α
y : α: Type ?u.65160
α) (hy: x ≠ y
hy : x: α
x ≠ y: α
y) (hx: ¬x ∈ l
hx : 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 := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

next (y :: l ++ [x]) x h = yrw [α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: 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_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: 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_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: 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 = d
nextOr_concatα: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y
α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

h¬x ∈ y :: l]α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y
α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

h¬x ∈ y :: l
  α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

next (y :: l ++ [x]) x h = y·α: Type u_1

inst✝: DecidableEq α

l: List α

x, y: α

hy: x ≠ y

hx: ¬x ∈ l

h: optParam (x ∈ y :: l ++ [x]) (_ : x ∈ y :: l ++ [x])

get (y :: l ++ [x]) { val := 0, isLt := (_ : 0 < length (y :: l ++ [x])) } = y