Theorem: Lean4Lean.VLCtx.WF.find?_wf (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ : VLCtx
hΔ : WF env U Δ
H : find? Δ v = some (e, A)
⊢ HasType env U (toCtx Δ) e A
Tactic:
let (ofv, d') :: Δ := Δ
State after:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H : find? ((ofv, d') :: Δ) v = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

State before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H : find? ((ofv, d') :: Δ) v = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
unfold VLCtx.find? at H
State after:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H :
  (match next ofv v with
    | none => some (VLocalDecl.value d', VLocalDecl.type d')
    | some v => do
      let __discr ← find? Δ v
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

State before:
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
H :
  (match next ofv v with
    | none => some (VLocalDecl.value d', VLocalDecl.type d')
    | some v => do
      let __discr ← find? Δ v
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
split at H
State after:
case h_1
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
H : some (VLocalDecl.value d', VLocalDecl.type d') = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H :
  (do
      let __discr ← find? Δ v✝
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

State before:
case h_1
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
H : some (VLocalDecl.value d', VLocalDecl.type d') = some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
cases H
State after:
case h_1.refl
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VLocalDecl.value d') (VLocalDecl.type d')

State before:
case h_1.refl
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv v = none
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VLocalDecl.value d') (VLocalDecl.type d')
Tactic:
exact hΔ.2.2.hasType
State after:
no goals

State before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H :
  (do
      let __discr ← find? Δ v✝
      match __discr with
        | (e, A) => some (VExpr.liftN (VLocalDecl.depth d') e, VExpr.liftN (VLocalDecl.depth d') A)) =
    some (e, A)
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
simp [bind, Option.bind_eq_some] at H
State after:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H : ∃ a, find? Δ v✝ = some a ∧ VExpr.liftN (VLocalDecl.depth d') a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d') a.snd = A
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A

State before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
e A : VExpr
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
H : ∃ a, find? Δ v✝ = some a ∧ VExpr.liftN (VLocalDecl.depth d') a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d') a.snd = A
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) e A
Tactic:
obtain ⟨⟨d'', n'⟩, H, rfl, rfl⟩ := H
State after:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)

State before:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Tactic:
obtain h3 := hΔ.1.find?_wf H
State after:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
h3 : HasType env U (toCtx Δ) d'' n'
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)

State before:
case h_2.intro.mk.intro.intro
env : VEnv
henv : Ordered env
U : Nat
v : Nat ⊕ FVarId
Δ✝ : VLCtx
ofv : Option FVarId
d' : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
hΔ : WF env U ((ofv, d') :: Δ)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv v = some v✝
d'' n' : VExpr
H : find? Δ v✝ = some (d'', n')
h3 : HasType env U (toCtx Δ) d'' n'
⊢ HasType env U (toCtx ((ofv, d') :: Δ)) (VExpr.liftN (VLocalDecl.depth d') (d'', n').fst)
    (VExpr.liftN (VLocalDecl.depth d') (d'', n').snd)
Tactic:
exact h3.weakN henv VLocalDecl.is_liftN
State after:
no goals