Theorem: Lean4Lean.TrLCtx.fvars_eq (Lean4Lean/Verify/LocalContext.lean)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ LocalContext.fvars lctx = VLCtx.fvars Δ
Tactic:
simp [LocalContext.fvars, VLCtx.fvars, LocalContext.toList]
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ List.map (fun x => LocalDecl.fvarId x) (List.filterMap id (List.reverse (PersistentArray.toList' lctx.decls))) =
    List.filterMap (fun x => x.fst) Δ

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
H : TrLCtx env Us lctx Δ
⊢ List.map (fun x => LocalDecl.fvarId x) (List.filterMap id (List.reverse (PersistentArray.toList' lctx.decls))) =
    List.filterMap (fun x => x.fst) Δ
Tactic:
induction H with
| nil => rfl
| cons h1 _ _ _ _ ih => simp [h1, ← ih]
State after:
no goals

State before:
case nil
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
⊢ List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id
        (List.reverse
          (PersistentArray.toList'
            { fvarIdToDecl := PersistentHashMap.empty, decls := PersistentArray.empty }.decls))) =
    List.filterMap (fun x => x.fst) []
Tactic:
rfl
State after:
no goals

State before:
case cons
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
a✝¹ : TrLCtx env Us { fvarIdToDecl := map✝, decls := arr✝ } Δ✝
a✝ : TrLocalDecl env Us Δ✝ d✝ d'✝
ih :
  List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id (List.reverse (PersistentArray.toList' { fvarIdToDecl := map✝, decls := arr✝ }.decls))) =
    List.filterMap (fun x => x.fst) Δ✝
⊢ List.map (fun x => LocalDecl.fvarId x)
      (List.filterMap id
        (List.reverse
          (PersistentArray.toList'
            { fvarIdToDecl := PersistentHashMap.insert map✝ fv✝ d✝,
                decls := PersistentArray.push arr✝ (some d✝) }.decls))) =
    List.filterMap (fun x => x.fst) ((some fv✝, d'✝) :: Δ✝)
Tactic:
simp [h1, ← ih]
State after:
no goals