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

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (swap (swap x i j) i j)[k] = x[k]
Tactic:
simp only [get_swap, if_pos]
State after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
State after:
case t.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

State before:
case t.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
all_goals simp only [hik, hjk, if_pos, if_neg]
State after:
case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if k = ↑i then x[↑i] else x[k]) = x[k]

State before:
case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if k = ↑i then x[↑i] else x[k]) = x[k]
Tactic:
rw [if_neg (Ne.symm hik)]
State after:
no goals

State before:
case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
simp only [hik, hjk, if_pos, if_neg]
State after:
no goals