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

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

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

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

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

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

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

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

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

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

State before:
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}
Tactic:
simp only [Var.freeVarSet]
State after:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {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}

State before:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {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}
Tactic:
simp
State after:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ ¬z = 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}

State before:
case s1
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ ¬z = 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}
Tactic:
simp at c1
State after:
case s1
z : String
t : Var
x : String
c1 : ¬z = x
⊢ ¬z = 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}

State before:
case s1
z : String
t : Var
x : String
c1 : ¬z = x
⊢ ¬z = 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}
Tactic:
exact c1
State after:
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}

State before:
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}
Tactic:
simp only [s1]
State after:
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}

State before:
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}
Tactic:
apply Finset.subset_union_right
State after:
no goals

State before:
z : String
t : Var
i : ℕ
⊢ ((free_ z).subst t (bound_ i)).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.subst]
State after:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}

State before:
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
conv =>
  lhs
  simp only [Var.freeVarSet]
State after:
z : String
t : Var
i : ℕ
⊢ ∅ ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}

State before:
z : String
t : Var
i : ℕ
⊢ ∅ ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp
State after:
no goals