rw [anotherClaim] at claim
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet X = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X