Theorem: Lean4Lean.Lookup.weak'_iff (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
generalize e : l.depth = n
State after:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A

State before:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
induction n generalizing l Γ' with
| zero => rw [liftVar_depth_zero e, VExpr.lift'_depth_zero e, W.depth_zero e]
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  rw [Lift.consN_skip_eq, liftVar_comp, liftVar_consN_skipN, lift'_comp, lift'_consN_skipN,
    weakN_iff W2, ih W1 Lift.depth_consN]
State after:
no goals

State before:
case zero
Γ : List VExpr
i : Nat
A : VExpr
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
rw [liftVar_depth_zero e, VExpr.lift'_depth_zero e, W.depth_zero e]
State after:
no goals

State before:
case succ
Γ : List VExpr
i : Nat
A : VExpr
n : Nat
ih :
  ∀ {l : Lift} {Γ' : List VExpr},
    Ctx.Lift' l Γ Γ' → Lift.depth l = n → (Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A)
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
State after:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A

State before:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
State after:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A

State before:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Tactic:
rw [Lift.consN_skip_eq, liftVar_comp, liftVar_consN_skipN, lift'_comp, lift'_consN_skipN,
  weakN_iff W2, ih W1 Lift.depth_consN]
State after:
no goals