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

State before:
n : Nat
i j : Fin n
⊢ transpos i j * transpos i j = 1
Tactic:
rewrite [mul_transpose_eq_swap]
State after:
n : Nat
i j : Fin n
⊢ swap (transpos i j) i j = 1

State before:
n : Nat
i j : Fin n
⊢ swap (transpos i j) i j = 1
Tactic:
dsimp [transpos]
State after:
n : Nat
i j : Fin n
⊢ swap (swap 1 i j) i j = 1

State before:
n : Nat
i j : Fin n
⊢ swap (swap 1 i j) i j = 1
Tactic:
exact swap_swap_same 1 i j
State after:
no goals