α : 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 ∈ xs
revert hd
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ ∀ (xs' : List α), (∀ (x : α), x ∈ xs → x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs'
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ d ∈ xs → nextOr xs x d ∈ xs
suffices ∀ (xs' : List α) (_ : ∀ x ∈ xs, x ∈ xs') (_ : d ∈ xs'), nextOr xs x d ∈ xs' by
  exact this xs fun _ => id
α : 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 : α
⊢ ∀ (xs' : List α), (∀ (x : α), x ∈ xs → x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs'
intro xs' hxs' hd
case nil
α : 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'
⊢ nextOr [] x d ∈ xs'

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

case cons.cons
α : 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'
⊢ nextOr (y :: z :: zs) x d ∈ xs'
case cons
α : 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'
⊢ nextOr (y :: ys) x d ∈ xs'
cases' ys with z zs
case cons.cons
α : 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'
⊢ (if x = y then z else nextOr (z :: zs) x d) ∈ xs'
case cons.cons
α : 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'
⊢ nextOr (y :: z :: zs) x d ∈ xs'
rw [nextOr]
case cons.cons.inl
α : 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
⊢ z ∈ xs'

case cons.cons.inr
α : 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
⊢ nextOr (z :: zs) x d ∈ xs'
case cons.cons
α : 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'
⊢ (if x = y then z else nextOr (z :: zs) x d) ∈ xs'
split_ifs with h
no goals
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
this : ∀ (xs' : List α), (∀ (x : α), x ∈ xs → x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs'
⊢ d ∈ xs → nextOr xs x d ∈ xs
exact this xs fun _ => id
no goals
case nil
α : 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'
⊢ nextOr [] x d ∈ xs'
exact hd
no goals
case cons.nil
α : 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'
⊢ nextOr [y] x d ∈ xs'
exact hd
no goals
case cons.cons.inl
α : 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
⊢ z ∈ xs'
exact hxs' _ (mem_cons_of_mem _ (mem_cons_self _ _))
no goals
case cons.cons.inr
α : 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
⊢ nextOr (z :: zs) x d ∈ xs'
exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)