[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
⊢ nextOr (y :: xs) x d = nextOr xs x d
[PROOFSTEP]
cases' xs with z zs
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ nextOr [y] x d = nextOr [] x d
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ nextOr (y :: z :: zs) x d = nextOr (z :: zs) x d
[PROOFSTEP]
exact if_neg h
[GOAL]
α : 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'
[PROOFSTEP]
induction' xs with y ys IH
[GOAL]
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'
[PROOFSTEP]
cases x_mem
[GOAL]
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'
[PROOFSTEP]
cases' ys with z zs
[GOAL]
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'
[PROOFSTEP]
simp at x_mem x_ne 
[GOAL]
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'
[PROOFSTEP]
contradiction
[GOAL]
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'
[PROOFSTEP]
by_cases h : x = y
[GOAL]
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'
[PROOFSTEP]
rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
[GOAL]
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'
[PROOFSTEP]
rw [nextOr, nextOr, IH]
[GOAL]
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
[PROOFSTEP]
simpa [h] using x_mem
[GOAL]
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 ≠ [])
[PROOFSTEP]
simpa using x_ne
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : nextOr xs x d ≠ d
⊢ x ∈ xs
[PROOFSTEP]
induction' xs with y ys IH
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : nextOr xs x d ≠ d
h : nextOr [] x d ≠ d
⊢ x ∈ []
[PROOFSTEP]
simp at h 
[GOAL]
case cons
α : 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
⊢ x ∈ y :: ys
[PROOFSTEP]
cases' ys with z zs
[GOAL]
case cons.nil
α : 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
⊢ x ∈ [y]
[PROOFSTEP]
simp at h 
[GOAL]
case cons.cons
α : 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
⊢ x ∈ y :: z :: zs
[PROOFSTEP]
by_cases hx : x = y
[GOAL]
case pos
α : 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
⊢ x ∈ y :: z :: zs
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : 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
⊢ x ∈ y :: z :: zs
[PROOFSTEP]
rw [nextOr_cons_of_ne _ _ _ _ hx] at h 
[GOAL]
case neg
α : 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
⊢ x ∈ y :: z :: zs
[PROOFSTEP]
simpa [hx] using IH h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : ¬x ∈ xs
⊢ nextOr (xs ++ [x]) x d = d
[PROOFSTEP]
induction' xs with z zs IH
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
h : ¬x ∈ []
⊢ nextOr ([] ++ [x]) x d = d
[PROOFSTEP]
simp
[GOAL]
case cons
α : 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
⊢ nextOr (z :: zs ++ [x]) x d = d
[PROOFSTEP]
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
[GOAL]
case cons.intro
α : 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
⊢ nextOr (z :: zs ++ [x]) x d = d
[PROOFSTEP]
rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
hd : d ∈ xs
⊢ nextOr xs x d ∈ xs
[PROOFSTEP]
revert hd
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ d ∈ xs → nextOr xs x d ∈ xs
[PROOFSTEP]
suffices ∀ (xs' : List α) (_ : ∀ x ∈ xs, x ∈ xs') (_ : d ∈ xs'), nextOr xs x d ∈ xs' by exact this xs fun _ => id
[GOAL]
α : 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
[PROOFSTEP]
exact this xs fun _ => id
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ ∀ (xs' : List α), (∀ (x : α), x ∈ xs → x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs'
[PROOFSTEP]
intro xs' hxs' hd
[GOAL]
α : 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'
[PROOFSTEP]
induction' xs with y ys ih
[GOAL]
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'
[PROOFSTEP]
exact hd
[GOAL]
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'
[PROOFSTEP]
cases' ys with z zs
[GOAL]
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'
[PROOFSTEP]
exact hd
[GOAL]
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'
[PROOFSTEP]
rw [nextOr]
[GOAL]
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'
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : 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'
[PROOFSTEP]
exact hxs' _ (mem_cons_of_mem _ (mem_cons_self _ _))
[GOAL]
case neg
α : 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'
[PROOFSTEP]
exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : α
h : x✝ ∈ []
⊢ α
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
y z : α
xs : List α
x : α
h : x ∈ y :: z :: xs
hx : ¬x = y
⊢ x ∈ z :: xs
[PROOFSTEP]
simpa [hx] using h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ next (y :: z :: l) x h = z
[PROOFSTEP]
rw [next, nextOr, if_pos hx]
[GOAL]
α : 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 ∈ l
[PROOFSTEP]
simpa [hy] using h
[GOAL]
α : 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)
[PROOFSTEP]
rw [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_of_ne]
[GOAL]
case x_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 ∈ l
[PROOFSTEP]
rwa [getLast_cons] at hx 
[GOAL]
case x_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 ≠ [])
⊢ l ≠ []
[PROOFSTEP]
exact ne_nil_of_mem (by assumption)
[GOAL]
α : 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.65756 ∈ l
[PROOFSTEP]
assumption
[GOAL]
case x_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 ≠ [])
⊢ x ≠ getLast l (_ : l ≠ [])
[PROOFSTEP]
rwa [getLast_cons] at hx 
[GOAL]
α : 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
[PROOFSTEP]
rw [next, nextOr_concat]
[GOAL]
α : 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
[PROOFSTEP]
rfl
[GOAL]
case h
α : 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])
⊢ ¬x ∈ y :: l
[PROOFSTEP]
simp [hy, hx]
[GOAL]
α : 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 ≠ [])
hl : Nodup l
⊢ next (y :: l) x h = y
[PROOFSTEP]
rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]
[GOAL]
case h
α : 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 ≠ [])
hl : Nodup l
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
[PROOFSTEP]
subst hx
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
⊢ ¬getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
[PROOFSTEP]
intro H
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
⊢ False
[PROOFSTEP]
obtain ⟨⟨_ | k, hk⟩, hk'⟩ := get_of_mem H
[GOAL]
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.zero, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
[PROOFSTEP]
rw [← Option.some_inj] at hk' 
[GOAL]
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : some (get (dropLast (y :: l)) { val := Nat.zero, isLt := hk }) = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ False
[PROOFSTEP]
rw [← get?_eq_get, dropLast_eq_take, get?_take, get?_zero, head?_cons, Option.some_inj] at hk' 
[GOAL]
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : y = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
[PROOFSTEP]
exact hy (Eq.symm hk')
[GOAL]
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ Nat.zero < Nat.pred (length (y :: l))
[PROOFSTEP]
rw [Nat.zero_eq, length_cons, Nat.pred_succ]
[GOAL]
case h.intro.mk.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ 0 < length l
[PROOFSTEP]
exact length_pos_of_mem (by assumption)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
hk : Nat.zero < length (dropLast (y :: l))
hk' : get? (take (Nat.pred (length (y :: l))) (y :: l)) Nat.zero = some (getLast (y :: l) (_ : y :: l ≠ []))
⊢ ?m.71859 ∈ l
[PROOFSTEP]
assumption
[GOAL]
case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ False
[PROOFSTEP]
suffices k.succ = l.length by simp [this] at hk 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
this : Nat.succ k = length l
⊢ False
[PROOFSTEP]
simp [this] at hk 
[GOAL]
case h.intro.mk.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : Nodup l
h✝ : getLast (y :: l) (_ : y :: l ≠ []) ∈ l
h : getLast (y :: l) (_ : y :: l ≠ []) ∈ y :: l
hy : getLast (y :: l) (_ : y :: l ≠ []) ≠ y
H : getLast (y :: l) (_ : y :: l ≠ []) ∈ dropLast (y :: l)
k : ℕ
hk : Nat.succ k < length (dropLast (y :: l))
hk' : get (dropLast (y :: l)) { val := Nat.succ k, isLt := hk } = getLast (y :: l) (_ : y :: l ≠ [])
⊢ Nat.succ k = length l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case h.intro.mk.succ.nil
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hl : Nodup []
h✝ : getLast [y] (_ : [y] ≠ []) ∈ []
h : getLast [y] (_ : [y] ≠ []) ∈ [y]
hy : getLast [y] (_ : [y] ≠ []) ≠ y
H : getLast [y] (_ : [y] ≠ []) ∈ dropLast [y]
hk : Nat.succ k < length (dropLast [y])
hk' : get (dropLast [y]) { val := Nat.succ k, isLt := hk } = getLast [y] (_ : [y] ≠ [])
⊢ Nat.succ k = length []
[PROOFSTEP]
simp at hk 
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Nodup (hd :: tl)
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
[PROOFSTEP]
rw [nodup_iff_injective_get] at hl 
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k = length (hd :: tl)
[PROOFSTEP]
rw [length, Nat.succ_inj']
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ k = length tl
[PROOFSTEP]
refine' Fin.veq_of_eq (@hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩ ⟨tl.length, by simp⟩ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ Nat.succ k < length (hd :: tl)
[PROOFSTEP]
simpa using hk
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ length tl < length (hd :: tl)
[PROOFSTEP]
simp
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
[PROOFSTEP]
rw [← Option.some_inj] at hk' 
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  some (get (dropLast (y :: hd :: tl)) { val := Nat.succ k, isLt := hk }) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
[PROOFSTEP]
rw [← get?_eq_get, dropLast_eq_take, get?_take, get?, get?_eq_get, Option.some_inj] at hk' 
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' : get (hd :: tl) { val := k, isLt := ?h.intro.mk.succ.cons } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ k < length (hd :: tl)
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
[PROOFSTEP]
rw [hk']
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk'✝ : get? (hd :: tl) k = some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
hk' :
  get (hd :: tl) { val := k, isLt := (_ : k < length (hd :: tl)) } = getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ [])
⊢ getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) =
    get (hd :: tl) { val := length tl, isLt := (_ : length tl < Nat.succ (length tl)) }
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
[PROOFSTEP]
simp [getLast_eq_get]
[GOAL]
case h.intro.mk.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (get (hd :: tl))
h✝ : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ hd :: tl
h : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ y :: hd :: tl
hy : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ≠ y
H : getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []) ∈ dropLast (y :: hd :: tl)
hk : Nat.succ k < length (dropLast (y :: hd :: tl))
hk' :
  get? (take (Nat.pred (length (y :: hd :: tl))) (y :: hd :: tl)) (Nat.succ k) =
    some (getLast (y :: hd :: tl) (_ : y :: hd :: tl ≠ []))
⊢ Nat.succ k < Nat.pred (length (y :: hd :: tl))
[PROOFSTEP]
simpa using hk
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hxy : x ∈ y :: l
hx : x = y
⊢ prev (y :: l) x hxy = getLast (y :: l) (_ : y :: l ≠ [])
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
hxy : x ∈ [y]
⊢ prev [y] x hxy = getLast [y] (_ : [y] ≠ [])
[PROOFSTEP]
simp [prev, hx]
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
head✝ : α
tail✝ : List α
hxy : x ∈ y :: head✝ :: tail✝
⊢ prev (y :: head✝ :: tail✝) x hxy = getLast (y :: head✝ :: tail✝) (_ : y :: head✝ :: tail✝ ≠ [])
[PROOFSTEP]
simp [prev, hx]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ prev (y :: z :: l) x h = getLast (z :: l) (_ : z :: l ≠ [])
[PROOFSTEP]
rw [prev, dif_pos hx]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x = z
⊢ prev (y :: z :: l) x h = y
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
h : x ∈ [y, z]
⊢ prev [y, z] x h = y
[PROOFSTEP]
simp [prev, hy, hz]
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ prev (y :: z :: head✝ :: tail✝) x h = y
[PROOFSTEP]
rw [prev, dif_neg hy, if_pos hz]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x ∈ z :: l
[PROOFSTEP]
simpa [hy] using h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ prev (y :: z :: l) x h = prev (z :: l) x (_ : x ∈ z :: l)
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ prev [y, z] x h = prev [z] x (_ : x ∈ [z])
[PROOFSTEP]
simp [hy, hz] at h 
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ prev (y :: z :: head✝ :: tail✝) x h = prev (z :: head✝ :: tail✝) x (_ : x ∈ z :: head✝ :: tail✝)
[PROOFSTEP]
rw [prev, dif_neg hy, if_neg hz]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ prev l x h ∈ l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ prev [] x h ∈ []
[PROOFSTEP]
simp at h 
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ prev (hd :: tl) x h ∈ hd :: tl
[PROOFSTEP]
induction' tl with hd' tl hl generalizing hd
[GOAL]
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl : List α
h✝ : x ∈ hd✝ :: tl
hd : α
h : x ∈ [hd]
⊢ prev [hd] x h ∈ [hd]
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ prev (hd :: hd' :: tl) x h ∈ hd :: hd' :: tl
[PROOFSTEP]
by_cases hx : x = hd
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ prev (hd :: hd' :: tl) x h ∈ hd :: hd' :: tl
[PROOFSTEP]
simp only [hx, prev_cons_cons_eq]
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ getLast (hd' :: tl) (_ : hd' :: tl ≠ []) ∈ hd :: hd' :: tl
[PROOFSTEP]
exact mem_cons_of_mem _ (getLast_mem _)
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ prev (hd :: hd' :: tl) x h ∈ hd :: hd' :: tl
[PROOFSTEP]
rw [prev, dif_neg hx]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else prev (hd' :: tl) x (_ : x ∈ hd' :: tl)) ∈ hd :: hd' :: tl
[PROOFSTEP]
split_ifs with hm
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd✝ : α
tl✝ : List α
h✝ : x ∈ hd✝ :: tl✝
hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), prev (hd :: tl) x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : ¬x = hd'
⊢ prev (hd' :: tl) x (_ : x ∈ hd' :: tl) ∈ hd :: hd' :: tl
[PROOFSTEP]
exact mem_cons_of_mem _ (hl _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
x✝ : Nodup []
i : Fin (length [])
⊢ next [] (get [] i) (_ : get [] { val := ↑i, isLt := (_ : ↑i < length []) } ∈ []) =
    get [] { val := (↑i + 1) % length [], isLt := (_ : (↑i + 1) % length [] < length []) }
[PROOFSTEP]
simpa using i.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x head✝ : α
x✝¹ : Nodup [head✝]
x✝ : Fin (length [head✝])
⊢ next [head✝] (get [head✝] x✝) (_ : get [head✝] { val := ↑x✝, isLt := (_ : ↑x✝ < length [head✝]) } ∈ [head✝]) =
    get [head✝] { val := (↑x✝ + 1) % length [head✝], isLt := (_ : (↑x✝ + 1) % length [head✝] < length [head✝]) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
⊢ next (x :: y :: l) (get (x :: y :: l) { val := 0, isLt := h0 })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := 0, isLt := h0 }, isLt := (_ : ↑{ val := 0, isLt := h0 } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
have h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x := by simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
⊢ get (x :: y :: l) { val := 0, isLt := h0 } = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := 0, isLt := h0 })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := 0, isLt := h0 }, isLt := (_ : ↑{ val := 0, isLt := h0 } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
rw [next_cons_cons_eq' _ _ _ _ _ h₁]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
_h : Nodup (x :: y :: l)
h0 : 0 < length (x :: y :: l)
h₁ : get (x :: y :: l) { val := 0, isLt := h0 } = x
⊢ y =
    get (x :: y :: l)
      { val := (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := 0, isLt := h0 } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
have hx' : (x :: y :: l).get ⟨i + 1, hi⟩ ≠ x := by
  intro H
  suffices (i + 1 : ℕ) = 0 by simpa
  rw [nodup_iff_injective_get] at hn 
  refine' Fin.veq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ _)
  simpa using H
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
[PROOFSTEP]
intro H
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ False
[PROOFSTEP]
suffices (i + 1 : ℕ) = 0 by simpa
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
this : i + 1 = 0
⊢ False
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
[PROOFSTEP]
rw [nodup_iff_injective_get] at hn 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ i + 1 = 0
[PROOFSTEP]
refine' Fin.veq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ 0 < length (x :: y :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Function.Injective (get (x :: y :: l))
i : ℕ
hi : i + 1 < length (x :: y :: l)
H : get (x :: y :: l) { val := i + 1, isLt := hi } = x
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := 0, isLt := (_ : 0 < Nat.succ (length l + 1)) }
[PROOFSTEP]
simpa using H
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
have hi' : i ≤ l.length := Nat.le_of_lt_succ (Nat.succ_lt_succ_iff.1 hi)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi' : i ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
rcases hi'.eq_or_lt with (hi' | hi')
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i = length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
subst hi'
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := length l + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := length l + 1, isLt := hi },
              isLt := (_ : ↑{ val := length l + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
rw [next_getLast_cons]
[GOAL]
case inl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ x =
    get (x :: y :: l)
      { val := (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := length l + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
simp [hi', get]
[GOAL]
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
rw [get_cons_succ]
[GOAL]
case inl.h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (y :: l) { val := length l, isLt := (_ : length l < length (y :: l)) } ∈ y :: l
[PROOFSTEP]
exact get_mem _ _ _
[GOAL]
case inl.hy
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
[PROOFSTEP]
exact hx'
[GOAL]
case inl.hx
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ get (x :: y :: l) { val := length l + 1, isLt := hi } = getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
[PROOFSTEP]
simp [getLast_eq_get]
[GOAL]
case inl.hl
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
hi : length l + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := length l + 1, isLt := hi } ≠ x
hi' : length l ≤ length l
⊢ Nodup (y :: l)
[PROOFSTEP]
exact hn.of_cons
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (x :: y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ :
        get (x :: y :: l)
            { val := ↑{ val := i + 1, isLt := hi },
              isLt := (_ : ↑{ val := i + 1, isLt := hi } < length (x :: y :: l)) } ∈
          x :: y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
[PROOFSTEP]
rw [next_ne_head_ne_getLast _ _ _ _ _ hx']
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (x :: y :: l) { val := i + 1, isLt := hi })
      (_ : get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l) =
    get (x :: y :: l)
      { val := (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
simp only [get_cons_succ]
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ next (y :: l) (get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) })
      (_ : get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l) =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
rw [next_get (y :: l), ← get_cons_succ (a := x)]
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l)
      { val := (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1, isLt := ?m.114701 } =
    get (x :: y :: l)
      { val := (i + 1 + 1) % length (x :: y :: l),
        isLt := (_ : (↑{ val := i + 1, isLt := hi } + 1) % length (x :: y :: l) < length (x :: y :: l)) }
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
congr
[GOAL]
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 = (i + 1 + 1) % length (x :: y :: l)
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
dsimp
[GOAL]
case inr.e_a.e_val
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (i + 1) % Nat.succ (length l) + 1 = (i + 1 + 1) % Nat.succ (Nat.succ (length l))
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
rw [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'),
  Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 (Nat.succ_lt_succ_iff.2 hi'))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ (↑{ val := i, isLt := (_ : i < length (y :: l)) } + 1) % length (y :: l) + 1 < length (x :: y :: l)
[PROOFSTEP]
simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), Nat.succ_eq_add_one, hi']
[GOAL]
case inr._h
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ Nodup (y :: l)
[PROOFSTEP]
exact hn.of_cons
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠ getLast (x :: y :: l) (_ : x :: y :: l ≠ [])
[PROOFSTEP]
rw [getLast_eq_get]
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ≠
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
[PROOFSTEP]
intro h
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
[PROOFSTEP]
have := nodup_iff_injective_get.1 hn h
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this :
  { val := i + 1, isLt := hi } =
    { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
⊢ False
[PROOFSTEP]
simp at this 
[GOAL]
case inr
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
h :
  get (x :: y :: l) { val := i + 1, isLt := hi } =
    get (x :: y :: l) { val := length (x :: y :: l) - 1, isLt := (_ : length (x :: y :: l) - 1 < length (x :: y :: l)) }
this : i = length l
⊢ False
[PROOFSTEP]
simp [this] at hi' 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (x :: y :: l) { val := i + 1, isLt := hi } ∈ y :: l
[PROOFSTEP]
rw [get_cons_succ]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hn : Nodup (x :: y :: l)
i : ℕ
hi : i + 1 < length (x :: y :: l)
hx' : get (x :: y :: l) { val := i + 1, isLt := hi } ≠ x
hi'✝ : i ≤ length l
hi' : i < length l
⊢ get (y :: l) { val := i, isLt := (_ : i < length (y :: l)) } ∈ y :: l
[PROOFSTEP]
exact get_mem _ _ _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
⊢ prev l (nthLe l n hn) (_ : nthLe l n hn ∈ l) =
    nthLe l ((n + (length l - 1)) % length l) (_ : (n + (length l - 1)) % length l < length l)
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
⊢ prev [] (nthLe [] n hn) (_ : nthLe [] n hn ∈ []) =
    nthLe [] ((n + (length [] - 1)) % length []) (_ : (n + (length [] - 1)) % length [] < length [])
[PROOFSTEP]
simp at hn 
[GOAL]
case cons
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
n : ℕ
x : α
l : List α
h : Nodup (x :: l)
hn : n < length (x :: l)
⊢ prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
    nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
      (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
[PROOFSTEP]
induction' l with y l hl generalizing n x
[GOAL]
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l : List α
h✝ : Nodup (x✝ :: l)
hn✝ : n✝ < length (x✝ :: l)
n : ℕ
x : α
h : Nodup [x]
hn : n < length [x]
⊢ prev [x] (nthLe [x] n hn) (_ : nthLe [x] n hn ∈ [x]) =
    nthLe [x] ((n + (length [x] - 1)) % length [x]) (_ : (n + (length [x] - 1)) % length [x] < length [x])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
n : ℕ
x : α
h : Nodup (x :: y :: l)
hn : n < length (x :: y :: l)
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) n hn) (_ : nthLe (x :: y :: l) n hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((n + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (n + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
rcases n with (_ | _ | n)
[GOAL]
case cons.cons.zero
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
hn : Nat.zero < length (x :: y :: l)
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) Nat.zero hn) (_ : nthLe (x :: y :: l) Nat.zero hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
simp [Nat.add_succ_sub_one, add_zero, List.prev_cons_cons_eq, Nat.zero_eq, List.length, List.nthLe,
  Nat.succ_add_sub_one, zero_add, getLast_eq_get, Nat.mod_eq_of_lt (Nat.succ_lt_succ l.length.lt_succ_self)]
[GOAL]
case cons.cons.succ.zero
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
hn : Nat.succ Nat.zero < length (x :: y :: l)
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) (Nat.succ Nat.zero) hn)
      (_ : nthLe (x :: y :: l) (Nat.succ Nat.zero) hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
simp only [mem_cons, nodup_cons] at h 
[GOAL]
case cons.cons.succ.zero
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
hn : Nat.succ Nat.zero < length (x :: y :: l)
h : ¬(x = y ∨ x ∈ l) ∧ ¬y ∈ l ∧ Nodup l
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) (Nat.succ Nat.zero) hn)
      (_ : nthLe (x :: y :: l) (Nat.succ Nat.zero) hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
push_neg at h 
[GOAL]
case cons.cons.succ.zero
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
hn : Nat.succ Nat.zero < length (x :: y :: l)
h : (x ≠ y ∧ ¬x ∈ l) ∧ ¬y ∈ l ∧ Nodup l
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) (Nat.succ Nat.zero) hn)
      (_ : nthLe (x :: y :: l) (Nat.succ Nat.zero) hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ Nat.zero + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
simp only [List.prev_cons_cons_of_ne _ _ _ _ h.left.left.symm, Nat.zero_eq, List.length, List.nthLe, add_comm,
  eq_self_iff_true, Nat.succ_add_sub_one, Nat.mod_self, zero_add, List.get]
[GOAL]
case cons.cons.succ.succ
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ prev (x :: y :: l) (nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn)
      (_ : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn ∈ x :: y :: l) =
    nthLe (x :: y :: l) ((Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
rw [prev_ne_cons_cons]
[GOAL]
case cons.cons.succ.succ
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ prev (y :: l) (nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn)
      (_ : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn ∈ y :: l) =
    nthLe (x :: y :: l) ((Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
convert hl n.succ y h.of_cons (Nat.le_of_succ_le_succ hn) using 1
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ nthLe (x :: y :: l) ((Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (y :: l) ((Nat.succ n + (length (y :: l) - 1)) % length (y :: l))
      (_ : (Nat.succ n + (length (y :: l) - 1)) % length (y :: l) < length (y :: l))
[PROOFSTEP]
have : ∀ k hk, (y :: l).nthLe k hk = (x :: y :: l).nthLe (k + 1) (Nat.succ_lt_succ hk) :=
  by
  intros
  simp [List.nthLe]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
k✝ : ℕ
hk✝ : k✝ < length (y :: l)
⊢ nthLe (y :: l) k✝ hk✝ = nthLe (x :: y :: l) (k✝ + 1) (_ : Nat.succ k✝ < Nat.succ (length (y :: l)))
[PROOFSTEP]
simp [List.nthLe]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
⊢ nthLe (x :: y :: l) ((Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (y :: l) ((Nat.succ n + (length (y :: l) - 1)) % length (y :: l))
      (_ : (Nat.succ n + (length (y :: l) - 1)) % length (y :: l) < length (y :: l))
[PROOFSTEP]
rw [this]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
⊢ nthLe (x :: y :: l) ((Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l))
      (_ : (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) ((Nat.succ n + (length (y :: l) - 1)) % length (y :: l) + 1)
      (_ : Nat.succ ((Nat.succ n + (length (y :: l) - 1)) % length (y :: l)) < Nat.succ (length (y :: l)))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
⊢ (Nat.succ (Nat.succ n) + (length (x :: y :: l) - 1)) % length (x :: y :: l) =
    (Nat.succ n + (length (y :: l) - 1)) % length (y :: l) + 1
[PROOFSTEP]
simp only [Nat.add_succ_sub_one, add_zero, length]
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
⊢ (Nat.succ (Nat.succ n) + (length l + 1)) % (length l + 1 + 1) = (Nat.succ n + length l) % (length l + 1) + 1
[PROOFSTEP]
simp only [length, Nat.succ_lt_succ_iff] at hn 
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
hn : n < length l
⊢ (Nat.succ (Nat.succ n) + (length l + 1)) % (length l + 1 + 1) = (Nat.succ n + length l) % (length l + 1) + 1
[PROOFSTEP]
set k := l.length
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
k : ℕ := length l
hn : n < k
⊢ (Nat.succ (Nat.succ n) + (k + 1)) % (k + 1 + 1) = (Nat.succ n + k) % (k + 1) + 1
[PROOFSTEP]
rw [Nat.succ_add, ← Nat.add_succ, Nat.add_mod_right, Nat.succ_add, ← Nat.add_succ _ k, Nat.add_mod_right,
  Nat.mod_eq_of_lt, Nat.mod_eq_of_lt]
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
k : ℕ := length l
hn : n < k
⊢ n < Nat.succ k
[PROOFSTEP]
exact Nat.lt_succ_of_lt hn
[GOAL]
case h.e'_3.e_n
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
this :
  ∀ (k : ℕ) (hk : k < length (y :: l)),
    nthLe (y :: l) k hk = nthLe (x :: y :: l) (k + 1) (_ : Nat.succ k < Nat.succ (length (y :: l)))
k : ℕ := length l
hn : n < k
⊢ n + 1 < Nat.succ (k + 1)
[PROOFSTEP]
exact Nat.succ_lt_succ (Nat.lt_succ_of_lt hn)
[GOAL]
case cons.cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn ≠ x
[PROOFSTEP]
intro H
[GOAL]
case cons.cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = x
⊢ False
[PROOFSTEP]
suffices n.succ.succ = 0 by simpa
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = x
this : Nat.succ (Nat.succ n) = 0
⊢ False
[PROOFSTEP]
simpa
[GOAL]
case cons.cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = x
⊢ Nat.succ (Nat.succ n) = 0
[PROOFSTEP]
rw [nodup_iff_nthLe_inj] at h 
[GOAL]
case cons.cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (x :: y :: l)) (h₂ : j < length (x :: y :: l)),
    nthLe (x :: y :: l) i h₁ = nthLe (x :: y :: l) j h₂ → i = j
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = x
⊢ Nat.succ (Nat.succ n) = 0
[PROOFSTEP]
refine' h _ _ hn Nat.succ_pos' _
[GOAL]
case cons.cons.succ.succ.hy
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (x :: y :: l)) (h₂ : j < length (x :: y :: l)),
    nthLe (x :: y :: l) i h₁ = nthLe (x :: y :: l) j h₂ → i = j
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = x
⊢ nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = nthLe (x :: y :: l) 0 (_ : 0 < Nat.succ (length (y :: l)))
[PROOFSTEP]
simpa using H
[GOAL]
case cons.cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
⊢ nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn ≠ y
[PROOFSTEP]
intro H
[GOAL]
case cons.cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = y
⊢ False
[PROOFSTEP]
suffices n.succ.succ = 1 by simpa
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = y
this : Nat.succ (Nat.succ n) = 1
⊢ False
[PROOFSTEP]
simpa
[GOAL]
case cons.cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h : Nodup (x :: y :: l)
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = y
⊢ Nat.succ (Nat.succ n) = 1
[PROOFSTEP]
rw [nodup_iff_nthLe_inj] at h 
[GOAL]
case cons.cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (x :: y :: l)) (h₂ : j < length (x :: y :: l)),
    nthLe (x :: y :: l) i h₁ = nthLe (x :: y :: l) j h₂ → i = j
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = y
⊢ Nat.succ (Nat.succ n) = 1
[PROOFSTEP]
refine' h _ _ hn (Nat.succ_lt_succ Nat.succ_pos') _
[GOAL]
case cons.cons.succ.succ.hz
α : Type u_1
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ : α
n✝ : ℕ
x✝ : α
l✝ : List α
h✝ : Nodup (x✝ :: l✝)
hn✝ : n✝ < length (x✝ :: l✝)
y : α
l : List α
hl :
  ∀ (n : ℕ) (x : α),
    Nodup (x :: l) →
      ∀ (hn : n < length (x :: l)),
        prev (x :: l) (nthLe (x :: l) n hn) (_ : nthLe (x :: l) n hn ∈ x :: l) =
          nthLe (x :: l) ((n + (length (x :: l) - 1)) % length (x :: l))
            (_ : (n + (length (x :: l) - 1)) % length (x :: l) < length (x :: l))
x : α
h :
  ∀ (i j : ℕ) (h₁ : i < length (x :: y :: l)) (h₂ : j < length (x :: y :: l)),
    nthLe (x :: y :: l) i h₁ = nthLe (x :: y :: l) j h₂ → i = j
n : ℕ
hn : Nat.succ (Nat.succ n) < length (x :: y :: l)
H : nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = y
⊢ nthLe (x :: y :: l) (Nat.succ (Nat.succ n)) hn = nthLe (x :: y :: l) 1 (_ : Nat.succ 0 < Nat.succ (length (y :: l)))
[PROOFSTEP]
simpa using H
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l) = rotate l 1
[PROOFSTEP]
apply List.ext_nthLe
[GOAL]
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = length (rotate l 1)
[PROOFSTEP]
simp
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ ∀ (n : ℕ) (h₁ : n < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))) (h₂ : n < length (rotate l 1)),
    nthLe (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n h₁ = nthLe (rotate l 1) n h₂
[PROOFSTEP]
intros
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
n✝ : ℕ
h₁✝ : n✝ < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
h₂✝ : n✝ < length (rotate l 1)
⊢ nthLe (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n✝ h₁✝ = nthLe (rotate l 1) n✝ h₂✝
[PROOFSTEP]
rw [nthLe_pmap, nthLe_rotate, next_nthLe _ h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l) = rotate l (length l - 1)
[PROOFSTEP]
apply List.ext_nthLe
[GOAL]
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) = length (rotate l (length l - 1))
[PROOFSTEP]
simp
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
⊢ ∀ (n : ℕ) (h₁ : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
    (h₂ : n < length (rotate l (length l - 1))),
    nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n h₁ = nthLe (rotate l (length l - 1)) n h₂
[PROOFSTEP]
intro n hn hn'
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup l
n : ℕ
hn : n < length (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
hn' : n < length (rotate l (length l - 1))
⊢ nthLe (pmap (prev l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) n hn = nthLe (rotate l (length l - 1)) n hn'
[PROOFSTEP]
rw [nthLe_rotate, nthLe_pmap, prev_nthLe _ h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ prev l (next l x hx) (_ : next l x hx ∈ l) = x
[PROOFSTEP]
obtain ⟨n, hn, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ prev l (next l (nthLe l n hn) hx) (_ : next l (nthLe l n hn) hx ∈ l) = nthLe l n hn
[PROOFSTEP]
simp only [next_nthLe, prev_nthLe, h, Nat.mod_add_mod]
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1 + (length l - 1)) % length l) (_ : (n + 1 + (length l - 1)) % length l < length l) = nthLe l n hn
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
hx : nthLe [] n hn ∈ []
⊢ nthLe [] ((n + 1 + (length [] - 1)) % length []) (_ : (n + 1 + (length [] - 1)) % length [] < length []) =
    nthLe [] n hn
[PROOFSTEP]
simp at hx 
[GOAL]
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
[PROOFSTEP]
have : (n + 1 + length tl) % (length tl + 1) = n :=
  by
  rw [length_cons] at hn 
  rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ (n + 1 + length tl) % (length tl + 1) = n
[PROOFSTEP]
rw [length_cons] at hn 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn✝ : n < length (hd :: tl)
hn : n < Nat.succ (length tl)
hx : nthLe (hd :: tl) n hn✝ ∈ hd :: tl
⊢ (n + 1 + length tl) % (length tl + 1) = n
[PROOFSTEP]
rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
[GOAL]
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
this : (n + 1 + length tl) % (length tl + 1) = n
⊢ nthLe (hd :: tl) ((n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl))
      (_ : (n + 1 + (length (hd :: tl) - 1)) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
[PROOFSTEP]
simp only [length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.succ_eq_add_one, this]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ next l (prev l x hx) (_ : prev l x hx ∈ l) = x
[PROOFSTEP]
obtain ⟨n, hn, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ next l (prev l (nthLe l n hn) hx) (_ : prev l (nthLe l n hn) hx ∈ l) = nthLe l n hn
[PROOFSTEP]
simp only [next_nthLe, prev_nthLe, h, Nat.mod_add_mod]
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + (length l - 1) + 1) % length l) (_ : (n + (length l - 1) + 1) % length l < length l) = nthLe l n hn
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.intro.nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
hx : nthLe [] n hn ∈ []
⊢ nthLe [] ((n + (length [] - 1) + 1) % length []) (_ : (n + (length [] - 1) + 1) % length [] < length []) =
    nthLe [] n hn
[PROOFSTEP]
simp at hx 
[GOAL]
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ nthLe (hd :: tl) ((n + (length (hd :: tl) - 1) + 1) % length (hd :: tl))
      (_ : (n + (length (hd :: tl) - 1) + 1) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
[PROOFSTEP]
have : (n + length tl + 1) % (length tl + 1) = n :=
  by
  rw [length_cons] at hn 
  rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
⊢ (n + length tl + 1) % (length tl + 1) = n
[PROOFSTEP]
rw [length_cons] at hn 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn✝ : n < length (hd :: tl)
hn : n < Nat.succ (length tl)
hx : nthLe (hd :: tl) n hn✝ ∈ hd :: tl
⊢ (n + length tl + 1) % (length tl + 1) = n
[PROOFSTEP]
rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
[GOAL]
case intro.intro.cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
hd : α
tl : List α
h : Nodup (hd :: tl)
hn : n < length (hd :: tl)
hx : nthLe (hd :: tl) n hn ∈ hd :: tl
this : (n + length tl + 1) % (length tl + 1) = n
⊢ nthLe (hd :: tl) ((n + (length (hd :: tl) - 1) + 1) % length (hd :: tl))
      (_ : (n + (length (hd :: tl) - 1) + 1) % length (hd :: tl) < length (hd :: tl)) =
    nthLe (hd :: tl) n hn
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ prev (reverse l) x (_ : x ∈ reverse l) = next l x hx
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
[PROOFSTEP]
have lpos : 0 < l.length := k.zero_le.trans_lt hk
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
[PROOFSTEP]
have key : l.length - 1 - k < l.length := (Nat.sub_le _ _).trans_lt (tsub_lt_self lpos Nat.succ_pos')
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) = next l (nthLe l k hk) hx
[PROOFSTEP]
rw [← nthLe_pmap l.next (fun _ h => h) (by simpa using hk)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ k < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l))
[PROOFSTEP]
simpa using hk
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe l k hk) (_ : nthLe l k hk ∈ reverse l) =
    nthLe (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)) k
      (_ : k < length (pmap (next l) l (_ : ∀ (x : α), x ∈ l → x ∈ l)))
[PROOFSTEP]
simp_rw [← nthLe_reverse l k (key.trans_le (by simp)), pmap_next_eq_rotate_one _ h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l ≤ length (reverse l)
[PROOFSTEP]
simp
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ prev (reverse l) (nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)))
      (_ : nthLe (reverse l) (length l - 1 - k) (_ : length l - 1 - k < length (reverse l)) ∈ reverse l) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
[PROOFSTEP]
rw [← nthLe_pmap l.reverse.prev fun _ h => h]
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l)) (length l - 1 - k)
      ?intro.intro =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
[PROOFSTEP]
simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse, length_reverse,
  Nat.mod_eq_of_lt (tsub_lt_self lpos Nat.succ_pos'), tsub_tsub_cancel_of_le (Nat.succ_le_of_lt lpos)]
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (rotate l (Nat.succ 0))) (length l - 1 - k)
      (_ : length l - 1 - k < length (reverse (rotate l (Nat.succ 0)))) =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
[PROOFSTEP]
rw [← nthLe_reverse]
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ nthLe (reverse (reverse (rotate l (Nat.succ 0)))) (length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k))
      ?intro.intro.h1 =
    nthLe (rotate l 1) k (_ : k < length (rotate l 1))
[PROOFSTEP]
simp [tsub_tsub_cancel_of_le (Nat.le_pred_of_lt hk)]
[GOAL]
case intro.intro.h1
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length (reverse (rotate l (Nat.succ 0))) - 1 - (length l - 1 - k) < length (reverse (reverse (rotate l (Nat.succ 0))))
[PROOFSTEP]
simpa using (Nat.sub_le _ _).trans_lt (tsub_lt_self lpos Nat.succ_pos')
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
lpos : 0 < length l
key : length l - 1 - k < length l
⊢ length l - 1 - k < length (pmap (prev (reverse l)) (reverse l) (_ : ∀ (x : α), x ∈ reverse l → x ∈ reverse l))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ next (reverse l) x (_ : x ∈ reverse l) = prev l x hx
[PROOFSTEP]
convert (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm
[GOAL]
case h.e'_3.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ l = reverse (reverse l)
[PROOFSTEP]
exact (reverse_reverse l).symm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ next l x hx = next l' x (_ : x ∈ l')
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
h : l ~r l'
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ next l (nthLe l k hk) hx = next l' (nthLe l k hk) (_ : nthLe l k hk ∈ l')
[PROOFSTEP]
obtain ⟨n, rfl⟩ := id h
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ next l (nthLe l k hk) hx = next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
[PROOFSTEP]
rw [next_nthLe _ hn]
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n) (nthLe l k hk) (_ : nthLe l k hk ∈ rotate l n)
[PROOFSTEP]
simp_rw [← nthLe_rotate' _ n k]
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe l ((k + 1) % length l) (_ : (k + 1) % length l < length l) =
    next (rotate l n)
      (nthLe (rotate l n) ((length l - n % length l + k) % length l)
        (_ : (length l - n % length l + k) % length l < length (rotate l n)))
      (_ :
        nthLe (rotate l n) ((length l - n % length l + k) % length l)
            (_ : (length l - n % length l + k) % length l < length (rotate l n)) ∈
          rotate l n)
[PROOFSTEP]
rw [next_nthLe _ (h.nodup_iff.mp hn), ← nthLe_rotate' _ n]
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hn : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n : ℕ
h : l ~r rotate l n
⊢ nthLe (rotate l n) ((length l - n % length l + (k + 1) % length l) % length l)
      (_ : (length l - n % length l + (k + 1) % length l) % length l < length (rotate l n)) =
    nthLe (rotate l n) (((length l - n % length l + k) % length l + 1) % length (rotate l n))
      (_ : ((length l - n % length l + k) % length l + 1) % length (rotate l n) < length (rotate l n))
[PROOFSTEP]
simp [add_assoc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ prev l x hx = prev l' x (_ : x ∈ l')
[PROOFSTEP]
rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l l' : List α
h : l ~r l'
hn : Nodup l
x : α
hx : x ∈ l
⊢ next (reverse l) x (_ : x ∈ reverse l) = next (reverse l') x (_ : x ∈ reverse l')
[PROOFSTEP]
exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _
[GOAL]
α : Type u_1
l : List α
a : α
⊢ rotate (a :: l) 1 = l ++ [a]
[PROOFSTEP]
rw [rotate_cons_succ, rotate_zero]
[GOAL]
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C (Quotient.mk'' l)
[PROOFSTEP]
refine List.recOn l ?_ ?_
[GOAL]
case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C (Quotient.mk'' [])
[PROOFSTEP]
simp
[GOAL]
case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C (Quotient.mk'' tail) → C (Quotient.mk'' (head :: tail))
[PROOFSTEP]
simp
[GOAL]
case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C nil
case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C ↑tail → C ↑(head :: tail)
[PROOFSTEP]
assumption'
[GOAL]
α : Type u_1
s : Cycle α
x✝ : List α
⊢ reverse (reverse (Quot.mk Setoid.r x✝)) = Quot.mk Setoid.r x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s : Cycle α
⊢ Subsingleton (reverse s) ↔ Subsingleton s
[PROOFSTEP]
simp [length_subsingleton_iff]
[GOAL]
α : Type u_1
s : Cycle α
h : Subsingleton s
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
[PROOFSTEP]
induction' s using Quot.inductionOn with l
[GOAL]
case h
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
l : List α
h : Subsingleton (Quot.mk Setoid.r l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r l → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r l → x = y
[PROOFSTEP]
simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff, length_eq_zero,
  length_eq_one, Nat.not_lt_zero, false_or_iff] at h 
[GOAL]
case h
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
l : List α
h : l = [] ∨ ∃ a, l = [a]
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r l → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r l → x = y
[PROOFSTEP]
rcases h with (rfl | ⟨z, rfl⟩)
[GOAL]
case h.inl
α : Type u_1
s : Cycle α
h : Subsingleton s
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r [] → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r [] → x = y
[PROOFSTEP]
simp
[GOAL]
case h.inr.intro
α : Type u_1
s : Cycle α
h : Subsingleton s
z : α
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r [z] → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r [z] → x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
hl : Nodup l
⊢ Nontrivial ↑l ↔ 2 ≤ List.length l
[PROOFSTEP]
rw [Nontrivial]
[GOAL]
α : Type u_1
l : List α
hl : Nodup l
⊢ (∃ x y _h, x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ List.length l
[PROOFSTEP]
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
[GOAL]
case nil
α : Type u_1
hl : Nodup []
⊢ (∃ x y _h, x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ List.length []
[PROOFSTEP]
simp
[GOAL]
case cons.nil
α : Type u_1
hd : α
hl : Nodup [hd]
⊢ (∃ x y _h, x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ List.length [hd]
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ (∃ x y _h, x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ List.length (hd :: hd' :: tl)
[PROOFSTEP]
simp only [mem_cons, exists_prop, mem_coe_iff, List.length, Ne.def, Nat.succ_le_succ_iff, zero_le, iff_true_iff]
[GOAL]
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
[PROOFSTEP]
refine' ⟨hd, hd', _, by simp⟩
[GOAL]
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ¬hd = hd'
[PROOFSTEP]
simp only [not_or, mem_cons, nodup_cons] at hl 
[GOAL]
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ ¬hd ∈ tl) ∧ ¬hd' ∈ tl ∧ Nodup tl
⊢ ¬hd = hd'
[PROOFSTEP]
exact hl.left.left
[GOAL]
α : Type u_1
s : Cycle α
⊢ Nontrivial (reverse s) ↔ Nontrivial s
[PROOFSTEP]
simp [Nontrivial]
[GOAL]
α : Type u_1
s : Cycle α
h : Nontrivial s
⊢ 2 ≤ length s
[PROOFSTEP]
obtain ⟨x, y, hxy, hx, hy⟩ := h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ length s
[PROOFSTEP]
induction' s using Quot.inductionOn with l
[GOAL]
case intro.intro.intro.intro.h
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
hy : y ∈ Quot.mk Setoid.r l
⊢ 2 ≤ length (Quot.mk Setoid.r l)
[PROOFSTEP]
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
[GOAL]
case intro.intro.intro.intro.h.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hx : x ∈ Quot.mk Setoid.r []
hy : y ∈ Quot.mk Setoid.r []
⊢ 2 ≤ length (Quot.mk Setoid.r [])
[PROOFSTEP]
simp at hx 
[GOAL]
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x ∈ Quot.mk Setoid.r [hd]
hy : y ∈ Quot.mk Setoid.r [hd]
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])
[PROOFSTEP]
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy 
[GOAL]
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk Setoid.r [hd])
[PROOFSTEP]
simp [hx, hy] at hxy 
[GOAL]
case intro.intro.intro.intro.h.cons.cons
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx✝ : x ∈ s
hy✝ : y ∈ s
hd hd' : α
tl : List α
hx : x ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
hy : y ∈ Quot.mk Setoid.r (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk Setoid.r (hd :: hd' :: tl))
[PROOFSTEP]
simp [Nat.succ_le_succ_iff]
[GOAL]
α : Type u_1
s : Cycle α
h : Subsingleton s
⊢ Nodup s
[PROOFSTEP]
induction' s using Quot.inductionOn with l
[GOAL]
case h
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
l : List α
h : Subsingleton (Quot.mk Setoid.r l)
⊢ Nodup (Quot.mk Setoid.r l)
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case h.nil
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
h : Subsingleton (Quot.mk Setoid.r [])
⊢ Nodup (Quot.mk Setoid.r [])
[PROOFSTEP]
simp
[GOAL]
case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
[PROOFSTEP]
have : tl = [] := by simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h
[GOAL]
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
⊢ tl = []
[PROOFSTEP]
simpa [Subsingleton, length_eq_zero, Nat.succ_le_succ_iff] using h
[GOAL]
case h.cons
α : Type u_1
s : Cycle α
h✝ : Subsingleton s
hd : α
tl : List α
h : Subsingleton (Quot.mk Setoid.r (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk Setoid.r (hd :: tl))
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
s : Cycle α
h : Nodup s
⊢ Nontrivial s ↔ ¬Subsingleton s
[PROOFSTEP]
rw [length_subsingleton_iff]
[GOAL]
α : Type u_1
s : Cycle α
h : Nodup s
⊢ Nontrivial s ↔ ¬length s ≤ 1
[PROOFSTEP]
induction s using Quotient.inductionOn'
[GOAL]
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
[PROOFSTEP]
simp only [mk''_eq_coe, nodup_coe_iff] at h 
[GOAL]
case h
α : Type u_1
a✝ : List α
h : List.Nodup a✝
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
[PROOFSTEP]
simp [h, Nat.succ_le_iff]
[GOAL]
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), ↑Multiset.card (toMultiset (Quotient.mk'' a)) = length (Quotient.mk'' a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α), b ∈ map f (Quotient.mk'' a) ↔ ∃ a_1, a_1 ∈ Quotient.mk'' a ∧ f a_1 = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
⊢ (fun l => ↑(cyclicPermutations l)) l₁ = (fun l => ↑(cyclicPermutations l)) l₂
[PROOFSTEP]
simpa using h.cyclicPermutations.perm
[GOAL]
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l
[PROOFSTEP]
rw [lists, Quotient.liftOn'_mk'']
[GOAL]
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑(cyclicPermutations l) ↔ ↑l✝ = Quotient.mk'' l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
⊢ lists nil = ↑[[]]
[PROOFSTEP]
rw [nil, lists_coe, cyclicPermutations_nil]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
⊢ ¬Nontrivial ↑[]
[PROOFSTEP]
simp [Nontrivial]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ ¬Nontrivial ↑[x]
[PROOFSTEP]
simp [Nontrivial]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x = y
⊢ Nontrivial ↑(x :: y :: l) ↔ Nontrivial ↑(x :: l)
[PROOFSTEP]
simp [h, Nontrivial]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ x ∈ ↑(x :: y :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ y ∈ ↑(x :: y :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : { l // List.Nodup l }
⊢ Nodup ↑↑l
[PROOFSTEP]
simpa using l.prop
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // Nodup s }
s : Cycle α
hs : Nodup s
⊢ ∃ a, (fun l => { val := ↑↑l, property := (_ : Nodup ↑↑l) }) a = { val := s, property := hs }
[PROOFSTEP]
induction' s using Quotient.inductionOn' with s hs
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // Nodup s }
s✝ : Cycle α
hs✝ : Nodup s✝
s : List α
hs : Nodup (Quotient.mk'' s)
⊢ ∃ a, (fun l => { val := ↑↑l, property := (_ : Nodup ↑↑l) }) a = { val := Quotient.mk'' s, property := hs }
[PROOFSTEP]
exact ⟨⟨s, hs⟩, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // Nodup s }
s✝ : Cycle α
hs✝ : Nodup s✝
s : List α
hs : Nodup (Quotient.mk'' s)
⊢ (fun l => { val := ↑↑l, property := (_ : Nodup ↑↑l) }) { val := s, property := hs } =
    { val := Quotient.mk'' s, property := hs }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Cycle α),
    x ∈ Finset.filter Nontrivial (Finset.map (Function.Embedding.subtype fun s => Nodup s) Finset.univ) ↔
      Nodup x ∧ Nontrivial x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
⊢ x ∈ Quot.mk Setoid.r l₁ ↔ y ∈ Quot.mk Setoid.r l₂
[PROOFSTEP]
rw [eq_of_heq hxy]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
⊢ y ∈ Quot.mk Setoid.r l₁ ↔ y ∈ Quot.mk Setoid.r l₂
[PROOFSTEP]
simpa [eq_of_heq hxy] using h.mem_iff
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
hm : x ∈ Quot.mk Setoid.r l₁
hm' : y ∈ Quot.mk Setoid.r l₂
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.next l x hx) l₁ h₁ x hm = (fun l _hn x hx => List.next l x hx) l₂ h₂ y hm'
[PROOFSTEP]
rw [heq_iff_eq] at hxy 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk Setoid.r l₁
hm' : y ∈ Quot.mk Setoid.r l₂
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.next l x hx) l₁ h₁ x hm = (fun l _hn x hx => List.next l x hx) l₂ h₂ y hm'
[PROOFSTEP]
subst x
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
y : α
hm' : y ∈ Quot.mk Setoid.r l₂
hm : y ∈ Quot.mk Setoid.r l₁
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.next l x hx) l₁ h₁ y hm = (fun l _hn x hx => List.next l x hx) l₂ h₂ y hm'
[PROOFSTEP]
simpa using isRotated_next_eq h h₁ _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
⊢ x ∈ Quot.mk Setoid.r l₁ ↔ y ∈ Quot.mk Setoid.r l₂
[PROOFSTEP]
rw [eq_of_heq hxy]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
⊢ y ∈ Quot.mk Setoid.r l₁ ↔ y ∈ Quot.mk Setoid.r l₂
[PROOFSTEP]
simpa [eq_of_heq hxy] using h.mem_iff
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : HEq x y
hm : x ∈ Quot.mk Setoid.r l₁
hm' : y ∈ Quot.mk Setoid.r l₂
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.prev l x hx) l₁ h₁ x hm = (fun l _hn x hx => List.prev l x hx) l₂ h₂ y hm'
[PROOFSTEP]
rw [heq_iff_eq] at hxy 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk Setoid.r l₁
hm' : y ∈ Quot.mk Setoid.r l₂
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.prev l x hx) l₁ h₁ x hm = (fun l _hn x hx => List.prev l x hx) l₂ h₂ y hm'
[PROOFSTEP]
subst x
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : Setoid.r l₁ l₂
h₁ : Nodup (Quot.mk Setoid.r l₁)
h₂ : Nodup (Quot.mk Setoid.r l₂)
_he : HEq h₁ h₂
y : α
hm' : y ∈ Quot.mk Setoid.r l₂
hm : y ∈ Quot.mk Setoid.r l₁
he' : HEq hm hm'
⊢ (fun l _hn x hx => List.prev l x hx) l₁ h₁ y hm = (fun l _hn x hx => List.prev l x hx) l₂ h₂ y hm'
[PROOFSTEP]
simpa using isRotated_prev_eq h h₁ _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next (reverse s) (_ : Nodup (reverse s)) x (_ : x ∈ reverse s) = prev s hs x hx
[PROOFSTEP]
simp [← prev_reverse_eq_next]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup (reverse s)
x : α
hx : x ∈ reverse s
⊢ next (reverse s) hs x hx = prev s (_ : Nodup s) x (_ : x ∈ s)
[PROOFSTEP]
simp [← prev_reverse_eq_next]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next s hs x hx ∈ s
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ next (Quot.mk Setoid.r a✝) hs x hx ∈ Quot.mk Setoid.r a✝
[PROOFSTEP]
apply next_mem
[GOAL]
case h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk Setoid.r a✝)
hx : x ∈ Quot.mk Setoid.r a✝
⊢ x ∈ a✝
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ prev s hs x hx ∈ s
[PROOFSTEP]
rw [← next_reverse_eq_prev, ← mem_reverse_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : Nodup s
x : α
hx : x ∈ s
⊢ next (reverse s) (_ : Nodup (reverse s)) x (_ : x ∈ reverse s) ∈ reverse s
[PROOFSTEP]
apply next_mem
[GOAL]
α : Type u_1
r : α → α → Prop
c : Cycle α
a b : List α
hab : Setoid.r a b
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      a ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      b
[PROOFSTEP]
cases' a with a l
[GOAL]
case nil
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
hab : Setoid.r [] b
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      [] ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      b
[PROOFSTEP]
cases' b with b m
[GOAL]
case cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : Setoid.r (a :: l) b
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (a :: l) ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      b
[PROOFSTEP]
cases' b with b m
[GOAL]
case nil.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
hab : Setoid.r [] []
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      [] ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      []
[PROOFSTEP]
rfl
[GOAL]
case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : Setoid.r [] (b :: m)
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      [] ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (b :: m)
[PROOFSTEP]
have := isRotated_nil_iff'.1 hab
[GOAL]
case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : Setoid.r [] (b :: m)
this : [] = b :: m
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      [] ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (b :: m)
[PROOFSTEP]
contradiction
[GOAL]
case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : Setoid.r (a :: l) []
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (a :: l) ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      []
[PROOFSTEP]
have := isRotated_nil_iff.1 hab
[GOAL]
case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : Setoid.r (a :: l) []
this : a :: l = []
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (a :: l) ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      []
[PROOFSTEP]
contradiction
[GOAL]
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : Setoid.r (a :: l) (b :: m)
⊢ (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (a :: l) ↔
    (fun l =>
        match l with
        | [] => True
        | a :: m => List.Chain r a (m ++ [a]))
      (b :: m)
[PROOFSTEP]
dsimp only
[GOAL]
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : Setoid.r (a :: l) (b :: m)
⊢ List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
cases' hab with n hn
[GOAL]
case cons.cons.intro
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
n : ℕ
hn : rotate (a :: l) n = b :: m
⊢ List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
induction' n with d hd generalizing a b l m
[GOAL]
case cons.cons.intro.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a✝ : α
l✝ : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l✝) n = b✝ :: m✝
a : α
l : List α
b : α
m : List α
hn : rotate (a :: l) Nat.zero = b :: m
⊢ List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
simp only [Nat.zero_eq, rotate_zero, cons.injEq] at hn 
[GOAL]
case cons.cons.intro.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a✝ : α
l✝ : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l✝) n = b✝ :: m✝
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
⊢ List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
rw [hn.1, hn.2]
[GOAL]
case cons.cons.intro.succ
α : Type u_1
r : α → α → Prop
c : Cycle α
a✝ : α
l✝ : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l✝) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a : α
l : List α
b : α
m : List α
hn : rotate (a :: l) (Nat.succ d) = b :: m
⊢ List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
cases' l with c s
[GOAL]
case cons.cons.intro.succ.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a✝ : α
l : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a b : α
m : List α
hn : rotate [a] (Nat.succ d) = b :: m
⊢ List.Chain r a ([] ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn 
[GOAL]
case cons.cons.intro.succ.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a✝ : α
l : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a b : α
m : List α
hn : a = b ∧ [] = m
⊢ List.Chain r a ([] ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
rw [hn.1, hn.2]
[GOAL]
case cons.cons.intro.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
a✝ : α
l : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : rotate (a :: c :: s) (Nat.succ d) = b :: m
⊢ List.Chain r a (c :: s ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
rw [Nat.succ_eq_one_add, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn 
[GOAL]
case cons.cons.intro.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
a✝ : α
l : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : rotate (c :: (s ++ [a])) d = b :: m
⊢ List.Chain r a (c :: s ++ [a]) ↔ List.Chain r b (m ++ [b])
[PROOFSTEP]
rw [← hd c _ _ _ hn]
[GOAL]
case cons.cons.intro.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
a✝ : α
l : List α
b✝ : α
m✝ : List α
n : ℕ
hn✝ : rotate (a✝ :: l) n = b✝ :: m✝
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    rotate (a :: l) d = b :: m → (List.Chain r a (l ++ [a]) ↔ List.Chain r b (m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : rotate (c :: (s ++ [a])) d = b :: m
⊢ List.Chain r a (c :: s ++ [a]) ↔ List.Chain r c (s ++ [a] ++ [c])
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil
[PROOFSTEP]
trivial
[GOAL]
α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a
[PROOFSTEP]
rw [chain_coe_cons, nil_append, List.chain_singleton]
[GOAL]
α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (hl : l ≠ []), Chain r ↑l ↔ List.Chain r (getLast l hl) l) →
      ∀ (hl : l ++ [a] ≠ []), Chain r ↑(l ++ [a]) ↔ List.Chain r (getLast (l ++ [a]) hl) (l ++ [a])
[PROOFSTEP]
intro m a _H _
[GOAL]
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ List.Chain r (getLast m hl) m
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ List.Chain r (getLast (m ++ [a]) hl✝) (m ++ [a])
[PROOFSTEP]
rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f (Quotient.mk'' l)) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' l)
[PROOFSTEP]
cases' l with a l
[GOAL]
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f (Quotient.mk'' [])) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' [])
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
[PROOFSTEP]
dsimp only [Chain, ← mk''_eq_coe, Quotient.liftOn'_mk'', Cycle.map, Quotient.map', Quot.map, Quotient.mk'',
  Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map]
[GOAL]
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain r (f a) (List.map f l ++ [f a]) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
[PROOFSTEP]
rw [← concat_eq_append, ← List.map_concat, List.chain_map f]
[GOAL]
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain (fun a b => r (f a) (f b)) a (concat l a) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range (Nat.succ n)) ↔ r n 0 ∧ ∀ (m : ℕ), m < n → r m (Nat.succ m)
[PROOFSTEP]
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, chain_range_succ]
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s
[PROOFSTEP]
induction s using Cycle.induction_on
[GOAL]
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil
[PROOFSTEP]
triv
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)
[PROOFSTEP]
rw [chain_coe_cons] at p ⊢
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : List.Chain r₁ a✝¹ (l✝ ++ [a✝¹])
⊢ List.Chain r₂ a✝¹ (l✝ ++ [a✝¹])
[PROOFSTEP]
exact p.imp H
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b) → Chain r s
[PROOFSTEP]
induction' s using Cycle.induction_on with a l _
[GOAL]
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), a ∈ nil → ∀ (b : α), b ∈ nil → r a b) → Chain r nil
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
[PROOFSTEP]
exact fun _ => Cycle.Chain.nil r
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
[PROOFSTEP]
intro hs
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
⊢ Chain r ↑(a :: l)
[PROOFSTEP]
have Ha : a ∈ (a :: l : Cycle α) := by simp
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
⊢ a ∈ ↑(a :: l)
[PROOFSTEP]
simp
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
[PROOFSTEP]
have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ b ∈ ↑(a :: l)
[PROOFSTEP]
simp [hb]
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
[PROOFSTEP]
rw [Cycle.chain_coe_cons]
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Chain r a (l ++ [a])
[PROOFSTEP]
apply Pairwise.chain
[GOAL]
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))
[PROOFSTEP]
rw [pairwise_cons]
[GOAL]
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ (a' : α), a' ∈ l ++ [a] → r a a') ∧ List.Pairwise r (l ++ [a])
[PROOFSTEP]
refine'
  ⟨fun b hb => _,
    pairwise_append.2
      ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc), pairwise_singleton r a, fun b hb c hc => _⟩⟩
[GOAL]
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ++ [a]
⊢ r a b
[PROOFSTEP]
rw [mem_append] at hb 
[GOAL]
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ∨ b ∈ [a]
⊢ r a b
[PROOFSTEP]
cases' hb with hb hb
[GOAL]
case HI.p.refine'_1.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ r a b
[PROOFSTEP]
exact hs a Ha b (Hl hb)
[GOAL]
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ [a]
⊢ r a b
[PROOFSTEP]
rw [mem_singleton] at hb 
[GOAL]
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a b
[PROOFSTEP]
rw [hb]
[GOAL]
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a a
[PROOFSTEP]
exact hs a Ha a Ha
[GOAL]
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c
[PROOFSTEP]
rw [mem_singleton] at hc 
[GOAL]
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b c
[PROOFSTEP]
rw [hc]
[GOAL]
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b a
[PROOFSTEP]
exact hs b (Hl hb) a Ha
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b
[PROOFSTEP]
induction' s using Cycle.induction_on with a l _
[GOAL]
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r nil → ∀ (a : α), a ∈ nil → ∀ (b : α), b ∈ nil → r a b
[PROOFSTEP]
exact fun _ b hb => (not_mem_nil _ hb).elim
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
⊢ Chain r ↑(a :: l) → ∀ (a_2 : α), a_2 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_2 b
[PROOFSTEP]
intro hs b hb c hc
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
[PROOFSTEP]
rw [Cycle.chain_coe_cons, List.chain_iff_pairwise] at hs 
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
[PROOFSTEP]
simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil, IsEmpty.forall_iff,
  imp_true_iff, Pairwise.nil, forall_eq, true_and_iff] at hs 
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ (a_1 : α), a_1 ∈ l → r a_1 a
⊢ r b c
[PROOFSTEP]
simp only [mem_coe_iff, mem_cons] at hb hc 
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ (a_1 : α), a_1 ∈ l → r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
⊢ r b c
[PROOFSTEP]
rcases hb with (rfl | hb)
[GOAL]
case HI.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ (a : α), a ∈ l → r a b
hc : c = b ∨ c ∈ l
⊢ r b c
[PROOFSTEP]
rcases hc with (rfl | hc)
[GOAL]
case HI.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ (a_1 : α), a_1 ∈ l → r a_1 a
hc : c = a ∨ c ∈ l
hb : b ∈ l
⊢ r b c
[PROOFSTEP]
rcases hc with (rfl | hc)
[GOAL]
case HI.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ (a : α), a ∈ l → r a c
⊢ r c c
[PROOFSTEP]
exact hs.1 c (Or.inr rfl)
[GOAL]
case HI.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ (a : α), a ∈ l → r a b
hc : c ∈ l
⊢ r b c
[PROOFSTEP]
exact hs.1 c (Or.inl hc)
[GOAL]
case HI.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ (a : α), a ∈ l → r a c
⊢ r b c
[PROOFSTEP]
exact hs.2.2 b hb
[GOAL]
case HI.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ (a_1 : α), a_1 ∈ l → r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c
[PROOFSTEP]
exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h : Chain r s
⊢ s = Cycle.nil
[PROOFSTEP]
induction' s using Cycle.induction_on with a l _ h
[GOAL]
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h✝ : Chain r s
h : Chain r Cycle.nil
⊢ Cycle.nil = Cycle.nil
[PROOFSTEP]
rfl
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h✝ : Chain r s
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
⊢ ↑(a :: l) = Cycle.nil
[PROOFSTEP]
have ha := mem_cons_self a l
[GOAL]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
h✝ : Chain r s
a : α
l : List α
a✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
ha : a ∈ a :: l
⊢ ↑(a :: l) = Cycle.nil
[PROOFSTEP]
exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
[PROOFSTEP]
rw [chain_iff_pairwise] at hs 
[GOAL]
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : IsAntisymm α r
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
[PROOFSTEP]
exact antisymm (hs a ha b hb) (hs b hb a ha)
