Theorem: Lean4Lean.TrLCtx.forall₂ (Lean4Lean/Verify/LocalContext.lean)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty }) []
Tactic:
simp [LocalContext.toList]
State after:
no goals

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv✝ : FVarId
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
h1 : LocalDecl.fvarId d✝ = fv✝
a✝² : PersistentHashMap.find? map✝ fv✝ = none
a✝¹ : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝ : TrLocalDecl env Us Δ✝ d✝ d'✝
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝, decls := PersistentArray.push arr✝ (some d✝) })
    ((some fv✝, d'✝) :: Δ✝)
Tactic:
subst h1
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝² : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
        decls := PersistentArray.push arr✝ (some d✝) })
    ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝² : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (LocalContext.toList
      { fvarIdToDecl := PersistentHashMap.insert map✝ (LocalDecl.fvarId d✝) d✝,
        decls := PersistentArray.push arr✝ (some d✝) })
    ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Tactic:
simp [LocalContext.toList]
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝² : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (d✝ :: List.filterMap id (List.reverse (PersistentArray.toList' arr✝))) ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
map✝ : PersistentHashMap FVarId LocalDecl
arr✝ : PersistentArray (Option LocalDecl)
Δ✝ : VLCtx
d✝ : LocalDecl
d'✝ : VLocalDecl
a✝² : LocalDecl.index d✝ = arr✝.size
h4 : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝¹ : TrLocalDecl env Us Δ✝ d✝ d'✝
a✝ : PersistentHashMap.find? map✝ (LocalDecl.fvarId d✝) = none
⊢ List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d))
    (d✝ :: List.filterMap id (List.reverse (PersistentArray.toList' arr✝))) ((some (LocalDecl.fvarId d✝), d'✝) :: Δ✝)
Tactic:
exact .cons rfl h4.forall₂
State after:
no goals