no goals
α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : Multiset.NodupKeys l₁
l₂ : Multiset (Sigma β)
nodupKeys✝ : Multiset.NodupKeys l₂
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }
congr