Theorem: projection_length_leq (Bml/Tableau.lean)

State before:
⊢ ∀ (f : Formula), (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
Tactic:
intro f
State after:
f : Formula
⊢ (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f

State before:
f : Formula
⊢ (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
Tactic:
cases f
State after:
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom

case atom_prop
a✝ : Char
⊢ (projection {·a✝}).sum lengthOfFormula ≤ lengthOfFormula (·a✝)

case neg
a✝ : Formula
⊢ (projection {~a✝}).sum lengthOfFormula ≤ lengthOfFormula (~a✝)

case And
a✝¹ a✝ : Formula
⊢ (projection {a✝¹⋀a✝}).sum lengthOfFormula ≤ lengthOfFormula (a✝¹⋀a✝)

case box
a✝ : Formula
⊢ (projection {□a✝}).sum lengthOfFormula ≤ lengthOfFormula (□a✝)

State before:
f : Formula
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
case box f =>
  have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp
  rw [subsubClaim]
  simp
State after:
no goals

State before:
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom
Tactic:
unfold projection
State after:
case bottom

⊢ (let X := {bottom};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula bottom

State before:
case bottom

⊢ (let X := {bottom};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula bottom
Tactic:
simp
State after:
no goals

State before:
case atom_prop
a✝ : Char
⊢ (projection {·a✝}).sum lengthOfFormula ≤ lengthOfFormula (·a✝)
Tactic:
unfold projection
State after:
case atom_prop
a✝ : Char
⊢ (let X := {·a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (·a✝)

State before:
case atom_prop
a✝ : Char
⊢ (let X := {·a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (·a✝)
Tactic:
simp
State after:
no goals

State before:
case neg
a✝ : Formula
⊢ (projection {~a✝}).sum lengthOfFormula ≤ lengthOfFormula (~a✝)
Tactic:
unfold projection
State after:
case neg
a✝ : Formula
⊢ (let X := {~a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (~a✝)

State before:
case neg
a✝ : Formula
⊢ (let X := {~a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (~a✝)
Tactic:
simp
State after:
no goals

State before:
case And
a✝¹ a✝ : Formula
⊢ (projection {a✝¹⋀a✝}).sum lengthOfFormula ≤ lengthOfFormula (a✝¹⋀a✝)
Tactic:
unfold projection
State after:
case And
a✝¹ a✝ : Formula
⊢ (let X := {a✝¹⋀a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (a✝¹⋀a✝)

State before:
case And
a✝¹ a✝ : Formula
⊢ (let X := {a✝¹⋀a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (a✝¹⋀a✝)
Tactic:
simp
State after:
no goals

State before:
f : Formula
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp
State after:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)

State before:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
rw [subsubClaim]
State after:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ {f}.sum lengthOfFormula ≤ lengthOfFormula (□f)

State before:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ {f}.sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
simp
State after:
no goals

State before:
f : Formula
⊢ projection {□f} = {f}
Tactic:
ext1
State after:
case a
f a✝ : Formula
⊢ a✝ ∈ projection {□f} ↔ a✝ ∈ {f}

State before:
case a
f a✝ : Formula
⊢ a✝ ∈ projection {□f} ↔ a✝ ∈ {f}
Tactic:
rw [proj]
State after:
case a
f a✝ : Formula
⊢ □a✝ ∈ {□f} ↔ a✝ ∈ {f}

State before:
case a
f a✝ : Formula
⊢ □a✝ ∈ {□f} ↔ a✝ ∈ {f}
Tactic:
simp
State after:
no goals