internlm/Lean-Github huggingface dataset:
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
a : Char
aIn : a ∈ vocabOfFormula ϕ
⊢ a ∈ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
Tactic:
aesop
Proof state after:
no goals
Theorem: vocMonotone
Proof state before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ voc X ⊆ voc Y
Tactic:
unfold voc
Proof state after:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ setFormulaHasVocabulary.1 X ⊆ setFormulaHasVocabulary.1 Y
Theorem: vocMonotone
Proof state before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ setFormulaHasVocabulary.1 X ⊆ setFormulaHasVocabulary.1 Y
Tactic:
simp at *
Proof state after:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ ∀ x ∈ X, vocabOfFormula x ⊆ Y.biUnion vocabOfFormula
Theorem: vocMonotone
Proof state before:
X Y : Finset Formula
hyp : X ⊆ Y
⊢ ∀ x ∈ X, vocabOfFormula x ⊆ Y.biUnion vocabOfFormula
Tactic:
intro a aIn
Proof state after:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula
Theorem: vocMonotone
Proof state before:
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula
Tactic:
unfold Finset.biUnion at *
Proof 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
Theorem: vocMonotone
Proof 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
Proof 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
Theorem: vocMonotone
Proof 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
Proof state after:
no goals
Theorem: vocErase
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ voc (X \ {ϕ}) ⊆ voc X
Tactic:
apply vocMonotone
Proof state after:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} ⊆ X
Theorem: vocErase
Proof state before:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} ⊆ X
Tactic:
rw [sdiff_singleton_is_erase]
Proof state after:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X.erase ϕ ⊆ X
Theorem: vocErase
Proof state before:
case hyp
X : Finset Formula
ϕ : Formula
⊢ X.erase ϕ ⊆ X
Tactic:
intro a aIn
Proof state after:
case hyp
X : Finset Formula
ϕ a : Formula
aIn : a ∈ X.erase ϕ
⊢ a ∈ X
Theorem: vocErase
Proof state before:
case hyp
X : Finset Formula
ϕ a : Formula
aIn : a ∈ X.erase ϕ
⊢ a ∈ X
Tactic:
exact Finset.mem_of_mem_erase aIn
Proof state after:
no goals
Theorem: vocUnion
Proof state before:
X Y : Finset Formula
⊢ voc (X ∪ Y) = voc X ∪ voc Y
Tactic:
simp
Proof state after:
X Y : Finset Formula
⊢ (X ∪ Y).biUnion vocabOfFormula = X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Theorem: vocUnion
Proof state before:
X Y : Finset Formula
⊢ (X ∪ Y).biUnion vocabOfFormula = X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Tactic:
ext1
Proof state after:
case a
X Y : Finset Formula
a✝ : Char
⊢ a✝ ∈ (X ∪ Y).biUnion vocabOfFormula ↔ a✝ ∈ X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Theorem: vocUnion
Proof state before:
case a
X Y : Finset Formula
a✝ : Char
⊢ a✝ ∈ (X ∪ Y).biUnion vocabOfFormula ↔ a✝ ∈ X.biUnion vocabOfFormula ∪ Y.biUnion vocabOfFormula
Tactic:
aesop
Proof state after:
no goals
Theorem: vocPreserved
Proof state before:
X : Finset Formula
ψ ϕ : Formula
⊢ ψ ∈ X → voc ϕ = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ})
Tactic:
intro psi_in_X eq_voc
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})
Theorem: vocPreserved
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})
Tactic:
simp at *
Proof state after:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
Theorem: vocPreserved
Proof state before:
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
Tactic:
ext1
Proof 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
Theorem: vocPreserved
Proof 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
Proof 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
Theorem: vocPreserved
Proof 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
Proof 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
Theorem: vocPreserved
Proof 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 *
Proof 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
Theorem: vocPreserved
Proof 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
Proof 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
Theorem: vocPreserved
Proof 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 *
Proof 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
Theorem: vocPreserved
Proof 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⟩
Proof 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
Theorem: vocPreserved
Proof 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 : θ = ψ
Proof 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
Theorem: vocPreserved
Proof 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
Proof state after:
no goals
Theorem: vocPreserved
Proof 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
Proof state after:
no goals
Theorem: vocPreserved
Proof 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
Proof state after:
no goals
Theorem: vocPreservedTwo
Proof state before:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
⊢ ψ ∈ X → voc {ϕ1, ϕ2} = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2})
Tactic:
intro psi_in_X eq_voc
Proof state after:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2})
Theorem: vocPreservedTwo
Proof state before:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2})
Tactic:
rw [vocUnion]
Proof state after:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ}) ∪ voc {ϕ1, ϕ2}
Theorem: vocPreservedTwo
Proof state before:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ}) ∪ voc {ϕ1, ϕ2}
Tactic:
simp at *
Proof state after:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
Theorem: vocPreservedTwo
Proof state before:
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
Tactic:
ext1
Proof state after:
case a
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
Theorem: vocPreservedTwo
Proof state before:
case a
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
Tactic:
constructor
Proof state after:
case a.mp
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula → a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)

case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2) → a✝ ∈ X.biUnion vocabOfFormula
Theorem: vocPreservedTwo
Proof state before:
case a.mp
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula → a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)

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

case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Theorem: vocPreservedTwo
Proof state before:
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Tactic:
cases a_in
Proof state after:
case a.mpr.inl
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a

case a.mpr.inr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Theorem: vocPreservedTwo
Proof state before:
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2) → a✝ ∈ X.biUnion vocabOfFormula
Tactic:
intro a_in
Proof state after:
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
⊢ a✝ ∈ X.biUnion vocabOfFormula
Theorem: vocPreservedTwo
Proof state before:
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
⊢ a✝ ∈ X.biUnion vocabOfFormula
Tactic:
norm_num at *
Proof state after:
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
Theorem: vocPreservedTwo
Proof state before:
case a.mp
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : ∃ a ∈ X, a✝ ∈ vocabOfFormula a
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
rcases a_in with ⟨θ, theta_in_X, a_in_vocTheta⟩
Proof state after:
case a.mp.intro.intro
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case a.mp.intro.intro
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
by_cases h : θ = ψ
Proof state after:
case pos
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2

case neg
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case pos
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
right
Proof state after:
case pos.h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case pos.h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
subst h
Proof state after:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
psi_in_X : θ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula θ
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Theorem: vocPreservedTwo
Proof state before:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
psi_in_X : θ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula θ
⊢ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
Tactic:
unfold vocabOfSetFormula vocabOfFormula at *
Proof state after:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  a✝ ∈
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
Theorem: vocPreservedTwo
Proof state before:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  a✝ ∈
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
Tactic:
rw [← eq_voc] at a_in_vocTheta
Proof state after:
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  a✝ ∈
    (match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ