Theorem: vocMonotone (Bml/Vocabulary.lean)

State before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ voc X ⊆ voc Y
Tactic:
unfold voc
State after:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ setFormulaHasVocabulary.1 X ⊆ setFormulaHasVocabulary.1 Y

State before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ setFormulaHasVocabulary.1 X ⊆ setFormulaHasVocabulary.1 Y
Tactic:
simp at *
State after:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ ∀ x ∈ X, vocabOfFormula x ⊆ Y.biUnion vocabOfFormula

State before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ ∀ x ∈ X, vocabOfFormula x ⊆ Y.biUnion vocabOfFormula
Tactic:
intro a aIn
State after:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula

State before:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula
Tactic:
unfold Finset.biUnion at *
State after:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset

State before:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset
Tactic:
intro p pIn
State after:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
p : Char
pIn : p ∈ vocabOfFormula a
⊢ p ∈ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset

State before:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
p : Char
pIn : p ∈ vocabOfFormula a
⊢ p ∈ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset
Tactic:
aesop
State after:
no goals