Theorem: Std.RBNode.min?_mem (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
a : α
t : RBNode α
h : RBNode.min? t = some a
⊢ a ∈ t
Tactic:
rw [min?_eq_toList_head?] at h
State after:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ t

State before:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ t
Tactic:
rw [← mem_toList]
State after:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ toList t

State before:
α : Type u_1
a : α
t : RBNode α
h : List.head? (toList t) = some a
⊢ a ∈ toList t
Tactic:
revert h
State after:
α : Type u_1
a : α
t : RBNode α
⊢ List.head? (toList t) = some a → a ∈ toList t

State before:
α : Type u_1
a : α
t : RBNode α
⊢ List.head? (toList t) = some a → a ∈ toList t
Tactic:
cases toList t <;> rintro ⟨⟩
State after:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝

State before:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝
Tactic:
constructor
State after:
no goals