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

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

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