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

State before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ Lookup Γ' (liftVar n i k) (liftN n A k) ↔ Lookup Γ i A
Tactic:
refine ⟨fun H => ?_, fun H => H.weakN W⟩
State after:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ' (liftVar n i k) (liftN n A k)
⊢ Lookup Γ i A

State before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ' (liftVar n i k) (liftN n A k)
⊢ Lookup Γ i A
Tactic:
induction W generalizing i A with
| zero As =>
  rw [liftVar_base, Nat.add_comm] at H
  subst n
  induction As with simp at H
  | nil => exact H
  | cons A As ih =>
    rw [liftN_succ] at H
    generalize eq : lift (liftN ..) = A' at H
    obtain _|H := H; cases liftN_inj.1 eq
    exact ih H
| @succ k _ _ _ _ ih =>
  generalize eA : liftN n A (k+1) = A' at H
  cases i with
  | zero =>
    simp at H; let .zero := H
    rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
    subst A; exact .zero
  | succ i =>
    simp at H; let .succ H := H
    obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
    exact .succ (ih H)
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 (As ++ Γ✝) (liftVar n i) (liftN n A)
⊢ Lookup Γ✝ i A
Tactic:
rw [liftVar_base, Nat.add_comm] at H
State after:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + n) (liftN n A)
⊢ Lookup Γ✝ i A

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

State before:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
⊢ Lookup Γ✝ i A
Tactic:
induction As with simp at H
| nil => exact H
| cons A As ih =>
  rw [liftN_succ] at H
  generalize eq : lift (liftN ..) = A' at H
  obtain _|H := H; cases liftN_inj.1 eq
  exact ih H
State after:
no goals

State before:
case zero.nil
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup Γ✝ i A
Tactic:
exact H
State after:
no goals

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

State before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) (lift (liftN (List.length As) A✝))
⊢ Lookup Γ✝ i A✝
Tactic:
generalize eq : lift (liftN ..) = A' at H
State after:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
A' : VExpr
eq : lift (liftN (List.length As) A✝) = A'
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) A'
⊢ Lookup Γ✝ i A✝

State before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
A' : VExpr
eq : lift (liftN (List.length As) A✝) = A'
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) A'
⊢ Lookup Γ✝ i A✝
Tactic:
obtain _|H := H
State after:
case zero.cons.succ
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
ty✝ : VExpr
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) ty✝
eq : lift (liftN (List.length As) A✝) = lift ty✝
⊢ Lookup Γ✝ i A✝

State before:
case zero.cons.succ
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
ty✝ : VExpr
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) ty✝
eq : lift (liftN (List.length As) A✝) = lift ty✝
⊢ Lookup Γ✝ i A✝
Tactic:
cases liftN_inj.1 eq
State after:
case zero.cons.succ.refl
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) (liftN (List.length As) A✝)
eq : lift (liftN (List.length As) A✝) = lift (liftN (List.length As) A✝)
⊢ Lookup Γ✝ i A✝

State before:
case zero.cons.succ.refl
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) (liftN (List.length As) A✝)
eq : lift (liftN (List.length As) A✝) = lift (liftN (List.length As) A✝)
⊢ Lookup Γ✝ i A✝
Tactic:
exact ih H
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 Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) (liftN n A (k + 1))
⊢ Lookup (A✝ :: Γ✝) i A
Tactic:
generalize eA : liftN n A (k+1) = A' at H
State after:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) i A

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 Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) i A
Tactic:
cases i with
| zero =>
  simp at H; let .zero := H
  rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
  subst A; exact .zero
| succ i =>
  simp at H; let .succ H := H
  obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
  exact .succ (ih H)
State after:
no goals

State before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n Nat.zero (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
simp at H
State after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A

State before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
let .zero := H
State after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : liftN n A (k + 1) = lift (liftN n A✝ k)
⊢ Lookup (A✝ :: Γ✝) Nat.zero A

State before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : liftN n A (k + 1) = lift (liftN n A✝ k)
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
State after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : A = liftN 1 A✝
⊢ Lookup (A✝ :: Γ✝) Nat.zero A

State before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : A = liftN 1 A✝
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
subst A
State after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero (liftN 1 A✝)

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

State before:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
i : Nat
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n (Nat.succ i) (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Tactic:
simp at H
State after:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
i : Nat
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A

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

State before:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
ty✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) ty✝
eA : liftN n A (k + 1) = lift ty✝
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Tactic:
obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
State after:
case succ.succ.intro.intro
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
w✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) (liftN n w✝ (k + 0))
eA : liftN n (liftN 1 w✝) (k + 1) = lift (liftN n w✝ (k + 0))
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) (liftN 1 w✝)

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