Theorem: Fin.OrbitChain.nodup (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
⊢ List.Nodup (i :: l)
Tactic:
induction h with
| single => exact .cons (fun _ h => nomatch h) .nil
| cons hnotmem _ IH =>
  refine .cons ?_ IH
  intro _ hfa h; cases h
  exact hnotmem hfa
State after:
no goals

State before:
case single
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ : Fin n
⊢ List.Nodup [i✝]
Tactic:
exact .cons (fun _ h => nomatch h) .nil
State after:
no goals

State before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ List.Nodup (f i✝ :: i✝ :: l✝)
Tactic:
refine .cons ?_ IH
State after:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ ∀ (a' : Fin n), a' ∈ i✝ :: l✝ → f i✝ ≠ a'

State before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ ∀ (a' : Fin n), a' ∈ i✝ :: l✝ → f i✝ ≠ a'
Tactic:
intro _ hfa h
State after:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
a'✝ : Fin n
hfa : a'✝ ∈ i✝ :: l✝
h : f i✝ = a'✝
⊢ False

State before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
a'✝ : Fin n
hfa : a'✝ ∈ i✝ :: l✝
h : f i✝ = a'✝
⊢ False
Tactic:
cases h
State after:
case cons.refl
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
hfa : f i✝ ∈ i✝ :: l✝
⊢ False

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