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

State before:
m n : Nat
x y : Permutation n
⊢ sign (x * y * inv x) = sign y
Tactic:
simp only [sign_mul]
State after:
m n : Nat
x y : Permutation n
⊢ ((sign x != sign y) != sign (inv x)) = sign y

State before:
m n : Nat
x y : Permutation n
⊢ ((sign x != sign y) != sign (inv x)) = sign y
Tactic:
rw [sign_inv, Bool.bne_comm x.sign, Bool.bne_assoc, Bool.bne_self, Bool.bne_false]
State after:
no goals