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

State before:
v : Var
σ : String → String
j : ℕ
z : String
h1 : σ z = z
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) v) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) v)
Tactic:
cases v
State after:
case free_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ a✝))

case bound_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ a✝))

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ x)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Tactic:
case free_ x =>
  conv =>
    lhs
    simp only [Var.open]
    simp only [Var.substFun]
    simp only [str_fun_to_var_fun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ free_ (σ x) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ i)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case bound_ i =>
  conv =>
    lhs
    simp only [Var.open]
  split_ifs
  case pos c1 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_pos c1]
  case pos c1 c2 =>
    simp only [Var.substFun]
    simp only [str_fun_to_var_fun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_pos c2]
    simp only [h1]
  case neg c1 c2 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_neg c2]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ x)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Tactic:
conv =>
  lhs
  simp only [Var.open]
  simp only [Var.substFun]
  simp only [str_fun_to_var_fun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ free_ (σ x) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ i)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
conv =>
  lhs
  simp only [Var.open]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
split_ifs
State after:
case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝ : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

case neg
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case pos c1 =>
  simp only [Var.substFun]
  simp only [Var.open]
  simp only [if_pos c1]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case pos c1 c2 =>
  simp only [Var.substFun]
  simp only [str_fun_to_var_fun]
  simp only [Var.open]
  simp only [if_neg c1]
  simp only [if_pos c2]
  simp only [h1]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case neg c1 c2 =>
  simp only [Var.substFun]
  simp only [Var.open]
  simp only [if_neg c1]
  simp only [if_neg c2]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = Var.open j (free_ z) (bound_ i)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_pos c1]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ str_fun_to_var_fun σ (free_ z) = Var.open j (free_ z) (bound_ i)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ str_fun_to_var_fun σ (free_ z) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [str_fun_to_var_fun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = Var.open j (free_ z) (bound_ i)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c1]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i = j then free_ z else bound_ (i - 1)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_pos c2]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = free_ z

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = free_ z
Tactic:
simp only [h1]
State after:
no goals

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = Var.open j (free_ z) (bound_ i)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c1]
State after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i = j then free_ z else bound_ (i - 1)

State before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c2]
State after:
no goals