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

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

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

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

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

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

State before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
have := Nat.lt_add_left k h
State after:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)

State before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) =
    if liftVar n i (k + j + 1) < j then bvar (liftVar n i (k + j + 1))
    else if liftVar n i (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n i (k + j + 1) - 1)
Tactic:
rw [liftVar_lt <| Nat.lt_succ_of_lt this, if_pos h]
State after:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar i

State before:
case inl
i : Nat
e2 : VExpr
n k j : Nat
h : i < j
this : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar i
Tactic:
simp [liftN, liftVar_lt this]
State after:
no goals

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

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

State before:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) =
    if liftVar n j (k + j + 1) < j then bvar (liftVar n j (k + j + 1))
    else if liftVar n j (k + j + 1) = j then liftN j (liftN n e2 k) else bvar (liftVar n j (k + j + 1) - 1)
Tactic:
simp [liftVar_lt (by exact Nat.lt_succ_of_le this)]
State after:
case inr.inl
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ liftN n (liftN j e2) (k + j) = liftN j (liftN n e2 k)

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

State before:
e2 : VExpr
n k j : Nat
h : ¬j < j
this : j ≤ k + j
⊢ ?m.56873 < ?m.56874
Tactic:
exact Nat.lt_succ_of_le this
State after:
no goals

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

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

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

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

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

State before:
case inr.inr.inl
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : i < k + j
⊢ liftN n (bvar i) (k + j) = bvar (i + 1 - 1)
Tactic:
simp [liftN, liftVar_lt hi]
State after:
no goals

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

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

State before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftN n (bvar i) (k + j) = bvar (n + (i + 1) - 1)
Tactic:
simp [liftN]
State after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftVar n i (k + j) = n + (i + 1) - 1

State before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ liftVar n i (k + j) = n + (i + 1) - 1
Tactic:
rw [liftVar_le (Nat.not_lt.1 hi)]
State after:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ n + i = n + (i + 1) - 1

State before:
case inr.inr.inr
i✝ : Nat
e2 : VExpr
n k j i : Nat
h : ¬i + 1 < j
h' : ¬i + 1 = j
hk : j < i + 1
hi : ¬i < k + j
this : j < n + (i + 1)
⊢ n + i = n + (i + 1) - 1
Tactic:
rfl
State after:
no goals