Theorem: vocPreserved (Bml/Vocabulary.lean)

State before:
X : Finset Formula
ψ ϕ : Formula
⊢ ψ ∈ X → voc ϕ = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ})
Tactic:
intro psi_in_X eq_voc
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})
Tactic:
simp at *
State after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

State before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
Tactic:
ext1
State after:
case a
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

State before:
case a
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
Tactic:
constructor
State after:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula → a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula → a✝ ∈ X.biUnion vocabOfFormula

State before:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula → a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula → a✝ ∈ X.biUnion vocabOfFormula
Tactic:
all_goals intro a_in
State after:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ X.biUnion vocabOfFormula
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a✝ ∈ X.biUnion vocabOfFormula

State before:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ X.biUnion vocabOfFormula
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a✝ ∈ X.biUnion vocabOfFormula
Tactic:
all_goals norm_num at *
State after:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : ∃ a ∈ X, a✝ ∈ vocabOfFormula a
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a

State before:
case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula → a✝ ∈ X.biUnion vocabOfFormula
Tactic:
intro a_in
State after:
case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a✝ ∈ X.biUnion vocabOfFormula

State before:
case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a✝ ∈ X.biUnion vocabOfFormula
Tactic:
norm_num at *
State after:
case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a

State before:
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : ∃ a ∈ X, a✝ ∈ vocabOfFormula a
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Tactic:
rcases a_in with ⟨θ, _, a_in_vocTheta⟩
State after:
case a.mp.intro.intro
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

State before:
case a.mp.intro.intro
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Tactic:
by_cases h : θ = ψ
State after:
case pos
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

case neg
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

State before:
case pos
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Tactic:
aesop
State after:
no goals

State before:
case neg
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
Tactic:
aesop
State after:
no goals

State before:
case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Tactic:
aesop
State after:
no goals