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

State before:
m n : Nat
⊢ sign 1 = false
Tactic:
dsimp [sign]
State after:
m n : Nat
⊢ (inversionNum 1 % 2 == 1) = false

State before:
m n : Nat
⊢ (inversionNum 1 % 2 == 1) = false
Tactic:
rewrite [inversionNum_one]
State after:
m n : Nat
⊢ (0 % 2 == 1) = false

State before:
m n : Nat
⊢ (0 % 2 == 1) = false
Tactic:
decide
State after:
no goals