have anotherClaim : insert ϕ (X \ {ϕ}) = X := by
  ext1
  simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton]
  constructor
  aesop
  tauto
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X