Theorem: Lean4Lean.VExpr.ClosedN.instN (Lean4Lean/Theory/VExpr.lean)

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

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

case inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
⊢ ClosedN (if i = j then liftN j e2 else bvar (i - 1)) (k + j)

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

case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
⊢ ClosedN (bvar (i - 1)) (k + j)

State before:
case inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : i < j
⊢ ClosedN (bvar i) (k + j)
Tactic:
exact Nat.lt_of_lt_of_le h1 (Nat.le_add_left ..)
State after:
no goals

State before:
case inr.inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : i = j
⊢ ClosedN (liftN j e2) (k + j)
Tactic:
exact h2.liftN
State after:
no goals

State before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
⊢ ClosedN (bvar (i - 1)) (k + j)
Tactic:
have hk := Nat.lt_of_le_of_ne (Nat.not_lt.1 h1) (Ne.symm h1')
State after:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
hk : j < i
⊢ ClosedN (bvar (i - 1)) (k + j)

State before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
hk : j < i
⊢ ClosedN (bvar (i - 1)) (k + j)
Tactic:
let i+1 := i
State after:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i✝ i : Nat
h : ClosedN (bvar (i + 1)) (k + j + 1)
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hk : j < i + 1
⊢ ClosedN (bvar (i + 1 - 1)) (k + j)

State before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i✝ i : Nat
h : ClosedN (bvar (i + 1)) (k + j + 1)
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hk : j < i + 1
⊢ ClosedN (bvar (i + 1 - 1)) (k + j)
Tactic:
exact Nat.lt_of_succ_lt_succ h
State after:
no goals