Theorem: vocProj (Bml/Tableau.lean)

State before:
X : Finset Formula
⊢ voc (projection X) ⊆ voc X
Tactic:
simp
State after:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula

State before:
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
Tactic:
intro ϕ phi_in_proj
State after:
X : Finset Formula
ϕ : Formula
phi_in_proj : ϕ ∈ projection X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula

State before:
X : Finset Formula
ϕ : Formula
phi_in_proj : ϕ ∈ projection X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Tactic:
rw [proj] at phi_in_proj
State after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula

State before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
Tactic:
intro a aInVocPhi
State after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ a ∈ X.biUnion vocabOfFormula

State before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ a ∈ X.biUnion vocabOfFormula
Tactic:
simp
State after:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1

State before:
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
tauto
State after:
no goals