-- Mathlib/Data/List/Cycle.lean
theorem nextOr_eq_nextOr_of_mem_of_ne (xs : List α) (x d d' : α) (x_mem : x ∈ xs)
    (x_ne : x ≠ xs.getLast (ne_nil_of_mem x_mem)) : nextOr xs x d = nextOr xs x d'

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [nextOr, nextOr, IH]

Result:
case neg.x_mem
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ x ∈ z :: zs

case neg.x_ne
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ x ≠ (z :: zs).getLast ⋯

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs
x_ne : x ≠ xs.getLast ⋯
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
induction' xs with y ys IH

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d d' : α
x_mem : x ∈ []
x_ne : x ≠ [].getLast ⋯
⊢ [].nextOr x d = [].nextOr x d'

case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : ∀ (x_mem : x ∈ ys), x ≠ ys.getLast ⋯ → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ y :: ys
x_ne : x ≠ (y :: ys).getLast ⋯
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Proof state:
case neg.x_mem
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ x ∈ z :: zs

Tactic:
simpa [h] using x_mem

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : ∀ (x_mem : x ∈ ys), x ≠ ys.getLast ⋯ → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ y :: ys
x_ne : x ≠ (y :: ys).getLast ⋯
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Tactic:
rcases ys with - | ⟨z, zs⟩

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : ∀ (x_mem : x ∈ []), x ≠ [].getLast ⋯ → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y]
x_ne : x ≠ [y].getLast ⋯
⊢ [y].nextOr x d = [y].nextOr x d'

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : ∀ (x_mem : x ∈ []), x ≠ [].getLast ⋯ → [].nextOr x d = [].nextOr x d'
x_ne : ¬x = y
x_mem : x = y
⊢ [y].nextOr x d = [y].nextOr x d'

Tactic:
contradiction

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d d' : α
x_mem : x ∈ []
x_ne : x ≠ [].getLast ⋯
⊢ [].nextOr x d = [].nextOr x d'

Tactic:
cases x_mem

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
by_cases h : x = y

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : ∀ (x_mem : x ∈ []), x ≠ [].getLast ⋯ → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y]
x_ne : x ≠ [y].getLast ⋯
⊢ [y].nextOr x d = [y].nextOr x d'

Tactic:
simp at x_mem x_ne

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : ∀ (x_mem : x ∈ []), x ≠ [].getLast ⋯ → [].nextOr x d = [].nextOr x d'
x_ne : ¬x = y
x_mem : x = y
⊢ [y].nextOr x d = [y].nextOr x d'

Proof state:
case neg.x_ne
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ z :: zs), x ≠ (z :: zs).getLast ⋯ → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ y :: z :: zs
x_ne : x ≠ (y :: z :: zs).getLast ⋯
h : ¬x = y
⊢ x ≠ (z :: zs).getLast ⋯

Tactic:
simpa using x_ne

Result:
no goals