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

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ find? t x = some v ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
simp [find?, findEntry?_some]
State after:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
constructor
State after:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq

case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

State before:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
rintro ⟨_, h, rfl⟩
State after:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ toList t ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ toList t ∧ cmp x y = Ordering.eq

State before:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ toList t ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ toList t ∧ cmp x y = Ordering.eq
Tactic:
exact ⟨_, h⟩
State after:
no goals

State before:
case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ toList t ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Tactic:
rintro ⟨b, h⟩
State after:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ toList t ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

State before:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ toList t ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ toList t ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v
Tactic:
exact ⟨_, h, rfl⟩
State after:
no goals