internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem
Proof state before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
⊢ admitsAux P zs H ∅ F
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
⊢ ∀ x ∉ ∅, V x = V x
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_is_valid
Proof state before:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : F.IsValid
⊢ (replace P zs H F).IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replace P zs H F).IsValid
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_is_valid
Proof state before:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ (replace P zs H F).IsValid
Tactic:
simp only [IsValid]
Proof state after:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (replace P zs H F)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_is_valid
Proof state before:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E (replace P zs H F)
Tactic:
intro D I V E
Proof state after:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (replace P zs H F)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_is_valid
Proof state before:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E (replace P zs H F)
Tactic:
simp only [← substitution_theorem D I V E F P zs H h1]
Proof state after:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D (I' D I V E P zs H) V E F
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_is_valid
Proof state before:
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D (I' D I V E P zs H) V E F
Tactic:
apply h2
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ↔ v ∈ F.varSet
Tactic:
induction F
Proof state after:
case pred_
v : Var
a✝¹ : String
a✝ : List Var
⊢ occursIn v (pred_ a✝¹ a✝) ↔ v ∈ (pred_ a✝¹ a✝).varSet

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v a✝.not_ ↔ v ∈ a✝.not_.varSet

case imp_
v : Var
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ↔ v ∈ a✝¹.varSet
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).varSet

case forall_
v : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ↔ v ∈ (pred_ X vs).varSet
Tactic:
case pred_ X vs =>
  simp only [occursIn]
  simp only [varSet]
  simp
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi.not_ ↔ v ∈ phi.not_.varSet
Tactic:
case not_ phi phi_ih =>
  simp only [occursIn]
  simp only [varSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v (phi.imp_ psi) ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
case imp_ phi psi phi_ih psi_ih =>
  simp only [occursIn]
  simp only [varSet]
  simp
  congr!
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v (forall_ a✝ phi) ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
case forall_ _ phi phi_ih =>
  simp only [occursIn]
  simp only [varSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ↔ v ∈ (pred_ X vs).varSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ (pred_ X vs).varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ (pred_ X vs).varSet
Tactic:
simp only [varSet]
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ vs.toFinset
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ↔ v ∈ vs.toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi.not_ ↔ v ∈ phi.not_.varSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.not_.varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.not_.varSet
Tactic:
simp only [varSet]
Proof state after:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v (phi.imp_ psi) ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ (phi.imp_ psi).varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ (phi.imp_ psi).varSet
Tactic:
simp only [varSet]
Proof state after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
Tactic:
simp
Proof state after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet
Tactic:
congr!
Proof state after:
no goals
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v (forall_ a✝ phi) ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ (forall_ a✝ phi).varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ (forall_ a✝ phi).varSet
Tactic:
simp only [varSet]
Proof state after:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Theorem: LN.occursIn_iff_mem_varSet
Proof state before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
F : Formula
⊢ occursIn v F ∧ v.isFree ↔ v ∈ F.freeVarSet
Tactic:
induction F
Proof state after:
case pred_
v : Var
a✝¹ : String
a✝ : List Var
⊢ occursIn v (pred_ a✝¹ a✝) ∧ v.isFree ↔ v ∈ (pred_ a✝¹ a✝).freeVarSet

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isFree ↔ v ∈ a✝.freeVarSet
⊢ occursIn v a✝.not_ ∧ v.isFree ↔ v ∈ a✝.not_.freeVarSet

case imp_
v : Var
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ∧ v.isFree ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : occursIn v a✝ ∧ v.isFree ↔ v ∈ a✝.freeVarSet
⊢ occursIn v (a✝¹.imp_ a✝) ∧ v.isFree ↔ v ∈ (a✝¹.imp_ a✝).freeVarSet

case forall_
v : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isFree ↔ v ∈ a✝.freeVarSet
⊢ occursIn v (forall_ a✝¹ a✝) ∧ v.isFree ↔ v ∈ (forall_ a✝¹ a✝).freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi.not_ ∧ v.isFree ↔ v ∈ phi.not_.freeVarSet
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.freeVarSet]
  simp only [occursIn]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ (phi.imp_ psi).freeVarSet
Tactic:
case imp_ phi psi phi_ih psi_ih =>
  simp only [Formula.freeVarSet]
  simp only [occursIn]
  simp
  tauto
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v (forall_ a✝ phi) ∧ v.isFree ↔ v ∈ (forall_ a✝ phi).freeVarSet
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Formula.freeVarSet]
  simp only [occursIn]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ (pred_ X vs).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet
Tactic:
simp
Proof state after:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ ∃ a ∈ vs, v ∈ a.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree ↔ ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
constructor
Proof state after:
case mp
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree → ∃ a ∈ vs, v ∈ a.freeVarSet

case mpr
v : Var
X : String
vs : List Var
⊢ (∃ a ∈ vs, v ∈ a.freeVarSet) → v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mp
v : Var
X : String
vs : List Var
⊢ v ∈ vs ∧ v.isFree → ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
intro a1
Proof state after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ ∃ a ∈ vs, v ∈ a.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ ∃ a ∈ vs, v ∈ a.freeVarSet
Tactic:
apply Exists.intro v
Proof state after:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ v ∈ vs ∧ v ∈ v.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isFree
⊢ v ∈ vs ∧ v ∈ v.freeVarSet
Tactic:
cases v
Proof state after:
case mp.free_
X : String
vs : List Var
a✝ : String
a1 : free_ a✝ ∈ vs ∧ (free_ a✝).isFree
⊢ free_ a✝ ∈ vs ∧ free_ a✝ ∈ (free_ a✝).freeVarSet

case mp.bound_
X : String
vs : List Var
a✝ : ℕ
a1 : bound_ a✝ ∈ vs ∧ (bound_ a✝).isFree
⊢ bound_ a✝ ∈ vs ∧ bound_ a✝ ∈ (bound_ a✝).freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
Tactic:
case _ x =>
  simp only [Var.freeVarSet]
  simp
  cases a1
  case _ a1_left a1_right =>
    exact a1_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
case _ i =>
  simp only [isFree] at a1
  cases a1
  case _ a1_left a1_right =>
    contradiction
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
Tactic:
simp only [Var.freeVarSet]
Proof state after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ {free_ x}
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ {free_ x}
Tactic:
simp
Proof state after:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
cases a1
Proof state after:
case intro
X : String
vs : List Var
x : String
left✝ : free_ x ∈ vs
right✝ : (free_ x).isFree
⊢ free_ x ∈ vs
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1_left : free_ x ∈ vs
a1_right : (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
case _ a1_left a1_right =>
  exact a1_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a1_left : free_ x ∈ vs
a1_right : (free_ x).isFree
⊢ free_ x ∈ vs
Tactic:
exact a1_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
simp only [isFree] at a1
Proof state after:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
cases a1
Proof state after:
case intro
X : String
vs : List Var
i : ℕ
left✝ : bound_ i ∈ vs
right✝ : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1_left : bound_ i ∈ vs
a1_right : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
case _ a1_left a1_right =>
  contradiction
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
i : ℕ
a1_left : bound_ i ∈ vs
a1_right : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
Tactic:
contradiction
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mpr
v : Var
X : String
vs : List Var
⊢ (∃ a ∈ vs, v ∈ a.freeVarSet) → v ∈ vs ∧ v.isFree
Tactic:
intro a1
Proof state after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
apply Exists.elim a1
Proof state after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.freeVarSet → v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.freeVarSet → v ∈ vs ∧ v.isFree
Tactic:
intro u a2
Proof state after:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
u : Var
a2 : u ∈ vs ∧ v ∈ u.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
u : Var
a2 : u ∈ vs ∧ v ∈ u.freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
cases u
Proof state after:
case mpr.free_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : String
a2 : free_ a✝ ∈ vs ∧ v ∈ (free_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree

case mpr.bound_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : ℕ
a2 : bound_ a✝ ∈ vs ∧ v ∈ (bound_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ x =>
  simp only [Var.freeVarSet] at a2
  simp at a2
  cases a2
  case _ a2_left a2_right =>
    subst a2_right
    simp only [isFree]
    simp
    exact a2_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ (bound_ i).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ i =>
  simp only [Var.freeVarSet] at a2
  simp at a2
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp only [Var.freeVarSet] at a2
Proof state after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ {free_ x}
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ {free_ x}
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp at a2
Proof state after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v = free_ x
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
cases a2
Proof state after:
case intro
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
left✝ : free_ x ∈ vs
right✝ : v = free_ x
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
case _ a2_left a2_right =>
  subst a2_right
  simp only [isFree]
  simp
  exact a2_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
Tactic:
subst a2_right
Proof state after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ (free_ x).isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ (free_ x).isFree
Tactic:
simp only [isFree]
Proof state after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ True
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ True
Tactic:
simp
Proof state after:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs
Tactic:
exact a2_left
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ (bound_ i).freeVarSet
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp only [Var.freeVarSet] at a2
Proof state after:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isFree
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isFree
Tactic:
simp at a2
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi.not_ ∧ v.isFree ↔ v ∈ phi.not_.freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi.not_ ∧ v.isFree ↔ v ∈ phi.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi.not_ ∧ v.isFree ↔ v ∈ phi.freeVarSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ (phi.imp_ psi).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Theorem: LN.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Tactic:
simp only [occursIn]
Proof state after:
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet