Theorem: Lean4Lean.Lookup.weakN (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ i A
⊢ Lookup Γ' (liftVar n i k) (liftN n A k)
Tactic:
induction W generalizing i A with
| zero As =>
  rw [liftVar_base, Nat.add_comm]
  subst n
  induction As with simp [*]
  | cons _ _ ih => rw [liftN_succ]; exact .succ ih
| @succ k _ _ _ _ ih =>
  match H with
  | .zero => rw [liftVar_zero, ← lift_liftN']; exact .zero
  | .succ H => rw [liftVar_succ, ← lift_liftN']; exact (ih H).succ
State after:
no goals

State before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (liftVar n i) (liftN n A)
Tactic:
rw [liftVar_base, Nat.add_comm]
State after:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + n) (liftN n A)

State before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + n) (liftN n A)
Tactic:
subst n
State after:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)

State before:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
Tactic:
induction As with simp [*]
| cons _ _ ih => rw [liftN_succ]; exact .succ ih
State after:
no goals

State before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (liftN (Nat.succ (List.length tail✝)) A)
Tactic:
rw [liftN_succ]
State after:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (lift (liftN (List.length tail✝) A))

State before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (lift (liftN (List.length tail✝) A))
Tactic:
exact .succ ih
State after:
no goals

State before:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) (liftN n A (k + 1))
Tactic:
match H with
| .zero => rw [liftVar_zero, ← lift_liftN']; exact .zero
| .succ H => rw [liftVar_succ, ← lift_liftN']; exact (ih H).succ
State after:
no goals

State before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n 0 (k + 1)) (liftN n (lift A✝) (k + 1))
Tactic:
rw [liftVar_zero, ← lift_liftN']
State after:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) 0 (lift (liftN n A✝ k))

State before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) 0 (lift (liftN n A✝ k))
Tactic:
exact .zero
State after:
no goals

State before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n (n✝ + 1) (k + 1)) (liftN n (lift ty✝) (k + 1))
Tactic:
rw [liftVar_succ, ← lift_liftN']
State after:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n n✝ k + 1) (lift (liftN n ty✝ k))

State before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n n✝ k + 1) (lift (liftN n ty✝ k))
Tactic:
exact (ih H).succ
State after:
no goals