Theorem: Std.RBMap.find?_some_mem_toList (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
v : β
t : RBMap α β cmp
h : find? t x = some v
⊢ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some'.1 h
State after:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : findEntry? t x = some (y, v)
h : find? t x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ toList t ∧ cmp x y_1 = Ordering.eq

State before:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : findEntry? t x = some (y, v)
h : find? t x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ toList t ∧ cmp x y_1 = Ordering.eq
Tactic:
exact ⟨_, findEntry?_some_mem_toList h', findEntry?_some_eq_eq h'⟩
State after:
no goals