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

State before:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
⊢ pos x ≠ pos x⁻¹
Tactic:
intro h
State after:
X : Type u_1
inst✝ : OrientableInvolutiveInv X
x x' : X
h : pos x = pos x⁻¹
⊢ False

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

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