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

State before:
m n : Nat
x : Permutation n
⊢ sign (inv x) = sign x
Tactic:
have : sign (x.inv * x) = sign (1 : Permutation n) := x.inv_mul ▸ rfl
State after:
m n : Nat
x : Permutation n
this : sign (inv x * x) = sign 1
⊢ sign (inv x) = sign x

State before:
m n : Nat
x : Permutation n
this : sign (inv x * x) = sign 1
⊢ sign (inv x) = sign x
Tactic:
conv at this =>
  simp only [sign_mul, sign_one]
  rewrite [Bool.bne_eq_false]
State after:
m n : Nat
x : Permutation n
this : sign (inv x) = sign x
⊢ sign (inv x) = sign x

State before:
m n : Nat
x : Permutation n
this : sign (inv x) = sign x
⊢ sign (inv x) = sign x
Tactic:
exact this
State after:
no goals