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

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d
Tactic:
funext v
State after:
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ (shift D V d ∘ Var.close (j + 1) (free_ z)) v = shift D (V ∘ Var.close j (free_ z)) d v

State before:
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ (shift D V d ∘ Var.close (j + 1) (free_ z)) v = shift D (V ∘ Var.close j (free_ z)) d v
Tactic:
simp
State after:
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ shift D V d (Var.close (j + 1) (free_ z) v) = shift D (V ∘ Var.close j (free_ z)) d v

State before:
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ shift D V d (Var.close (j + 1) (free_ z) v) = shift D (V ∘ Var.close j (free_ z)) d v
Tactic:
cases v
State after:
case h.free_
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
a✝ : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ a✝)) = shift D (V ∘ Var.close j (free_ z)) d (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
a✝ : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ a✝)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ a✝)

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ x)) = shift D (V ∘ Var.close j (free_ z)) d (free_ x)
Tactic:
case _ x =>
  conv =>
    rhs
    simp only [shift]
    simp
  simp only [Var.close]
  simp
  split_ifs
  case _ c1 =>
    simp only [shift]
    simp
  case _ c1 =>
    simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ i)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ i)
Tactic:
case _ i =>
  cases i
  case zero =>
    conv =>
      rhs
      simp only [shift]
    simp only [Var.close]
    simp
    simp only [shift]
  case succ i =>
    conv =>
      rhs
      simp only [shift]
      simp
      simp only [Var.close]
    simp only [Var.close]
    split
    case _ c1 =>
      have s1 : i < j
      linarith
      simp only [if_pos s1]
      simp only [shift]
    case _ c1 =>
      simp at c1
      have s1 : ¬ i < j
      linarith
      simp only [if_neg s1]
      simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ x)) = shift D (V ∘ Var.close j (free_ z)) d (free_ x)
Tactic:
conv =>
  rhs
  simp only [shift]
  simp
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ x)) = V (Var.close j (free_ z) (free_ x))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ x)) = V (Var.close j (free_ z) (free_ x))
Tactic:
simp only [Var.close]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if free_ x = free_ z then bound_ (j + 1) else free_ x) =
    V (if free_ x = free_ z then bound_ j else free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if free_ x = free_ z then bound_ (j + 1) else free_ x) =
    V (if free_ x = free_ z then bound_ j else free_ x)
Tactic:
simp
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if x = z then bound_ (j + 1) else free_ x) = V (if x = z then bound_ j else free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if x = z then bound_ (j + 1) else free_ x) = V (if x = z then bound_ j else free_ x)
Tactic:
split_ifs
State after:
case pos
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
h✝ : x = z
⊢ shift D V d (bound_ (j + 1)) = V (bound_ j)

case neg
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
h✝ : ¬x = z
⊢ shift D V d (free_ x) = V (free_ x)

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
c1 : x = z
⊢ shift D V d (bound_ (j + 1)) = V (bound_ j)
Tactic:
case _ c1 =>
  simp only [shift]
  simp
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
c1 : ¬x = z
⊢ shift D V d (free_ x) = V (free_ x)
Tactic:
case _ c1 =>
  simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
c1 : x = z
⊢ shift D V d (bound_ (j + 1)) = V (bound_ j)
Tactic:
simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
c1 : ¬x = z
⊢ shift D V d (free_ x) = V (free_ x)
Tactic:
simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ i)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ i)
Tactic:
cases i
State after:
case zero
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ 0)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ 0)

case succ
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
n✝ : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ (n✝ + 1))) = shift D (V ∘ Var.close j (free_ z)) d (bound_ (n✝ + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ 0)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ 0)
Tactic:
case zero =>
  conv =>
    rhs
    simp only [shift]
  simp only [Var.close]
  simp
  simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ (i + 1))) = shift D (V ∘ Var.close j (free_ z)) d (bound_ (i + 1))
Tactic:
case succ i =>
  conv =>
    rhs
    simp only [shift]
    simp
    simp only [Var.close]
  simp only [Var.close]
  split
  case _ c1 =>
    have s1 : i < j
    linarith
    simp only [if_pos s1]
    simp only [shift]
  case _ c1 =>
    simp at c1
    have s1 : ¬ i < j
    linarith
    simp only [if_neg s1]
    simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ 0)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ 0)
Tactic:
conv =>
  rhs
  simp only [shift]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ 0)) = d

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ 0)) = d
Tactic:
simp only [Var.close]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (if 0 < j + 1 then bound_ 0 else bound_ (0 + 1)) = d

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (if 0 < j + 1 then bound_ 0 else bound_ (0 + 1)) = d
Tactic:
simp
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (bound_ 0) = d

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d (bound_ 0) = d
Tactic:
simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ (i + 1))) = shift D (V ∘ Var.close j (free_ z)) d (bound_ (i + 1))
Tactic:
conv =>
  rhs
  simp only [shift]
  simp
  simp only [Var.close]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ (i + 1))) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ (i + 1))) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [Var.close]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (if i + 1 < j + 1 then bound_ (i + 1) else bound_ (i + 1 + 1)) =
    V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (if i + 1 < j + 1 then bound_ (i + 1) else bound_ (i + 1 + 1)) =
    V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
split
State after:
case inl
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
h✝ : i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

case inr
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
h✝ : ¬i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
case _ c1 =>
  have s1 : i < j
  linarith
  simp only [if_pos s1]
  simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : ¬i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
case _ c1 =>
  simp at c1
  have s1 : ¬ i < j
  linarith
  simp only [if_neg s1]
  simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
have s1 : i < j
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
⊢ i < j

D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
case s1
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
⊢ i < j

D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
linarith
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [if_pos s1]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (bound_ i)

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : i + 1 < j + 1
s1 : i < j
⊢ shift D V d (bound_ (i + 1)) = V (bound_ i)
Tactic:
simp only [shift]
State after:
no goals

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : ¬i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp at c1
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
have s1 : ¬ i < j
State after:
case s1
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
⊢ ¬i < j

D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
case s1
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
⊢ ¬i < j

D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
linarith
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))
Tactic:
simp only [if_neg s1]
State after:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (bound_ (i + 1))

State before:
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
c1 : j ≤ i
s1 : ¬i < j
⊢ shift D V d (bound_ (i + 1 + 1)) = V (bound_ (i + 1))
Tactic:
simp only [shift]
State after:
no goals