Theorem: vocElem_subs_vocSet (Bml/Vocabulary.lean)

State before:
ϕ : Formula
X : Finset Formula
⊢ ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X
Tactic:
induction X using Finset.induction_on
State after:
case empty
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : ϕ ∈ s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula s✝
⊢ ϕ ∈ insert a✝² s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert a✝² s✝)

State before:
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
case empty =>
  intro phi_in_X;
  cases phi_in_X
State after:
no goals

State before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
⊢ ϕ ∈ insert ψ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
case insert ψ S _ _ =>
  intro psi_in_insert
  simp at *
  intro a aIn
  aesop
State after:
no goals

State before:
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
intro phi_in_X
State after:
ϕ : Formula
phi_in_X : ϕ ∈ ∅
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅

State before:
ϕ : Formula
phi_in_X : ϕ ∈ ∅
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
cases phi_in_X
State after:
no goals

State before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
⊢ ϕ ∈ insert ψ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
intro psi_in_insert
State after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
psi_in_insert : ϕ ∈ insert ψ S
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)

State before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
psi_in_insert : ϕ ∈ insert ψ S
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
simp at *
State after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
⊢ vocabOfFormula ϕ ⊆ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula

State before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
⊢ vocabOfFormula ϕ ⊆ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
Tactic:
intro a aIn
State after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
a : Char
aIn : a ∈ vocabOfFormula ϕ
⊢ a ∈ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula

State before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
a : Char
aIn : a ∈ vocabOfFormula ϕ
⊢ a ∈ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
Tactic:
aesop
State after:
no goals