have : (maxInvFreeSet X).val ⊆ C.val := by
  show (maxInvFreeSet X).val ⊆ (maxInvFreeSet X).val.insert x⁻¹
  intro _; aesop (add norm simp [Set.insert])
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))) }
⊢ 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
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)