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

State before:
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
k : Fin n
hk : ¬k ∈ l
hfk : f k ∈ i :: l
⊢ f k = j
Tactic:
induction l generalizing i with
| nil => cases h; exact List.mem_singleton.mp hfk
| cons k' l IH =>
  cases h with | cons hfk' htail =>
  specialize IH htail (List.not_mem_of_not_mem_cons hk)
  rewrite [List.mem_cons] at hfk
  rewrite [List.mem_cons, not_or] at hk
  cases hfk with
  | inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
  | inr h => exact IH h
State after:
no goals

State before:
case nil
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k i : Fin n
h : OrbitChain f i [] j
hk : ¬k ∈ []
hfk : f k ∈ [i]
⊢ f k = j
Tactic:
cases h
State after:
case nil.single
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k : Fin n
hk : ¬k ∈ []
hfk : f k ∈ [j]
⊢ f k = j

State before:
case nil.single
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k : Fin n
hk : ¬k ∈ []
hfk : f k ∈ [j]
⊢ f k = j
Tactic:
exact List.mem_singleton.mp hfk
State after:
no goals

State before:
case cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
IH : ∀ {i : Fin n}, OrbitChain f i l j → ¬k ∈ l → f k ∈ i :: l → f k = j
i : Fin n
h : OrbitChain f i (k' :: l) j
hk : ¬k ∈ k' :: l
hfk : f k ∈ i :: k' :: l
⊢ f k = j
Tactic:
cases h with | cons hfk' htail =>
specialize IH htail (List.not_mem_of_not_mem_cons hk)
rewrite [List.mem_cons] at hfk
rewrite [List.mem_cons, not_or] at hk
cases hfk with
| inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
| inr h => exact IH h
State after:
no goals

State before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
IH : ∀ {i : Fin n}, OrbitChain f i l j → ¬k ∈ l → f k ∈ i :: l → f k = j
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
⊢ f k = j
Tactic:
specialize IH htail (List.not_mem_of_not_mem_cons hk)
State after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j

State before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
rewrite [List.mem_cons] at hfk
State after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j

State before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
rewrite [List.mem_cons, not_or] at hk
State after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j

State before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
cases hfk with
| inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
| inr h => exact IH h
State after:
no goals

State before:
case cons.cons.inl
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
hfkk' : f k = f k'
⊢ f k = j
Tactic:
exact absurd (f_inj _ _ hfkk') hk.1
State after:
no goals

State before:
case cons.cons.inr
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
h : f k ∈ k' :: l
⊢ f k = j
Tactic:
exact IH h
State after:
no goals