rw [← hmem] at this
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
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