Theorem: vocErase (Bml/Vocabulary.lean)

State before:
X : Finset Formula
ϕ : Formula
⊢ voc (X \ {ϕ}) ⊆ voc X
Tactic:
apply vocMonotone
State after:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} ⊆ X

State before:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} ⊆ X
Tactic:
rw [sdiff_singleton_is_erase]
State after:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X.erase ϕ ⊆ X

State before:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X.erase ϕ ⊆ X
Tactic:
intro a aIn
State after:
case hyp
X : Finset Formula
ϕ a : Formula
aIn : a ∈ X.erase ϕ
⊢ a ∈ X

State before:
case hyp
X : Finset Formula
ϕ a : Formula
aIn : a ∈ X.erase ϕ
⊢ a ∈ X
Tactic:
exact Finset.mem_of_mem_erase aIn
State after:
no goals