linarith
X Cond Res : Finset Formula
hyp : Res.sum lengthOfFormula < Cond.sum lengthOfFormula
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) + ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x) =
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
this : 0 ≤ ∑ x ∈ X \ Cond ∩ Res, ↑(lengthOfFormula x)
⊢ ∑ x ∈ X \ Cond ∪ Res, ↑(lengthOfFormula x) ≤
    ∑ x ∈ X, ↑(lengthOfFormula x) - ∑ x ∈ Cond, ↑(lengthOfFormula x) + ∑ x ∈ Res, ↑(lengthOfFormula x)
no goals