Theorem: Permutation.get_cyclic_not_mem (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
l : List (Fin n)
i : Fin n
h : ¬i ∈ l
⊢ (cyclic l)[↑i] = i
Tactic:
cases l with
| nil => exact get_one i.1
| cons j l =>
  dsimp [cyclic]
  simp only [List.mem_cons, not_or] at h
  suffices ∀ (y : Permutation n), (l.foldr _ y)[i.1] = y[i.1] by
    rewrite [this 1]; exact get_one i.1
  induction l with
  | nil => intros; rfl
  | cons k l IH =>
    intro y
    simp only [List.mem_cons, not_or] at h 
    specialize IH ⟨h.1,h.2.2⟩ y
    dsimp only [List.foldr]
    rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
    exact IH
State after:
no goals

State before:
case nil
n : Nat
i : Fin n
h : ¬i ∈ []
⊢ (cyclic [])[↑i] = i
Tactic:
exact get_one i.1
State after:
no goals

State before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (cyclic (j :: l))[↑i] = i
Tactic:
dsimp [cyclic]
State after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i

State before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
simp only [List.mem_cons, not_or] at h
State after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i

State before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
suffices ∀ (y : Permutation n), (l.foldr _ y)[i.1] = y[i.1] by
  rewrite [this 1]; exact get_one i.1
State after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]

State before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Tactic:
induction l with
| nil => intros; rfl
| cons k l IH =>
  intro y
  simp only [List.mem_cons, not_or] at h 
  specialize IH ⟨h.1,h.2.2⟩ y
  dsimp only [List.foldr]
  rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
  exact IH
State after:
no goals

State before:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (?m.45215 y) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
rewrite [this 1]
State after:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ 1[↑i] = i

State before:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ 1[↑i] = i
Tactic:
exact get_one i.1
State after:
no goals

State before:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y [])[↑i] = y[↑i]
Tactic:
intros
State after:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
y✝ : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y✝ [])[↑i] = y✝[↑i]

State before:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
y✝ : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y✝ [])[↑i] = y✝[↑i]
Tactic:
rfl
State after:
no goals

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
intro y
State after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
y : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
y : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
simp only [List.mem_cons, not_or] at h
State after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
specialize IH ⟨h.1,h.2.2⟩ y
State after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
dsimp only [List.foldr]
State after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (swap (List.foldr (fun j_1 x => swap x j j_1) y l) j k)[↑i] = y[↑i]

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (swap (List.foldr (fun j_1 x => swap x j j_1) y l) j k)[↑i] = y[↑i]
Tactic:
rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
State after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]

State before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Tactic:
exact IH
State after:
no goals