internlm/Lean-Github huggingface dataset:
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ∪ psi.freeVarSet ⊆
    (Formula.open j (free_ z) phi).freeVarSet ∪ (Formula.open j (free_ z) psi).freeVarSet
Tactic:
apply Finset.union_subset_left_right
Proof state after:
case h1
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet

case h2
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
case h1
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
Tactic:
exact phi_ih j
Proof state after:
no goals
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
case h2
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
Tactic:
exact psi_ih j
Proof state after:
no goals
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ (forall_ x phi).freeVarSet ⊆ (Formula.open j (free_ z) (forall_ x phi)).freeVarSet
Tactic:
simp only [Formula.open]
Proof state after:
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ (forall_ x phi).freeVarSet ⊆ (forall_ x (Formula.open (j + 1) (free_ z) phi)).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ (forall_ x phi).freeVarSet ⊆ (forall_ x (Formula.open (j + 1) (free_ z) phi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open (j + 1) (free_ z) phi).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z x : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open (j + 1) (free_ z) phi).freeVarSet
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
v : Var
⊢ (Var.close j (free_ z) v).freeVarSet ⊆ v.freeVarSet \ {free_ z}
Tactic:
cases v
Proof state after:
case free_
j : ℕ
z a✝ : String
⊢ (Var.close j (free_ z) (free_ a✝)).freeVarSet ⊆ (free_ a✝).freeVarSet \ {free_ z}

case bound_
j : ℕ
z : String
a✝ : ℕ
⊢ (Var.close j (free_ z) (bound_ a✝)).freeVarSet ⊆ (bound_ a✝).freeVarSet \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (Var.close j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case free_ x =>
  simp only [Var.close]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
    simp at c1
    exact c1
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (Var.close j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case bound_ i =>
  simp only [Var.close]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (Var.close j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [Var.close]
Proof state after:
j : ℕ
z x : String
⊢ (if free_ x = free_ z then bound_ j else free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
⊢ (if free_ x = free_ z then bound_ j else free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
split_ifs
Proof state after:
case pos
j : ℕ
z x : String
h✝ : free_ x = free_ z
⊢ (bound_ j).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}

case neg
j : ℕ
z x : String
h✝ : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ (bound_ j).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
  simp at c1
  exact c1
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ (bound_ j).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ ∅ ⊆ {free_ x} \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ ∅ ⊆ {free_ x} \ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ {free_ x} ⊆ {free_ x} \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ {free_ x} ⊆ {free_ x} \ {free_ z}
Tactic:
simp
Proof state after:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ ¬x = z
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ ¬x = z
Tactic:
simp at c1
Proof state after:
j : ℕ
z x : String
c1 : ¬x = z
⊢ ¬x = z
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z x : String
c1 : ¬x = z
⊢ ¬x = z
Tactic:
exact c1
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (Var.close j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.close]
Proof state after:
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
split_ifs
Proof state after:
case pos
j : ℕ
z : String
i : ℕ
h✝ : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}

case neg
j : ℕ
z : String
i : ℕ
h✝ : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Theorem: LN.VarCloseFreeVarSet
Proof state before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
j : ℕ
z : String
F : Formula
⊢ (Formula.close j (free_ z) F).freeVarSet ⊆ F.freeVarSet \ {free_ z}
Tactic:
induction F generalizing j
Proof state after:
case pred_
z a✝¹ : String
a✝ : List Var
j : ℕ
⊢ (Formula.close j (free_ z) (pred_ a✝¹ a✝)).freeVarSet ⊆ (pred_ a✝¹ a✝).freeVarSet \ {free_ z}

case not_
z : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.close j (free_ z) a✝).freeVarSet ⊆ a✝.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) a✝.not_).freeVarSet ⊆ a✝.not_.freeVarSet \ {free_ z}

case imp_
z : String
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (j : ℕ), (Formula.close j (free_ z) a✝¹).freeVarSet ⊆ a✝¹.freeVarSet \ {free_ z}
a_ih✝ : ∀ (j : ℕ), (Formula.close j (free_ z) a✝).freeVarSet ⊆ a✝.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) (a✝¹.imp_ a✝)).freeVarSet ⊆ (a✝¹.imp_ a✝).freeVarSet \ {free_ z}

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

z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.close j (free_ z) v).freeVarSet ⊆ v.freeVarSet \ {free_ z}
Tactic:
exact VarCloseFreeVarSet j z v
Proof state after:
no goals
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case hst
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet

case hvu
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ {free_ z} ⊆ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
case hst
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet
Tactic:
apply Finset.subset_biUnion_of_mem
Proof state after:
case hst.xs
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
case hst.xs
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset
Tactic:
simp
Proof state after:
case hst.xs
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
case hst.xs
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs
Tactic:
exact a1
Proof state after:
no goals
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
case hvu
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ {free_ z} ⊆ {free_ z}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi.not_).freeVarSet ⊆ phi.not_.freeVarSet \ {free_ z}
Tactic:
simp only [Formula.close]
Proof state after:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).not_.freeVarSet ⊆ phi.not_.freeVarSet \ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).not_.freeVarSet ⊆ phi.not_.freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) (phi.imp_ psi)).freeVarSet ⊆ (phi.imp_ psi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.close]
Proof state after:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ ((Formula.close j (free_ z) phi).imp_ (Formula.close j (free_ z) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet \ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ ((Formula.close j (free_ z) phi).imp_ (Formula.close j (free_ z) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet \ {free_ z}
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ∪ (Formula.close j (free_ z) psi).freeVarSet ⊆
    (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}
Theorem: LN.FormulaCloseFreeVarSet
Proof state before:
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ∪ (Formula.close j (free_ z) psi).freeVarSet ⊆
    (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z}
Tactic:
apply Finset.union_subset_diff
Proof state after:
case h1
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
psi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) psi).freeVarSet ⊆ psi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}

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

case bound_
z : String
t : Var
a✝ : ℕ
⊢ ((free_ z).subst t (bound_ a✝)).freeVarSet ⊆ t.freeVarSet ∪ (bound_ a✝).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
⊢ ((free_ z).subst t (free_ x)).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
case free_ x =>
  simp only [Var.subst]
  split_ifs
  case pos c1 =>
    apply Finset.subset_union_left
  case neg c1 =>
    have s1 : Var.freeVarSet (free_ x) \ {free_ z} = {free_ x}
    simp only [Var.freeVarSet]
    simp
    simp at c1
    exact c1
    simp only [s1]
    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:
case bound_ i =>
  simp only [Var.subst]
  conv =>
    lhs
    simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
⊢ ((free_ z).subst t (free_ x)).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
simp only [Var.subst]
Proof state after:
z : String
t : Var
x : String
⊢ (if free_ z = free_ x then t else free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
⊢ (if free_ z = free_ x then t else free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
split_ifs
Proof state after:
case pos
z : String
t : Var
x : String
h✝ : free_ z = free_ x
⊢ t.freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}

case neg
z : String
t : Var
x : String
h✝ : ¬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
⊢ t.freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
case pos c1 =>
  apply Finset.subset_union_left
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 ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
case neg c1 =>
  have s1 : Var.freeVarSet (free_ x) \ {free_ z} = {free_ x}
  simp only [Var.freeVarSet]
  simp
  simp at c1
  exact c1
  simp only [s1]
  apply Finset.subset_union_right
Proof state after:
no goals
Theorem: LN.VarSubstFreeVarSet
Proof state before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ t.freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
apply Finset.subset_union_left
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 ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
Tactic:
have s1 : Var.freeVarSet (free_ x) \ {free_ z} = {free_ x}
Proof state after:
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}