Theorem: Fin.OrbitChain.not_mem (Fifteen/Data/Fin/Basic.lean)

State before:
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
⊢ ¬i ∈ l
Tactic:
cases h with
| single => exact List.not_mem_nil _
| cons hnotmem _ => exact hnotmem
State after:
no goals

State before:
case single
m n : Nat
f : Fin n → Fin n
i : Fin n
⊢ ¬i ∈ []
Tactic:
exact List.not_mem_nil _
State after:
no goals

State before:
case cons
m n : Nat
f : Fin n → Fin n
j i✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j
⊢ ¬f i✝ ∈ i✝ :: l✝
Tactic:
exact hnotmem
State after:
no goals