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

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

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

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

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

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

State before:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [if_pos]
State after:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k = bvar (liftVar n i k)

case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftVar n i k < n + j

State before:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftVar n i k < n + j
Tactic:
simp only [liftN, liftVar]
State after:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ (if i < k then i else n + i) < n + j

State before:
case inl.hc
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ (if i < k then i else n + i) < n + j
Tactic:
split <;> rename_i hk
State after:
case inl.hc.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : i < k
⊢ i < n + j

case inl.hc.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : ¬i < k
⊢ n + i < n + j

State before:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k = bvar (liftVar n i k)
Tactic:
rfl
State after:
no goals

State before:
case inl.hc.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : i < k
⊢ i < n + j
Tactic:
exact Nat.lt_add_left _ h
State after:
no goals

State before:
case inl.hc.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
hk : ¬i < k
⊢ n + i < n + j
Tactic:
exact Nat.add_lt_add_left h _
State after:
no goals

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

State before:
case inr.inl
n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬j < j
⊢ liftN n (liftN j e) k =
    if liftVar n j k < n + j then bvar (liftVar n j k)
    else if liftVar n j k = n + j then liftN (n + j) e else bvar (liftVar n j k - 1)
Tactic:
rw [liftN'_liftN' (h1 := Nat.zero_le _) (h2 := hj), liftVar_le hj,
  if_neg (by simp), if_pos rfl, Nat.add_comm]
State after:
no goals

State before:
n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬j < j
⊢ ¬n + j < n + j
Tactic:
simp
State after:
no goals

State before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [Nat.not_lt] at h
State after:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)

State before:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
rw [liftVar_le (Nat.le_trans hj h)]
State after:
case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : j ≤ i
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if n + i < n + j then bvar (n + i) else if n + i = n + j then liftN (n + j) e else bvar (n + i - 1)

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

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

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

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

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

State before:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (liftVar n (i + 1 - 1) k) = bvar (n + (i + 1) - 1)
Tactic:
rw [liftVar_le (Nat.le_trans hj <| by exact Nat.le_of_lt_succ hk)]
State after:
case inr.inr
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ bvar (n + (i + 1 - 1)) = bvar (n + (i + 1) - 1)

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

State before:
i✝ n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
i : Nat
h : j ≤ i + 1
h' : ¬i + 1 = j
hk : j < i + 1
this : n + j < n + (i + 1)
⊢ j ≤ i + 1 - 1
Tactic:
exact Nat.le_of_lt_succ hk
State after:
no goals