internlm/Lean-Github huggingface dataset:
Theorem: LN.VarSubstFreeVarSet
Proof state before:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} = {free_ x}

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} = {free_ x}

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} = {free_ x}

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp
Proof state after:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ ¬z = x

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ ¬z = x

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp at c1
Proof state after:
case s1
z : String
t : Var
x : String
c1 : ¬z = x
⊢ ¬z = x

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
case s1
z : String
t : Var
x : String
c1 : ¬z = x
⊢ ¬z = x

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
exact c1
Proof state after:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [s1]
Proof state after:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ {free_ x}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ {free_ x}
Tactic:
apply Finset.subset_union_right
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
i : ℕ
⊢ ((free_ z).subst t (bound_ i)).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.subst]
Proof state after:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
conv =>
  lhs
  simp only [Var.freeVarSet]
Proof state after:
z : String
t : Var
i : ℕ
⊢ ∅ ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
i : ℕ
⊢ ∅ ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
F : Formula
⊢ (Formula.subst (free_ z) t F).freeVarSet ⊆ t.freeVarSet ∪ F.freeVarSet \ {free_ z}
Tactic:
induction F
Proof state after:
case pred_
z : String
t : Var
a✝¹ : String
a✝ : List Var
⊢ (Formula.subst (free_ z) t (pred_ a✝¹ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ a✝¹ a✝).freeVarSet \ {free_ z}

case not_
z : String
t : Var
a✝ : Formula
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t a✝.not_).freeVarSet ⊆ t.freeVarSet ∪ a✝.not_.freeVarSet \ {free_ z}

case imp_
z : String
t : Var
a✝¹ a✝ : Formula
a_ih✝¹ : (Formula.subst (free_ z) t a✝¹).freeVarSet ⊆ t.freeVarSet ∪ a✝¹.freeVarSet \ {free_ z}
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (a✝¹.imp_ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (a✝¹.imp_ a✝).freeVarSet \ {free_ z}

case forall_
z : String
t : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : (Formula.subst (free_ z) t a✝).freeVarSet ⊆ t.freeVarSet ∪ a✝.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (forall_ a✝¹ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ a✝¹ a✝).freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi.not_).freeVarSet ⊆ t.freeVarSet ∪ phi.not_.freeVarSet \ {free_ z}
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (forall_ x phi)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ x phi).freeVarSet \ {free_ z}
Tactic:
case forall_ x phi phi_ih =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (Formula.subst (free_ z) t (pred_ X vs)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ X vs).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X (List.map ((free_ z).subst t) vs)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ X vs).freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X (List.map ((free_ z).subst t) vs)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ X vs).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
X : String
vs : List Var
⊢ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet ⊆
    t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet ⊆
    t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
simp
Proof state after:
z : String
t : Var
X : String
vs : List Var
⊢ ∀ a ∈ vs, ((free_ z).subst t a).freeVarSet ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ ∀ a ∈ vs, ((free_ z).subst t a).freeVarSet ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
intro v a1
Proof state after:
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
trans Var.freeVarSet t ∪ Var.freeVarSet v \ {free_ z}
Proof state after:
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ v.freeVarSet \ {free_ z}

z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ t.freeVarSet ∪ v.freeVarSet \ {free_ z} ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ v.freeVarSet \ {free_ z}
Tactic:
exact VarSubstFreeVarSet z t v
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ t.freeVarSet ∪ v.freeVarSet \ {free_ z} ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
apply Finset.union_subset_union_right
Proof state after:
case h
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
simp only [← List.mem_toFinset] at a1
Proof state after:
case h
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case h.hst
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet

case h.hvu
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ {free_ z} ⊆ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h.hst
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet
Tactic:
apply Finset.subset_biUnion_of_mem Var.freeVarSet a1
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h.hvu
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ {free_ z} ⊆ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi.not_).freeVarSet ⊆ t.freeVarSet ∪ phi.not_.freeVarSet \ {free_ z}
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).not_.freeVarSet ⊆ t.freeVarSet ∪ phi.not_.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).not_.freeVarSet ⊆ t.freeVarSet ∪ phi.not_.freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (phi.imp_ psi)).freeVarSet ⊆ t.freeVarSet ∪ (phi.imp_ psi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet ⊆
    t.freeVarSet ∪ (phi.imp_ psi).freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet ⊆
    t.freeVarSet ∪ (phi.imp_ psi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet ⊆
    t.freeVarSet ∪ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet ⊆
    t.freeVarSet ∪ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}
Tactic:
apply Finset.union_subset_left_right_diff
Proof state after:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}

case h2
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
case h2
z : String
t : Var
phi psi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
psi_ih : (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t psi).freeVarSet ⊆ t.freeVarSet ∪ psi.freeVarSet \ {free_ z}
Tactic:
exact psi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t (forall_ x phi)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ x phi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ x phi).freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet ⊆ t.freeVarSet ∪ (forall_ x phi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
Theorem: LN.FormulaSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
⊢ (Formula.subst (free_ z) t phi).freeVarSet ⊆ t.freeVarSet ∪ phi.freeVarSet \ {free_ z}
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t v : Var
⊢ v.freeVarSet \ {free_ z} ⊆ ((free_ z).subst t v).freeVarSet
Tactic:
cases v
Proof state after:
case free_
z : String
t : Var
a✝ : String
⊢ (free_ a✝).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ a✝)).freeVarSet

case bound_
z : String
t : Var
a✝ : ℕ
⊢ (bound_ a✝).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (bound_ a✝)).freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
Tactic:
case free_ x =>
  simp only [Var.subst]
  split_ifs
  case pos c1 =>
    simp only [c1]
    conv =>
      lhs
      simp only [Var.freeVarSet]
    simp
  case neg c1 =>
    simp only [Var.freeVarSet]
    exact Finset.sdiff_subset {free_ x} {free_ z}
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (bound_ i)).freeVarSet
Tactic:
case bound_ i =>
  conv =>
    lhs
    simp only [Var.freeVarSet]
Proof state after:
z : String
t : Var
i : ℕ
⊢ ∅ \ {free_ z} ⊆ ((free_ z).subst t (bound_ i)).freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
Tactic:
simp only [Var.subst]
Proof state after:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (if free_ z = free_ x then t else free_ x).freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (if free_ z = free_ x then t else free_ x).freeVarSet
Tactic:
split_ifs
Proof state after:
case pos
z : String
t : Var
x : String
h✝ : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet

case neg
z : String
t : Var
x : String
h✝ : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet
Tactic:
case pos c1 =>
  simp only [c1]
  conv =>
    lhs
    simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet
Tactic:
case neg c1 =>
  simp only [Var.freeVarSet]
  exact Finset.sdiff_subset {free_ x} {free_ z}
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet
Tactic:
simp only [c1]
Proof state after:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ x} ⊆ t.freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ x} ⊆ t.freeVarSet
Tactic:
conv =>
  lhs
  simp only [Var.freeVarSet]
Proof state after:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ {free_ x} \ {free_ x} ⊆ t.freeVarSet
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ {free_ x} \ {free_ x} ⊆ t.freeVarSet
Tactic:
simp
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet
Tactic:
simp only [Var.freeVarSet]
Proof state after:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} ⊆ {free_ x}
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} ⊆ {free_ x}
Tactic:
exact Finset.sdiff_subset {free_ x} {free_ z}
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet'
Proof state before:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (bound_ i)).freeVarSet
Tactic:
conv =>
  lhs
  simp only [Var.freeVarSet]
Proof state after:
z : String
t : Var
i : ℕ
⊢ ∅ \ {free_ z} ⊆ ((free_ z).subst t (bound_ i)).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
F : Formula
⊢ F.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t F).freeVarSet
Tactic:
induction F
Proof state after:
case pred_
z : String
t : Var
a✝¹ : String
a✝ : List Var
⊢ (pred_ a✝¹ a✝).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (pred_ a✝¹ a✝)).freeVarSet

case not_
z : String
t : Var
a✝ : Formula
a_ih✝ : a✝.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t a✝).freeVarSet
⊢ a✝.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t a✝.not_).freeVarSet

case imp_
z : String
t : Var
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t a✝¹).freeVarSet
a_ih✝ : a✝.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t a✝).freeVarSet
⊢ (a✝¹.imp_ a✝).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (a✝¹.imp_ a✝)).freeVarSet

case forall_
z : String
t : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : a✝.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t a✝).freeVarSet
⊢ (forall_ a✝¹ a✝).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (forall_ a✝¹ a✝)).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X vs).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (pred_ X vs)).freeVarSet
Tactic:
case pred_ X vs =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  induction vs
  case nil =>
    simp
  case cons hd tl ih =>
    simp
    have s1 : (Var.freeVarSet hd ∪ Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z} = (Var.freeVarSet hd \ {free_ z}) ∪ ((Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z})
    exact Finset.union_sdiff_distrib (Var.freeVarSet hd) (Finset.biUnion (List.toFinset tl) Var.freeVarSet) {free_ z}
    simp only [s1]
    exact Finset.union_subset_union (VarSubstFreeVarSet' z t hd) ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi.not_).freeVarSet
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ (forall_ x phi).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (forall_ x phi)).freeVarSet
Tactic:
case forall_ x phi phi_ih =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X vs).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (pred_ X vs)).freeVarSet
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X vs).freeVarSet \ {free_ z} ⊆ (pred_ X (List.map ((free_ z).subst t) vs)).freeVarSet