Theorem: projSet (Bml/Tableau.lean)

State before:
X : Finset Formula
⊢ ↑(projection X) = {ϕ | □ϕ ∈ X}
Tactic:
ext1
State after:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ ↑(projection X) ↔ x✝ ∈ {ϕ | □ϕ ∈ X}

State before:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ ↑(projection X) ↔ x✝ ∈ {ϕ | □ϕ ∈ X}
Tactic:
simp
State after:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ projection X ↔ □x✝ ∈ X

State before:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ projection X ↔ □x✝ ∈ X
Tactic:
exact proj
State after:
no goals