internlm/Lean-Github huggingface dataset:
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ v ∈ vs
Tactic:
subst contra
Proof state after:
case left
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : x ∉ vs
⊢ x ∈ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case left
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : x ∉ vs
⊢ x ∈ vs
Tactic:
exact h1_left
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬y = v
Tactic:
intro contra
Proof state after:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ False
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ False
Tactic:
apply h2
Proof state after:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ v ∈ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : y = v
⊢ v ∈ vs
Tactic:
subst contra
Proof state after:
case right
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : y ∉ vs
⊢ y ∈ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case right
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
h2 : y ∉ vs
⊢ y ∈ vs
Tactic:
exact h1_right
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ True
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ True
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : v ∉ vs
⊢ NotFree Γ v phi.not_
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi.not_
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi.not_
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NotFree Γ v phi
Tactic:
exact phi_ih vs h1 h2
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
h2 : v ∉ vs
⊢ NotFree Γ v (phi.imp_ psi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v (phi.imp_ psi)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v (phi.imp_ psi)
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Tactic:
cases h1
Proof state after:
case intro
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
Tactic:
constructor
Proof state after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi

case right
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v psi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi
Tactic:
exact phi_ih vs h1_left h2
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case right
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v psi
Tactic:
exact psi_ih vs h1_right h2
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
h2 : v ∉ vs
⊢ NotFree Γ v (forall_ x phi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NotFree Γ v (forall_ x phi)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NotFree Γ v (forall_ x phi)
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ x = v ∨ NotFree Γ v phi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ x = v ∨ NotFree Γ v phi
Tactic:
by_cases c1 : x = v
Proof state after:
case pos
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v ∨ NotFree Γ v phi

case neg
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ x = v ∨ NotFree Γ v phi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case pos
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v ∨ NotFree Γ v phi
Tactic:
left
Proof state after:
case pos.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case pos.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v
Tactic:
exact c1
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ x = v ∨ NotFree Γ v phi
Tactic:
right
Proof state after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ NotFree Γ v phi
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ NotFree Γ v phi
Tactic:
apply phi_ih (x :: vs) h1
Proof state after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ x :: vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ x :: vs
Tactic:
simp
Proof state after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ ¬v = x ∧ v ∉ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ ¬v = x ∧ v ∉ vs
Tactic:
push_neg
Proof state after:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x ∧ v ∉ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x ∧ v ∉ vs
Tactic:
constructor
Proof state after:
case neg.h.left
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x

case neg.h.right
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ vs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h.left
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ≠ x
Tactic:
tauto
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case neg.h.right
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ v ∉ vs
Tactic:
exact h2
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (def_ X xs)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Tactic:
tauto
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
⊢ F.metaVarSet = ∅
Tactic:
induction F generalizing vs
Proof state after:
case meta_var_
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
⊢ (meta_var_ a✝).metaVarSet = ∅

case pred_
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
⊢ (pred_ a✝¹ a✝).metaVarSet = ∅

case eq_
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
⊢ (eq_ a✝¹ a✝).metaVarSet = ∅

case true_
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ true_.metaVarSet = ∅

case not_
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
⊢ a✝.not_.metaVarSet = ∅

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → a✝¹.metaVarSet = ∅
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
⊢ (a✝¹.imp_ a✝).metaVarSet = ∅

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
⊢ (forall_ a✝¹ a✝).metaVarSet = ∅

case def_
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
⊢ (def_ a✝¹ a✝).metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ (meta_var_ X).metaVarSet = ∅
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ (pred_ X xs).metaVarSet = ∅
Tactic:
case pred_ X xs =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
⊢ (eq_ x y).metaVarSet = ∅
Tactic:
case eq_ x y =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ true_.metaVarSet = ∅
Tactic:
case true_ =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ phi.not_.metaVarSet = ∅
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold Formula.metaVarSet
  exact phi_ih vs h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
⊢ (phi.imp_ psi).metaVarSet = ∅
Tactic:
case imp_ phi psi phi_ih psi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold Formula.metaVarSet
  cases h1
  case intro h1_left h1_right =>
    simp only [phi_ih vs h1_left]
    simp only [psi_ih vs h1_right]
    simp
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
⊢ (forall_ x phi).metaVarSet = ∅
Tactic:
case forall_ x phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold Formula.metaVarSet
  exact phi_ih (x :: vs) h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ (def_ X xs).metaVarSet = ∅
Tactic:
case def_ X xs =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ (meta_var_ X).metaVarSet = ∅
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
X : MetaVarName
vs : List VarName
h1 : False
⊢ (meta_var_ X).metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : MetaVarName
vs : List VarName
h1 : False
⊢ (meta_var_ X).metaVarSet = ∅
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ (pred_ X xs).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
⊢ (eq_ x y).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ true_.metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ phi.not_.metaVarSet = ∅
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ phi.not_.metaVarSet = ∅