Theorem: OrientableInvolutiveInv.not_pos_inv_of_pos (GroupComp/SymmFreeGroup.lean)

State before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
⊢ ¬pos x⁻¹ = true
Tactic:
have := h ▸ selection x
State after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
this : xor true (pos x⁻¹) = true
⊢ ¬pos x⁻¹ = true

State before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = true
this : xor true (pos x⁻¹) = true
⊢ ¬pos x⁻¹ = true
Tactic:
simp_all only [Bool.true_xor, Bool.not_eq_true', not_false_eq_true]
State after:
no goals