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

State before:
m n i : Nat
h : i + 1 < n
⊢ sign (transposAdj i h) = true
Tactic:
dsimp [sign]
State after:
m n i : Nat
h : i + 1 < n
⊢ (inversionNum (transposAdj i h) % 2 == 1) = true

State before:
m n i : Nat
h : i + 1 < n
⊢ (inversionNum (transposAdj i h) % 2 == 1) = true
Tactic:
rewrite [inversionNum_transposAdj]
State after:
m n i : Nat
h : i + 1 < n
⊢ (1 % 2 == 1) = true

State before:
m n i : Nat
h : i + 1 < n
⊢ (1 % 2 == 1) = true
Tactic:
decide
State after:
no goals