rw [lengthRemove (X \ S) ϕ, Nat.add_comm, ih subs_X]
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet S + (lengthOfSet ((X \ S).erase ϕ) + lengthOfFormula ϕ) = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet X = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X \ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X