Theorem: Lean4Lean.VLCtx.lookup_eq_some (Lean4Lean/Verify/VLCtx.lean)

State before:
fv : FVarId
⊢ (∃ x, List.lookup (some fv) [] = some x) ↔ fv ∈ fvars []
Tactic:
simp
State after:
no goals

State before:
fv : FVarId
ofv : Option FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ (∃ x, List.lookup (some fv) ((ofv, d) :: Δ) = some x) ↔ fv ∈ fvars ((ofv, d) :: Δ)
Tactic:
cases ofv with
| none => simp [List.lookup, show (some fv == none) = false from rfl, lookup_eq_some]
| some fv' =>
  simp [List.lookup, show (some fv == some fv') = (fv == fv') from rfl]
  cases e : fv == fv' <;> simp at e <;> simp [e, lookup_eq_some]
State after:
no goals

State before:
case none
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
⊢ (∃ x, List.lookup (some fv) ((none, d) :: Δ) = some x) ↔ fv ∈ fvars ((none, d) :: Δ)
Tactic:
simp [List.lookup, show (some fv == none) = false from rfl, lookup_eq_some]
State after:
no goals

State before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x, List.lookup (some fv) ((some fv', d) :: Δ) = some x) ↔ fv ∈ fvars ((some fv', d) :: Δ)
Tactic:
simp [List.lookup, show (some fv == some fv') = (fv == fv') from rfl]
State after:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x,
      (match fv == fv' with
        | true => some d
        | false => List.lookup (some fv) Δ) =
        some x) ↔
    fv = fv' ∨ fv ∈ fvars Δ

State before:
case some
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
fv' : FVarId
⊢ (∃ x,
      (match fv == fv' with
        | true => some d
        | false => List.lookup (some fv) Δ) =
        some x) ↔
    fv = fv' ∨ fv ∈ fvars Δ
Tactic:
cases e : fv == fv' <;> simp at e <;> simp [e, lookup_eq_some]
State after:
no goals