From dfca2b0fb95497099e2edd0b4b19f281beb680b7 Mon Sep 17 00:00:00 2001
From: Vincent Beffara <vbeffara@gmail.com>
Date: Thu, 20 Jan 2022 17:46:05 +0000
Subject: [PATCH] feat(data/sym/sym2): add lemma that eq from distinct common
 members (#11563)

Two terms of type `sym2 a` are equal if one can find two distinct elements of type `a` that are members of both.
---
 src/data/sym/sym2.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/data/sym/sym2.lean b/src/data/sym/sym2.lean
index 50689c57a2252..bd9d2a62f46f5 100644
--- a/src/data/sym/sym2.lean
+++ b/src/data/sym/sym2.lean
@@ -216,6 +216,10 @@ begin
   { rintro rfl, simp },
 end
 
+lemma eq_of_ne_mem {x y : α} {z z' : sym2 α} (h : x ≠ y)
+  (h1 : x ∈ z) (h2 : y ∈ z) (h3 : x ∈ z') (h4 : y ∈ z') : z = z' :=
+((mem_and_mem_iff h).mp ⟨h1, h2⟩).trans ((mem_and_mem_iff h).mp ⟨h3, h4⟩).symm
+
 @[ext]
 protected lemma ext (z z' : sym2 α) (h : ∀ x, x ∈ z ↔ x ∈ z') : z = z' :=
 begin