Theorem: Lean4Lean.VExpr.inst_instVar_lo (Lean4Lean/Theory/VExpr.lean)

State before:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (instVar i e2 (k + j + 1)) e3 j = inst (instVar i (liftN 1 e3 k) j) e2 (k + j)
Tactic:
simp [instVar]
State after:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (if i < k + j + 1 then bvar i else if i = k + j + 1 then liftN (k + j + 1) e2 else bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

State before:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (if i < k + j + 1 then bvar i else if i = k + j + 1 then liftN (k + j + 1) e2 else bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
split <;> rename_i h
State after:
case inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
⊢ inst (bvar i) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

case inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
⊢ inst (if i = k + j + 1 then liftN (k + j + 1) e2 else bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

State before:
case inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
⊢ inst (if i = k + j + 1 then liftN (k + j + 1) e2 else bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
split <;> rename_i h'
State after:
case inr.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : i = k + j + 1
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

State before:
case inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
⊢ inst (bvar i) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
split <;> rename_i h1
State after:
case inl.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : i < j
⊢ inst (bvar i) e3 j = inst (bvar i) e2 (k + j)

case inl.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
⊢ inst (bvar i) e3 j = inst (if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

State before:
case inl.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
⊢ inst (bvar i) e3 j = inst (if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
split <;> rename_i h1'
State after:
case inl.inr.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : i = j
⊢ inst (bvar i) e3 j = inst (liftN j (liftN 1 e3 k)) e2 (k + j)

case inl.inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : ¬i = j
⊢ inst (bvar i) e3 j = inst (bvar (i - 1)) e2 (k + j)

State before:
case inl.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : i < j
⊢ inst (bvar i) e3 j = inst (bvar i) e2 (k + j)
Tactic:
simp [inst, instVar, h1]
State after:
case inl.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : i < j
⊢ bvar i = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)

State before:
case inl.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : i < j
⊢ bvar i = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)
Tactic:
rw [if_pos (Nat.lt_of_lt_of_le h1 (Nat.le_add_left ..))]
State after:
no goals

State before:
case inl.inr.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : i = j
⊢ inst (bvar i) e3 j = inst (liftN j (liftN 1 e3 k)) e2 (k + j)
Tactic:
subst i
State after:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ inst (bvar j) e3 j = inst (liftN j (liftN 1 e3 k)) e2 (k + j)

State before:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ inst (bvar j) e3 j = inst (liftN j (liftN 1 e3 k)) e2 (k + j)
Tactic:
simp [inst, instVar]
State after:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ liftN j e3 = inst (liftN j (liftN 1 e3 k)) e2 (k + j)

State before:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ liftN j e3 = inst (liftN j (liftN 1 e3 k)) e2 (k + j)
Tactic:
rw [liftN'_comm (h := Nat.zero_le _), Nat.add_comm]
State after:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ liftN j e3 = inst (liftN 1 (liftN j e3) (k + j)) e2 (k + j)

State before:
case inl.inr.inl
e2 e3 : VExpr
k j : Nat
h : j < k + j + 1
h1 : ¬j < j
⊢ liftN j e3 = inst (liftN 1 (liftN j e3) (k + j)) e2 (k + j)
Tactic:
exact (inst_liftN ..).symm
State after:
no goals

State before:
case inl.inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : ¬i = j
⊢ inst (bvar i) e3 j = inst (bvar (i - 1)) e2 (k + j)
Tactic:
have hj := Nat.lt_of_le_of_ne (Nat.not_lt.1 h1) (Ne.symm h1')
State after:
case inl.inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : ¬i = j
hj : j < i
⊢ inst (bvar i) e3 j = inst (bvar (i - 1)) e2 (k + j)

State before:
case inl.inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k + j + 1
h1 : ¬i < j
h1' : ¬i = j
hj : j < i
⊢ inst (bvar i) e3 j = inst (bvar (i - 1)) e2 (k + j)
Tactic:
let i+1 := i
State after:
case inl.inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : i + 1 < k + j + 1
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hj : j < i + 1
⊢ inst (bvar (i + 1)) e3 j = inst (bvar (i + 1 - 1)) e2 (k + j)

State before:
case inl.inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : i + 1 < k + j + 1
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hj : j < i + 1
⊢ inst (bvar (i + 1)) e3 j = inst (bvar (i + 1 - 1)) e2 (k + j)
Tactic:
simp [inst, instVar, h1, h1', Nat.lt_of_succ_lt_succ h]
State after:
no goals

State before:
case inr.inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : i = k + j + 1
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
subst i
State after:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst
      (if k + j + 1 < j then bvar (k + j + 1)
      else if k + j + 1 = j then liftN j (liftN 1 e3 k) else bvar (k + j + 1 - 1))
      e2 (k + j)

State before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst
      (if k + j + 1 < j then bvar (k + j + 1)
      else if k + j + 1 = j then liftN j (liftN 1 e3 k) else bvar (k + j + 1 - 1))
      e2 (k + j)
Tactic:
have := Nat.lt_succ_of_le (Nat.le_add_left j k)
State after:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst
      (if k + j + 1 < j then bvar (k + j + 1)
      else if k + j + 1 = j then liftN j (liftN 1 e3 k) else bvar (k + j + 1 - 1))
      e2 (k + j)

State before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j =
    inst
      (if k + j + 1 < j then bvar (k + j + 1)
      else if k + j + 1 = j then liftN j (liftN 1 e3 k) else bvar (k + j + 1 - 1))
      e2 (k + j)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
State after:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j = inst (bvar (k + j + 1 - 1)) e2 (k + j)

State before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j = inst (bvar (k + j + 1 - 1)) e2 (k + j)
Tactic:
simp [inst, instVar]
State after:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j = liftN (k + j) e2

State before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ inst (liftN (k + j + 1) e2) e3 j = liftN (k + j) e2
Tactic:
suffices liftN (k+j+1) .. = _ by rw [this]; exact inst_liftN ..
State after:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ liftN (k + j + 1) e2 = liftN 1 (liftN (k + j) e2) j

State before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ liftN (k + j + 1) e2 = liftN 1 (liftN (k + j) e2) j
Tactic:
exact (liftN'_liftN' (Nat.zero_le _) (Nat.le_add_left j k)).symm
State after:
no goals

State before:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) ?m.117762 = ?m.117771
⊢ inst (liftN (k + j + 1) e2) e3 j = liftN (k + j) e2
Tactic:
rw [this]
State after:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) e2 = ?m.117771
⊢ inst ?m.117771 e3 j = liftN (k + j) e2

e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ VExpr

State before:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) e2 = ?m.117771
⊢ inst ?m.117771 e3 j = liftN (k + j) e2

e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ VExpr
Tactic:
exact inst_liftN ..
State after:
no goals

State before:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
have hk := Nat.lt_of_le_of_ne (Nat.not_lt.1 h) (Ne.symm h')
State after:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
hk : k + j + 1 < i
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)

State before:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
hk : k + j + 1 < i
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
let i+1 := i
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk : k + j + 1 < i + 1
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk : k + j + 1 < i + 1
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Tactic:
have hk := Nat.lt_of_add_lt_add_right hk
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Tactic:
simp [inst, instVar, hk]
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
have := Nat.lt_of_le_of_lt (Nat.le_add_left ..) hk
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
have := Nat.lt_succ_of_lt this
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = inst (bvar i) e2 (k + j)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = inst (bvar i) e2 (k + j)
Tactic:
simp [inst, instVar]
State after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)

State before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)
Tactic:
rw [if_neg (Nat.lt_asymm hk), if_neg (Nat.ne_of_gt hk)]
State after:
no goals