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

State before:
j : ℕ
zs : List String
v : Var
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ v.freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
cases v
State after:
case free_
j : ℕ
zs : List String
a✝ : String
⊢ (Var.openList j (List.map free_ zs) (free_ a✝)).freeVarSet ⊆ (free_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

case bound_
j : ℕ
zs : List String
a✝ : ℕ
⊢ (Var.openList j (List.map free_ zs) (bound_ a✝)).freeVarSet ⊆ (bound_ a✝).freeVarSet ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
x : String
⊢ (Var.openList j (List.map free_ zs) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
case free_ x =>
  simp only [Var.openList]
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
⊢ (Var.openList j (List.map free_ zs) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
case bound_ i =>
  simp only [Var.openList]
  split_ifs
  case pos c1 =>
    simp only [Var.freeVarSet]
    simp
  case pos c1 c2 =>
    simp
    simp only [Var.freeVarSet]
    simp
    apply List.get_mem
  case neg c1 c2 =>
    simp only [Var.freeVarSet]
    simp
State after:
no goals

State before:
j : ℕ
zs : List String
x : String
⊢ (Var.openList j (List.map free_ zs) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.openList]
State after:
j : ℕ
zs : List String
x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
zs : List String
x : String
⊢ {free_ x} ⊆ {free_ x} ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
x : String
⊢ {free_ x} ⊆ {free_ x} ∪ (List.map free_ zs).toFinset
Tactic:
simp
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
⊢ (Var.openList j (List.map free_ zs) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.openList]
State after:
j : ℕ
zs : List String
i : ℕ
⊢ (if i < j then bound_ i
      else
        if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
        else bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆
    (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
⊢ (if i < j then bound_ i
      else
        if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
        else bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆
    (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
split_ifs
State after:
case pos
j : ℕ
zs : List String
i : ℕ
h✝ : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

case pos
j : ℕ
zs : List String
i : ℕ
h✝¹ : ¬i < j
h✝ : i - j < (List.map free_ zs).length
⊢ (List.map free_ zs)[i - j].freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

case neg
j : ℕ
zs : List String
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬i - j < (List.map free_ zs).length
⊢ (bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
case pos c1 =>
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (List.map free_ zs)[i - j].freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
case pos c1 c2 =>
  simp
  simp only [Var.freeVarSet]
  simp
  apply List.get_mem
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ (bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
case neg c1 c2 =>
  simp only [Var.freeVarSet]
  simp
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
c1 : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
zs : List String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
c1 : i < j
⊢ ∅ ⊆ ∅ ∪ (List.map free_ zs).toFinset
Tactic:
simp
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (List.map free_ zs)[i - j].freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp
State after:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (free_ (zs.get ⟨i - j, ⋯⟩)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (free_ (zs.get ⟨i - j, ⋯⟩)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ {free_ (zs.get ⟨i - j, ⋯⟩)} ⊆ ∅ ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ {free_ (zs.get ⟨i - j, ⋯⟩)} ⊆ ∅ ∪ (List.map free_ zs).toFinset
Tactic:
simp
State after:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ zs.get ⟨i - j, ⋯⟩ ∈ zs

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ zs.get ⟨i - j, ⋯⟩ ∈ zs
Tactic:
apply List.get_mem
State after:
no goals

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ (bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
Tactic:
simp only [Var.freeVarSet]
State after:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ ∅ ⊆ ∅ ∪ (List.map free_ zs).toFinset

State before:
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ ∅ ⊆ ∅ ∪ (List.map free_ zs).toFinset
Tactic:
simp
State after:
no goals