Theorem: proj_does_not_increase_vocab (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 φ φ_in_proj ℓ ℓ_in_φ
State after:
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula

State before:
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Tactic:
rw [proj] at φ_in_proj
State after:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula

State before:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
Tactic:
simp
State after:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ X, ℓ ∈ vocabOfFormula a

State before:
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ X, ℓ ∈ vocabOfFormula a
Tactic:
tauto
State after:
no goals