Theorem: vocPreservedSub (Bml/Vocabulary.lean)

State before:
X : Finset Formula
ψ ϕ : Formula
⊢ ψ ∈ X → voc ϕ ⊆ voc ψ → voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X
Tactic:
intro psi_in_X sub_voc
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : voc ϕ ⊆ voc ψ
⊢ voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : voc ϕ ⊆ voc ψ
⊢ voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X
Tactic:
simp at *
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
⊢ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula ⊆ X.biUnion vocabOfFormula

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
⊢ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula ⊆ X.biUnion vocabOfFormula
Tactic:
intro a a_in
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a ∈ X.biUnion vocabOfFormula

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a ∈ X.biUnion vocabOfFormula
Tactic:
norm_num at *
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∨ ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∨ ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
cases a_in
State after:
case inl
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1

case inr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1

State before:
case inl
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
use ψ
State after:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ

State before:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Tactic:
rw [Finset.subset_iff] at sub_voc
State after:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : ∀ ⦃x : Char⦄, x ∈ vocabOfFormula ϕ → x ∈ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ

State before:
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : ∀ ⦃x : Char⦄, x ∈ vocabOfFormula ϕ → x ∈ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
Tactic:
tauto
State after:
no goals

State before:
case inr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
Tactic:
aesop
State after:
no goals