rw [Nat.add_comm, Nat.add_assoc, Nat.add_comm (lengthOfFormula ϕ) (lengthOfSet (Finset.erase (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
⊢ lengthOfSet ((X \ S).erase ϕ) + (lengthOfSet S + 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 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