internlm/Lean-Github huggingface dataset:
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (pred_ X vs)).freeVarSet ⊆
    (pred_ X vs).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)).freeVarSet ⊆
    (pred_ X vs).freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)).freeVarSet ⊆
    (pred_ X vs).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (List.map (Var.openList j (List.map free_ zs)) vs).toFinset.biUnion Var.freeVarSet ⊆
    vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (List.map (Var.openList j (List.map free_ zs)) vs).toFinset.biUnion Var.freeVarSet ⊆
    vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ ∀ a ∈ vs,
    (Var.openList j (List.map free_ zs) a).freeVarSet ⊆
      vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
⊢ ∀ a ∈ vs,
    (Var.openList j (List.map free_ zs) a).freeVarSet ⊆
      vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
intro v a1
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
trans v.freeVarSet ∪ (zs.map free_).toFinset
Proof state after:
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ v.freeVarSet ∪ (List.map free_ zs).toFinset

zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ∪ (List.map free_ zs).toFinset ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ v.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
exact VarOpenListFreeVarSet j zs v
Proof state after:
no goals
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ∪ (List.map free_ zs).toFinset ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
apply Finset.union_subset_union_left
Proof state after:
case h
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
case h
zs : List String
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 h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset
Tactic:
simp
Proof state after:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs
Tactic:
exact a1
Proof state after:
no goals
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi.not_).freeVarSet ⊆ phi.not_.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).not_.freeVarSet ⊆ phi.not_.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).not_.freeVarSet ⊆ phi.not_.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (phi.imp_ psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ∪ (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆
    phi.freeVarSet ∪ psi.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ∪ (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆
    phi.freeVarSet ∪ psi.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
apply Finset.union_subset_union_left_right
Proof state after:
case h1
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset

case h2
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
case h1
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
exact phi_ih j
Proof state after:
no goals
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
case h2
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
exact psi_ih j
Proof state after:
no goals
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (forall_ x phi)).freeVarSet ⊆
    (forall_ x phi).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.openList]
Proof state after:
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (forall_ x (Formula.openList (j + 1) (List.map free_ zs) phi)).freeVarSet ⊆
    (forall_ x phi).freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (forall_ x (Formula.openList (j + 1) (List.map free_ zs) phi)).freeVarSet ⊆
    (forall_ x phi).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList (j + 1) (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
Theorem: LN.FormulaOpenListFreeVarSet
Proof state before:
zs : List String
x : String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList (j + 1) (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z : String
v : Var
⊢ v.freeVarSet ⊆ (Var.open j (free_ z) v).freeVarSet
Tactic:
cases v
Proof state after:
case free_
j : ℕ
z a✝ : String
⊢ (free_ a✝).freeVarSet ⊆ (Var.open j (free_ z) (free_ a✝)).freeVarSet

case bound_
j : ℕ
z : String
a✝ : ℕ
⊢ (bound_ a✝).freeVarSet ⊆ (Var.open j (free_ z) (bound_ a✝)).freeVarSet
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (Var.open j (free_ z) (free_ x)).freeVarSet
Tactic:
case free_ x =>
  simp only [Var.open]
  simp only [Var.freeVarSet]
  simp
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ (Var.open j (free_ z) (bound_ i)).freeVarSet
Tactic:
case bound_ i =>
  simp only [Var.open]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 c2 =>
    simp only [Var.freeVarSet]
    simp
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (Var.open j (free_ z) (free_ x)).freeVarSet
Tactic:
simp only [Var.open]
Proof state after:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet
Tactic:
simp only [Var.freeVarSet]
Proof state after:
j : ℕ
z x : String
⊢ {free_ x} ⊆ {free_ x}
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z x : String
⊢ {free_ x} ⊆ {free_ x}
Tactic:
simp
Proof state after:
no goals
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ (Var.open j (free_ z) (bound_ i)).freeVarSet
Tactic:
simp only [Var.open]
Proof state after:
j : ℕ
z : String
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)).freeVarSet
Theorem: LN.VarOpenFreeVarSet'
Proof state before:
j : ℕ
z : String
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)).freeVarSet
Tactic:
split_ifs
Proof state after:
case pos
j : ℕ
z : String
i : ℕ
h✝ : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet

case pos
j : ℕ
z : String
i : ℕ
h✝¹ : ¬i < j
h✝ : i = j
⊢ (bound_ i).freeVarSet ⊆ (free_ z).freeVarSet

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

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

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

case forall_
z a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), a✝.freeVarSet ⊆ (Formula.open j (free_ z) a✝).freeVarSet
j : ℕ
⊢ (forall_ a✝¹ a✝).freeVarSet ⊆ (Formula.open j (free_ z) (forall_ a✝¹ a✝)).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.not_.freeVarSet ⊆ (Formula.open j (free_ z) phi.not_).freeVarSet
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.open]
  simp only [Formula.freeVarSet]
  apply phi_ih
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:
case forall_ x phi phi_ih =>
  simp only [Formula.open]
  simp only [Formula.freeVarSet]
  apply phi_ih
Proof state after:
no goals
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
⊢ (pred_ X vs).freeVarSet ⊆ (Formula.open j (free_ z) (pred_ X vs)).freeVarSet
Tactic:
simp only [Formula.open]
Proof state after:
z X : String
vs : List Var
j : ℕ
⊢ (pred_ X vs).freeVarSet ⊆ (pred_ X (List.map (Var.open j (free_ z)) vs)).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
⊢ (pred_ X vs).freeVarSet ⊆ (pred_ X (List.map (Var.open j (free_ z)) vs)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z X : String
vs : List Var
j : ℕ
⊢ vs.toFinset.biUnion Var.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
⊢ vs.toFinset.biUnion Var.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Tactic:
simp
Proof state after:
z X : String
vs : List Var
j : ℕ
⊢ ∀ x ∈ vs, x.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
⊢ ∀ x ∈ vs, x.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Tactic:
intro v a1
Proof state after:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Tactic:
trans Var.freeVarSet (Var.open j (free_ z) v)
Proof state after:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ (Var.open j (free_ z) v).freeVarSet

z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.open j (free_ z) v).freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ (Var.open j (free_ z) v).freeVarSet
Tactic:
apply VarOpenFreeVarSet'
Proof state after:
no goals
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.open j (free_ z) v).freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
Tactic:
apply Finset.subset_biUnion_of_mem Var.freeVarSet
Proof state after:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ Var.open j (free_ z) v ∈ (List.map (Var.open j (free_ z)) vs).toFinset
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ Var.open j (free_ z) v ∈ (List.map (Var.open j (free_ z)) vs).toFinset
Tactic:
apply List.mem_toFinset.mpr
Proof state after:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ Var.open j (free_ z) v ∈ List.map (Var.open j (free_ z)) vs
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ Var.open j (free_ z) v ∈ List.map (Var.open j (free_ z)) vs
Tactic:
exact List.mem_map_of_mem (Var.open j (free_ z)) a1
Proof state after:
no goals
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.not_.freeVarSet ⊆ (Formula.open j (free_ z) phi.not_).freeVarSet
Tactic:
simp only [Formula.open]
Proof state after:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.not_.freeVarSet ⊆ (Formula.open j (free_ z) phi).not_.freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.not_.freeVarSet ⊆ (Formula.open j (free_ z) phi).not_.freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
Theorem: LN.FormulaOpenFreeVarSet'
Proof state before:
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
j : ℕ
⊢ phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
Tactic:
apply phi_ih
Proof state after:
no goals
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.imp_ psi).freeVarSet ⊆ (Formula.open j (free_ z) (phi.imp_ psi)).freeVarSet
Tactic:
simp only [Formula.open]
Proof state after:
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.imp_ psi).freeVarSet ⊆ ((Formula.open j (free_ z) phi).imp_ (Formula.open j (free_ z) psi)).freeVarSet
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.imp_ psi).freeVarSet ⊆ ((Formula.open j (free_ z) phi).imp_ (Formula.open j (free_ z) psi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
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