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

State before:
env : VEnv
Us : List Name
lctx : LocalContext
Δ : VLCtx
fv : FVarId
H : TrLCtx env Us lctx Δ
⊢ (∃ d, LocalContext.find? lctx fv = some d) ↔ fv ∈ VLCtx.fvars Δ
Tactic:
rw [← Option.isSome_iff_exists, H.find?_isSome, Option.isSome_iff_exists, VLCtx.find?_eq_some]
State after:
no goals