Theorem: List.nodupkeys_eq_of_mk_mem (LeanSAT/Util/Nodupkeys.lean)

State before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
⊢ b = b'
Tactic:
have goal := nodupkeys_eq_of_fst_eq nd h h' rfl
State after:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : (a, b) = (a, b')
⊢ b = b'

State before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : (a, b) = (a, b')
⊢ b = b'
Tactic:
simp only [Prod.mk.injEq, true_and] at goal
State after:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : b = b'
⊢ b = b'

State before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : b = b'
⊢ b = b'
Tactic:
exact goal
State after:
no goals