Theorem: LN.FormulaOpenListFreeVarSet (FOL/LN/Paper.lean)

State before:
j : ℕ
zs : List String
F : Formula
⊢ (Formula.openList j (List.map free_ zs) F).freeVarSet ⊆ F.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
induction F generalizing j
State after:
case pred_
zs : List String
a✝¹ : String
a✝ : List Var
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝)).freeVarSet ⊆
    (pred_ a✝¹ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case not_
zs : List String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) a✝.not_).freeVarSet ⊆ a✝.not_.freeVarSet ∪ (List.map free_ zs).toFinset

case imp_
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝¹).freeVarSet ⊆ a✝¹.freeVarSet ∪ (List.map free_ zs).toFinset
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝)).freeVarSet ⊆
    (a✝¹.imp_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case forall_
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) a✝).freeVarSet ⊆ a✝.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝)).freeVarSet ⊆
    (forall_ a✝¹ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

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:
case not_ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.freeVarSet]
  apply phi_ih
State after:
no goals

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:
case forall_ x phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.freeVarSet]
  apply phi_ih
State after:
no goals

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]
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

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]
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset

State before:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs.toFinset
Tactic:
simp
State after:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs

State before:
case h.xs
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v ∈ vs
Tactic:
exact a1
State after:
no goals

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]
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

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]
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

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
State after:
no goals

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]
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

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]
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

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
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

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
State after:
no goals

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
State after:
no goals

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]
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

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]
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

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
State after:
no goals