Theorem: Permutation.sign_swap (Fifteen/Data/Permutation/Sign.lean)

State before:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ sign (swap x i j) = !sign x
Tactic:
rewrite [← mul_transpose_eq_swap, sign_mul, sign_transpos i j h]
State after:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ (sign x != true) = !sign x

State before:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ (sign x != true) = !sign x
Tactic:
exact Bool.bne_true _
State after:
no goals