calc
  (projection (insert f S)).sum lengthOfFormula
    = (projection {f} ∪ projection S).sum lengthOfFormula := by rw [insert_comm_proj S f]
  _ ≤ (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula := by
    apply sum_union_le
  _ ≤ lengthOfFormula f + (projection S).sum lengthOfFormula := by
    simp only [add_le_add_iff_right, projection_length_leq]
  _ ≤ lengthOfFormula f + S.sum lengthOfFormula := by simp; apply IH
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
no goals