rw [← this]
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑C