Theorem: Lean4Lean.TrLCtx.find?_isSome (Lean4Lean/Verify/LocalContext.lean)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (LocalContext.find? lctx fv) = Option.isSome (VLCtx.find? Δ (Sum.inr fv))
Tactic:
rw [LocalContext.find?, H.map_wf.find?_eq, ← VLCtx.lookup_isSome,
  H.map_toList.lookup_eq H.map_wf.nodupKeys, List.map_fst_lookup]
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Tactic:
have := H.forall₂
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) (LocalContext.toList lctx) Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) (LocalContext.toList lctx) Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (LocalContext.toList lctx)) =
    Option.isSome (List.lookup (some fv) Δ)
Tactic:
generalize lctx.toList = l at this ⊢
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)
Tactic:
clear H
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
this : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l Δ
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l) = Option.isSome (List.lookup (some fv) Δ)
Tactic:
induction this with
| nil => rfl
| @cons d d' _ _ eq _ ih =>
  cases d'; cases eq
  simp [List.find?, List.lookup, show (some fv == some d.fvarId) = (fv == d.fvarId) from rfl]
  split <;> simp [*]
State after:
no goals

State before:
case nil
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) []) = Option.isSome (List.lookup (some fv) [])
Tactic:
rfl
State after:
no goals

State before:
case cons
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
d' : Option FVarId × VLocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
eq : d'.fst = some (LocalDecl.fvarId d)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) (d' :: l₂✝))
Tactic:
cases d'
State after:
case cons.mk
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
fst✝ : Option FVarId
snd✝ : VLocalDecl
eq : (fst✝, snd✝).fst = some (LocalDecl.fvarId d)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((fst✝, snd✝) :: l₂✝))

State before:
case cons.mk
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
fst✝ : Option FVarId
snd✝ : VLocalDecl
eq : (fst✝, snd✝).fst = some (LocalDecl.fvarId d)
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((fst✝, snd✝) :: l₂✝))
Tactic:
cases eq
State after:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((some (LocalDecl.fvarId d), snd✝) :: l₂✝))

State before:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) (d :: l₁✝)) =
    Option.isSome (List.lookup (some fv) ((some (LocalDecl.fvarId d), snd✝) :: l₂✝))
Tactic:
simp [List.find?, List.lookup, show (some fv == some d.fvarId) = (fv == d.fvarId) from rfl]
State after:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some d
      | false => List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) =
    Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some snd✝
      | false => List.lookup (some fv) l₂✝)

State before:
case cons.mk.refl
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
l : List LocalDecl
d : LocalDecl
l₁✝ : List LocalDecl
l₂✝ : List (Option FVarId × VLocalDecl)
a✝ : List.Forall₂ (fun d d' => d'.fst = some (LocalDecl.fvarId d)) l₁✝ l₂✝
ih : Option.isSome (List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) = Option.isSome (List.lookup (some fv) l₂✝)
snd✝ : VLocalDecl
⊢ Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some d
      | false => List.find? (fun a => fv == LocalDecl.fvarId a) l₁✝) =
    Option.isSome
      (match fv == LocalDecl.fvarId d with
      | true => some snd✝
      | false => List.lookup (some fv) l₂✝)
Tactic:
split <;> simp [*]
State after:
no goals