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

State before:
z : String
t v : Var
⊢ v.freeVarSet \ {free_ z} ⊆ ((free_ z).subst t v).freeVarSet
Tactic:
cases v
State after:
case free_
z : String
t : Var
a✝ : String
⊢ (free_ a✝).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ a✝)).freeVarSet

case bound_
z : String
t : Var
a✝ : ℕ
⊢ (bound_ a✝).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (bound_ a✝)).freeVarSet

State before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
Tactic:
case free_ x =>
  simp only [Var.subst]
  split_ifs
  case pos c1 =>
    simp only [c1]
    conv =>
      lhs
      simp only [Var.freeVarSet]
    simp
  case neg c1 =>
    simp only [Var.freeVarSet]
    exact Finset.sdiff_subset {free_ x} {free_ z}
State after:
no goals

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

State before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
Tactic:
simp only [Var.subst]
State after:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (if free_ z = free_ x then t else free_ x).freeVarSet

State before:
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (if free_ z = free_ x then t else free_ x).freeVarSet
Tactic:
split_ifs
State after:
case pos
z : String
t : Var
x : String
h✝ : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet

case neg
z : String
t : Var
x : String
h✝ : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet

State before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet
Tactic:
case pos c1 =>
  simp only [c1]
  conv =>
    lhs
    simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet
Tactic:
case neg c1 =>
  simp only [Var.freeVarSet]
  exact Finset.sdiff_subset {free_ x} {free_ z}
State after:
no goals

State before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ t.freeVarSet
Tactic:
simp only [c1]
State after:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ x} ⊆ t.freeVarSet

State before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ x} ⊆ t.freeVarSet
Tactic:
conv =>
  lhs
  simp only [Var.freeVarSet]
State after:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ {free_ x} \ {free_ x} ⊆ t.freeVarSet

State before:
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ {free_ x} \ {free_ x} ⊆ t.freeVarSet
Tactic:
simp
State after:
no goals

State before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (free_ x).freeVarSet
Tactic:
simp only [Var.freeVarSet]
State after:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} ⊆ {free_ x}

State before:
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
⊢ {free_ x} \ {free_ z} ⊆ {free_ x}
Tactic:
exact Finset.sdiff_subset {free_ x} {free_ z}
State after:
no goals

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