Theorem: Classical.ProperInvolutiveInv.selection (GroupComp/SymmFreeGroup.lean)

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ xor (orientation x) (orientation x⁻¹) = true
Tactic:
rw [@Bool.xor_iff_ne]
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ orientation x ≠ orientation x⁻¹

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ orientation x ≠ orientation x⁻¹
Tactic:
dsimp [orientation]
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))
Tactic:
rw [@decide_eq_decide]
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))
Tactic:
intro hmem
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
rw [@iff_eq_eq] at hmem
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
⊢ False

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
⊢ False
Tactic:
by_cases hx:x ∈ (maxInvFreeSet X).val
State after:
case pos
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∈ ↑(maxInvFreeSet X)
⊢ False

case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
⊢ False

State before:
case pos
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
exact (maxInvFreeSet X).prop x hx (hmem ▸ hx)
State after:
no goals

State before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
⊢ False
Tactic:
have :=  maxInvFreeSet_mem_inv hx
State after:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False

State before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
rw [← hmem] at this
State after:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x ∈ ↑(maxInvFreeSet X)
⊢ False

State before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
contradiction
State after:
no goals