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

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

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

State before:
j : ℕ
z x : String
⊢ (Var.close j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case free_ x =>
  simp only [Var.close]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
    simp at c1
    exact c1
State after:
no goals

State before:
j : ℕ
z : String
i : ℕ
⊢ (Var.close j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case bound_ i =>
  simp only [Var.close]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
State after:
no goals

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

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

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

State before:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ (bound_ j).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
  simp at c1
  exact c1
State after:
no goals

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

State before:
j : ℕ
z x : String
c1 : free_ x = free_ z
⊢ ∅ ⊆ {free_ x} \ {free_ z}
Tactic:
simp
State after:
no goals

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

State before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ {free_ x} ⊆ {free_ x} \ {free_ z}
Tactic:
simp
State after:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ ¬x = z

State before:
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ ¬x = z
Tactic:
simp at c1
State after:
j : ℕ
z x : String
c1 : ¬x = z
⊢ ¬x = z

State before:
j : ℕ
z x : String
c1 : ¬x = z
⊢ ¬x = z
Tactic:
exact c1
State after:
no goals

State before:
j : ℕ
z : String
i : ℕ
⊢ (Var.close j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.close]
State after:
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}

State before:
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
split_ifs
State after:
case pos
j : ℕ
z : String
i : ℕ
h✝ : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}

case neg
j : ℕ
z : String
i : ℕ
h✝ : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}

State before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
case _ c1 =>
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ \ {free_ z}

State before:
j : ℕ
z : String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Tactic:
simp
State after:
no goals

State before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ ∅ ⊆ ∅ \ {free_ z}

State before:
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
⊢ ∅ ⊆ ∅ \ {free_ z}
Tactic:
simp
State after:
no goals