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

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

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

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

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

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

State before:
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
Tactic:
simp only [Formula.freeVarSet]
State after:
z : String
t : Var
X : String
vs : List Var
⊢ vs.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet

State before:
z : String
t : Var
X : String
vs : List Var
⊢ vs.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet
Tactic:
induction vs
State after:
case nil
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet

case cons
z : String
t : Var
X : String
head✝ : Var
tail✝ : List Var
tail_ih✝ :
  tail✝.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) tail✝).toFinset.biUnion Var.freeVarSet
⊢ (head✝ :: tail✝).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (head✝ :: tail✝)).toFinset.biUnion Var.freeVarSet

State before:
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet
Tactic:
case nil =>
  simp
State after:
no goals

State before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd :: tl).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (hd :: tl)).toFinset.biUnion Var.freeVarSet
Tactic:
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
State after:
no goals

State before:
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet
Tactic:
simp
State after:
no goals

State before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd :: tl).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (hd :: tl)).toFinset.biUnion Var.freeVarSet
Tactic:
simp
State after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet

State before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
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})
State after:
case s1
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}

z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet

State before:
case s1
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}

z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
exact Finset.union_sdiff_distrib (Var.freeVarSet hd) (Finset.biUnion (List.toFinset tl) Var.freeVarSet) {free_ z}
State after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet

State before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
simp only [s1]
State after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet

State before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
exact Finset.union_subset_union (VarSubstFreeVarSet' z t hd) ih
State after:
no goals

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:
simp only [Formula.subst]
State after:
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

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:
simp only [Formula.freeVarSet]
State after:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet

State before:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
exact phi_ih
State after:
no goals

State before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (phi.imp_ psi)).freeVarSet
Tactic:
simp only [Formula.subst]
State after:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆
    ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet

State before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆
    ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
State after:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z} ⊆
    (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet

State before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z} ⊆
    (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet
Tactic:
apply Finset.diff_union_subset
State after:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet

case h2
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet

State before:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
apply phi_ih
State after:
no goals

State before:
case h2
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
Tactic:
apply psi_ih
State after:
no goals

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:
simp only [Formula.subst]
State after:
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} ⊆ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet

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} ⊆ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
State after:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet

State before:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
exact phi_ih
State after:
no goals