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

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ LocalContext.contains lctx fv = true ↔ fv ∈ VLCtx.fvars Δ
Tactic:
rw [LocalContext.contains, PersistentHashMap.find?_isSome, Option.isSome_iff_exists]
State after:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ a, PersistentHashMap.find? lctx.fvarIdToDecl fv = some a) ↔ fv ∈ VLCtx.fvars Δ

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ a, PersistentHashMap.find? lctx.fvarIdToDecl fv = some a) ↔ fv ∈ VLCtx.fvars Δ
Tactic:
exact H.find?_eq_some
State after:
no goals