simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton]
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ insert ϕ (X \ {ϕ}) ↔ a✝ ∈ X
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ ↔ a✝ ∈ X