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

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

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

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

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

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

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

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

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

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

State before:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k
h' : ¬i = k
⊢ inst (bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k
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
h' : ¬i = k
hk : k < i
⊢ inst (bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k

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

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

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

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

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

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

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

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

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

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

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

State before:
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬j + k + 1 < k
h' : ¬j + k + 1 = k
hk : k < j + k + 1
hi : ¬j + k < j + k
this : liftN (j + k + 1) ?m.110132 = ?m.110135
⊢ liftN (j + k) e3 = inst (liftN (j + k + 1) e3) (inst e2 e3 j) k
Tactic:
rw [this]
State after:
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬j + k + 1 < k
h' : ¬j + k + 1 = k
hk : k < j + k + 1
hi : ¬j + k < j + k
this : liftN (j + k + 1) e3 = ?m.110135
⊢ liftN (j + k) e3 = inst ?m.110135 (inst e2 e3 j) k

i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬j + k + 1 < k
h' : ¬j + k + 1 = k
hk : k < j + k + 1
hi : ¬j + k < j + k
⊢ VExpr

State before:
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬j + k + 1 < k
h' : ¬j + k + 1 = k
hk : k < j + k + 1
hi : ¬j + k < j + k
this : liftN (j + k + 1) e3 = ?m.110135
⊢ liftN (j + k) e3 = inst ?m.110135 (inst e2 e3 j) k

i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬j + k + 1 < k
h' : ¬j + k + 1 = k
hk : k < j + k + 1
hi : ¬j + k < j + k
⊢ VExpr
Tactic:
exact (inst_liftN ..).symm
State after:
no goals

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

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

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

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

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