case nil
α : 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 [] (_ : [] ≠ [])
⊢ nextOr [] x d = nextOr [] x d'

case cons
α : 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 ≠ [])
⊢ nextOr (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'
induction' xs with y ys IH
case cons.nil
α : 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] ≠ [])
⊢ nextOr [y] x d = nextOr [y] x d'

case 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 ≠ [])
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
case cons
α : 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 ≠ [])
⊢ nextOr (y :: ys) x d = nextOr (y :: ys) x d'
cases' ys with z zs
case pos
α : 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
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'

case neg
α : 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
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
case 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 ≠ [])
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
by_cases h : x = y
no goals
case nil
α : 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 [] (_ : [] ≠ [])
⊢ nextOr [] x d = nextOr [] x d'
cases x_mem
case cons.nil
α : 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
⊢ nextOr [y] x d = nextOr [y] x d'
case cons.nil
α : 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] ≠ [])
⊢ nextOr [y] x d = nextOr [y] x d'
simp at x_mem x_ne
no goals
case cons.nil
α : 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
⊢ nextOr [y] x d = nextOr [y] x d'
contradiction
no goals
case pos
α : 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
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
case neg.x_mem
α : 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
⊢ x ∈ z :: zs

case neg.x_ne
α : 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
⊢ x ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
case neg
α : 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
⊢ nextOr (y :: z :: zs) x d = nextOr (y :: z :: zs) x d'
rw [nextOr, nextOr, IH]
case neg.x_ne
α : 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
⊢ x ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
case neg.x_mem
α : 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
⊢ x ∈ z :: zs

case neg.x_ne
α : 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
⊢ x ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
. simpa [h] using x_mem
no goals
case neg.x_ne
α : 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
⊢ x ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
. simpa using x_ne
no goals
case neg.x_mem
α : 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
⊢ x ∈ z :: zs
simpa [h] using x_mem
no goals
case neg.x_ne
α : 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
⊢ x ≠ getLast (z :: zs) (_ : z :: zs ≠ [])
simpa using x_ne