Theorem: conDecreasesLength (Bml/Tableau.lean)

State before:
φ ψ : Formula
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
cases' em (φ = ψ) with heq hneq
State after:
case inl
φ ψ : Formula
heq : φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ

case inr
φ ψ : Formula
hneq : ¬φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ

State before:
case inl
φ ψ : Formula
heq : φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
simp [heq] at *
State after:
no goals

State before:
case inr
φ ψ : Formula
hneq : ¬φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
simp [Finset.sum_pair hneq]
State after:
no goals