Theorem: vocOfBigCon (Bml/bigConDis.lean)

State before:
x : Char
l : List Formula
⊢ x ∈ voc (bigCon l) → ∃ φ ∈ l, x ∈ voc φ
Tactic:
intro hyp
State after:
x : Char
l : List Formula
hyp : x ∈ voc (bigCon l)
⊢ ∃ φ ∈ l, x ∈ voc φ

State before:
x : Char
l : List Formula
hyp : x ∈ voc (bigCon l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Tactic:
induction l
State after:
case nil
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ

case cons
x : Char
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∈ voc (bigCon tail✝) → ∃ φ ∈ tail✝, x ∈ voc φ
hyp : x ∈ voc (bigCon (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, x ∈ voc φ

State before:
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
case nil  => aesop
State after:
no goals

State before:
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
aesop
State after:
no goals

State before:
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
cases em (x ∈ vocabOfFormula head)
State after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

State before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
simp
State after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a

State before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Tactic:
tauto
State after:
no goals

State before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
unfold bigCon at hyp
State after:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

State before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
aesop
State after:
no goals