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

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (x * transpos i j)[k] = (swap x i j)[k]
Tactic:
simp only [get_mul, get_transpos, get_swap]
State after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
if hjk : j.1 = k then
  cases hjk; simp only [if_pos]
else if hik : i.1 = k then
  cases hik; simp only [if_neg hjk, if_pos]
else
  simp only [if_neg hjk, if_neg hik]
State after:
no goals

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hjk : ↑j = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
cases hjk
State after:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]

State before:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]
Tactic:
simp only [if_pos]
State after:
no goals

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

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hjk : ¬↑j = k
hik : ↑i = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
cases hik
State after:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑i < n
hjk : ¬↑j = ↑i
⊢ x[↑(if ↑j = ↑i then i else if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑j = ↑i then x[↑i] else if ↑i = ↑i then x[↑j] else x[↑i]

State before:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑i < n
hjk : ¬↑j = ↑i
⊢ x[↑(if ↑j = ↑i then i else if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑j = ↑i then x[↑i] else if ↑i = ↑i then x[↑j] else x[↑i]
Tactic:
simp only [if_neg hjk, if_pos]
State after:
no goals

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