Theorem: localRuleAppDecreasesLengthSide (Bml/Tableau.lean)

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf (X \ Cond ∪ Res) < lengthOf X
Tactic:
rw [zlen_iff]
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X
Tactic:
calc zlengthOfSet (X \ Cond ∪ Res)
    ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res := by
        have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
        have : zlengthOfSet (X \ Cond ∩ Res) ≥ 0 := zlengthOfSet.pos
        simp_all
        linarith
  _ = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res := by
        simp only [zlengthOfSet]
        rw [Finset.sum_sdiff_eq_sub precondProof]
  _ < zlengthOfSet X := by
        have : zlengthOfSet Res < zlengthOfSet Cond := by
          rw [← zlen_iff]
          exact hyp
        linarith
State after:
no goals

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
have : zlengthOfSet (X \ Cond ∩ Res) ≥ 0 := zlengthOfSet.pos
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
this : zlengthOfSet (X \ Cond ∩ Res) ≥ 0
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this✝ :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
this : zlengthOfSet (X \ Cond ∩ Res) ≥ 0
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
Tactic:
simp_all
State after:
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)

State before:
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)
Tactic:
linarith
State after:
no goals

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond) + zlengthOfSet Res = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res
Tactic:
simp only [zlengthOfSet]
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ (X \ Cond).sum zlengthOf + Res.sum zlengthOf = X.sum zlengthOf - Cond.sum zlengthOf + Res.sum zlengthOf

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ (X \ Cond).sum zlengthOf + Res.sum zlengthOf = X.sum zlengthOf - Cond.sum zlengthOf + Res.sum zlengthOf
Tactic:
rw [Finset.sum_sdiff_eq_sub precondProof]
State after:
no goals

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
Tactic:
have : zlengthOfSet Res < zlengthOfSet Cond := by
  rw [← zlen_iff]
  exact hyp
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this : zlengthOfSet Res < zlengthOfSet Cond
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this : zlengthOfSet Res < zlengthOfSet Cond
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
Tactic:
linarith
State after:
no goals

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet Res < zlengthOfSet Cond
Tactic:
rw [← zlen_iff]
State after:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf Res < lengthOf Cond

State before:
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf Res < lengthOf Cond
Tactic:
exact hyp
State after:
no goals