internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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'
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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)]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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')
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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]
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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'
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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']
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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]
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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')
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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]
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof 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)]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_hi
Proof state before:
e1 e2 e3 : VExpr
k j : Nat
⊢ inst (inst e1 e2 k) e3 (j + k) = inst (inst e1 e3 (j + k + 1)) (inst e2 e3 j) k
Tactic:
induction e1 generalizing k with simp [liftN, inst, instVar, *]
| bvar i => apply inst_instVar_hi
| _ => rename_i IH; apply IH
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_hi
Proof state before:
case bvar
e2 e3 : VExpr
j i k : 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:
apply inst_instVar_hi
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_hi
Proof state before:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
body_ih✝ : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)
Tactic:
rename_i IH
Proof state after:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
IH : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)
Theorem: Lean4Lean.VExpr.inst_inst_hi
Proof state before:
case forallE
e2 e3 : VExpr
j : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (k : Nat), inst (inst binderType✝ e2 k) e3 (j + k) = inst (inst binderType✝ e3 (j + k + 1)) (inst e2 e3 j) k
IH : ∀ (k : Nat), inst (inst body✝ e2 k) e3 (j + k) = inst (inst body✝ e3 (j + k + 1)) (inst e2 e3 j) k
k : Nat
⊢ inst (inst body✝ e2 (k + 1)) e3 (j + k + 1) = inst (inst body✝ e3 (j + k + 1 + 1)) (inst e2 e3 j) (k + 1)
Tactic:
apply IH
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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'
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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'
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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 ..))]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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')
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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)
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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)]
Proof 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)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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]
Proof 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
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof 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 ..
Proof 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