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

State before:
z : String
t : Var
F : Formula
⊢ (Formula.subst (free_ z) t F).freeVarSet ⊆ t.freeVarSet ∪ F.freeVarSet \ {free_ z}
Tactic:
induction F
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}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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