-- Mathlib/Data/List/Cycle.lean
theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ (hd :: tl).prev x h ∈ hd :: tl

Tactic:
induction' tl with hd' tl hl generalizing hd

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x hd : α
h : x ∈ [hd]
⊢ [hd].prev x h ∈ [hd]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
rw [prev, dif_neg hx]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.prev x h ∈ l

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].prev x h ∈ []

case cons
α : Type u_1
inst✝ : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ (hd :: tl).prev x h ∈ hd :: tl

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x hd : α
h : x ∈ [hd]
⊢ [hd].prev x h ∈ [hd]

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].prev x h ∈ []

Tactic:
simp at h

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
simp only [hx, prev_cons_cons_eq]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_of_mem _ (getLast_mem _)

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_of_mem _ (hl _ _)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_self _ _

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
by_cases hx : x = hd

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl

Tactic:
split_ifs with hm

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl

case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl