no goals
α : Type u
β : α → Type v
l l₁✝ l₂ : List (Sigma β)
inst✝ : DecidableEq α
l₀ l₁ : List (Sigma β)
nd₀ : NodupKeys l₀
nd₁ : NodupKeys l₁
h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁
x✝ : Sigma β
a : α
b : β a
⊢ { fst := a, snd := b } ∈ l₀ ↔ { fst := a, snd := b } ∈ l₁
rw [← mem_dlookup_iff, ← mem_dlookup_iff, h] <;> assumption