Theorem: vocUnion (Bml/Vocabulary.lean)

State before:
X Y : Finset Formula
⊢ voc (X ∪ Y) = voc X ∪ voc Y
Tactic:
simp
State after:
X Y : Finset Formula
⊢ (X ∪ Y).biUnion vocabOfFormula = X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula

State before:
X Y : Finset Formula
⊢ (X ∪ Y).biUnion vocabOfFormula = X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Tactic:
ext1
State after:
case a
X Y : Finset Formula
a✝ : Char
⊢ a✝ ∈ (X ∪ Y).biUnion vocabOfFormula ↔ a✝ ∈ X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula

State before:
case a
X Y : Finset Formula
a✝ : Char
⊢ a✝ ∈ (X ∪ Y).biUnion vocabOfFormula ↔ a✝ ∈ X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Tactic:
aesop
State after:
no goals