From cb132c2ade58f07fe0e074e84901275b912320e4 Mon Sep 17 00:00:00 2001
From: Kexing <kexing.ying19@imperial.ac.uk>
Date: Wed, 18 Aug 2021 15:27:54 +0200
Subject: [PATCH 1/5] initial commit

---
 src/data/nat/pairing.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index cad2491734c7f..267d6895aa791 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -131,4 +131,36 @@ lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
   (⋃ n : ℕ, (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ n, s n).prod (⋃ n, t n) :=
 by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
 
+lemma Union_unpair_union {α} {s t : ℕ → set α} :
+  (⋃ n : ℕ, s n.unpair.1 ∪ t n.unpair.2) = ⋃ i j : ℕ, s i ∪ t j :=
+begin
+  have : (⋃ i : ℕ × ℕ, s i.1 ∪ t i.2) = ⋃ i j : ℕ, s i ∪ t j,
+  { ext, simp },
+  rw [← this, ← nat.surjective_unpair.Union_comp],
+end
+
+lemma Union_unpair_inter {α} {s t : ℕ → set α} :
+  (⋃ n : ℕ, s n.unpair.1 ∩ t n.unpair.2) = ⋃ i j : ℕ, s i ∩ t j :=
+begin
+  have : (⋃ i : ℕ × ℕ, s i.1 ∩ t i.2) = ⋃ i j : ℕ, s i ∩ t j,
+  { ext, simp },
+  rw [← this, ← nat.surjective_unpair.Union_comp],
+end
+
+lemma Inter_unpair_union {α} {s t : ℕ → set α} :
+  (⋂ n : ℕ, s n.unpair.1 ∪ t n.unpair.2) = ⋂ i j : ℕ, s i ∪ t j :=
+begin
+  have : (⋂ i : ℕ × ℕ, s i.1 ∪ t i.2) = ⋂ i j : ℕ, s i ∪ t j,
+  { ext, simp },
+  rw [← this, ← nat.surjective_unpair.Inter_comp],
+end
+
+lemma Inter_unpair_inter {α} {s t : ℕ → set α} :
+  (⋂ n : ℕ, s n.unpair.1 ∩ t n.unpair.2) = ⋂ i j : ℕ, s i ∩ t j :=
+begin
+  have : (⋂ i : ℕ × ℕ, s i.1 ∩ t i.2) = ⋂ i j : ℕ, s i ∩ t j,
+  { ext, simp, },
+  rw [← this, ← nat.surjective_unpair.Inter_comp],
+end
+
 end set

From 4b80f6dab8fb9ce0a812f4cd45da08bcd39ad8ac Mon Sep 17 00:00:00 2001
From: Kexing <kexing.ying19@imperial.ac.uk>
Date: Wed, 18 Aug 2021 17:09:47 +0200
Subject: [PATCH 2/5] generalize and change rhs

---
 src/data/nat/pairing.lean | 42 +++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index 267d6895aa791..1792da9d0eab4 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -131,36 +131,36 @@ lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
   (⋃ n : ℕ, (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ n, s n).prod (⋃ n, t n) :=
 by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
 
-lemma Union_unpair_union {α} {s t : ℕ → set α} :
-  (⋃ n : ℕ, s n.unpair.1 ∪ t n.unpair.2) = ⋃ i j : ℕ, s i ∪ t j :=
+end set
+
+section complete_lattice
+
+lemma supr_unpair_sup {α} [complete_lattice α] {s t : ℕ → α} :
+  (⨆ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨆ i : ℕ, s i) ⊔ ⨆ j, t j :=
 begin
-  have : (⋃ i : ℕ × ℕ, s i.1 ∪ t i.2) = ⋃ i j : ℕ, s i ∪ t j,
-  { ext, simp },
-  rw [← this, ← nat.surjective_unpair.Union_comp],
+  simp_rw [supr_sup, sup_supr, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
+           ← nat.surjective_unpair.supr_comp],
 end
 
-lemma Union_unpair_inter {α} {s t : ℕ → set α} :
-  (⋃ n : ℕ, s n.unpair.1 ∩ t n.unpair.2) = ⋃ i j : ℕ, s i ∩ t j :=
+lemma supr_unpair_inf {α} [complete_distrib_lattice α] {s t : ℕ → α} :
+  (⨆ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨆ i : ℕ, s i) ⊓ ⨆ j, t j :=
 begin
-  have : (⋃ i : ℕ × ℕ, s i.1 ∩ t i.2) = ⋃ i j : ℕ, s i ∩ t j,
-  { ext, simp },
-  rw [← this, ← nat.surjective_unpair.Union_comp],
+  simp_rw [supr_inf_eq, inf_supr_eq, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
+           ← nat.surjective_unpair.supr_comp],
 end
 
-lemma Inter_unpair_union {α} {s t : ℕ → set α} :
-  (⋂ n : ℕ, s n.unpair.1 ∪ t n.unpair.2) = ⋂ i j : ℕ, s i ∪ t j :=
+lemma infi_unpair_sup {α} [complete_distrib_lattice α] {s t : ℕ → α} :
+  (⨅ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨅ i : ℕ, s i) ⊔ ⨅ j, t j :=
 begin
-  have : (⋂ i : ℕ × ℕ, s i.1 ∪ t i.2) = ⋂ i j : ℕ, s i ∪ t j,
-  { ext, simp },
-  rw [← this, ← nat.surjective_unpair.Inter_comp],
+  simp_rw [infi_sup_eq, sup_infi_eq, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
+           ← nat.surjective_unpair.infi_comp],
 end
 
-lemma Inter_unpair_inter {α} {s t : ℕ → set α} :
-  (⋂ n : ℕ, s n.unpair.1 ∩ t n.unpair.2) = ⋂ i j : ℕ, s i ∩ t j :=
+lemma infi_unpair_inf {α} [complete_lattice α] {s t : ℕ → α} :
+  (⨅ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨅ i : ℕ, s i) ⊓ ⨅ j, t j :=
 begin
-  have : (⋂ i : ℕ × ℕ, s i.1 ∩ t i.2) = ⋂ i j : ℕ, s i ∩ t j,
-  { ext, simp, },
-  rw [← this, ← nat.surjective_unpair.Inter_comp],
+  simp_rw [infi_inf, inf_infi, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
+           ← nat.surjective_unpair.infi_comp],
 end
 
-end set
+end complete_lattice

From 0ab470d70c26af00519f0b6d42cb2d33c18e860b Mon Sep 17 00:00:00 2001
From: Kexing <kexing.ying19@imperial.ac.uk>
Date: Wed, 18 Aug 2021 17:23:19 +0200
Subject: [PATCH 3/5] change to supr_unpair and infi unpair

---
 src/data/nat/pairing.lean | 32 ++++++--------------------------
 1 file changed, 6 insertions(+), 26 deletions(-)

diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index 1792da9d0eab4..3f292b2aed738 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -135,32 +135,12 @@ end set
 
 section complete_lattice
 
-lemma supr_unpair_sup {α} [complete_lattice α] {s t : ℕ → α} :
-  (⨆ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨆ i : ℕ, s i) ⊔ ⨆ j, t j :=
-begin
-  simp_rw [supr_sup, sup_supr, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
-           ← nat.surjective_unpair.supr_comp],
-end
-
-lemma supr_unpair_inf {α} [complete_distrib_lattice α] {s t : ℕ → α} :
-  (⨆ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨆ i : ℕ, s i) ⊓ ⨆ j, t j :=
-begin
-  simp_rw [supr_inf_eq, inf_supr_eq, ← (supr_prod : (⨆ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
-           ← nat.surjective_unpair.supr_comp],
-end
+lemma supr_unpair {α} [complete_lattice α] (f : ℕ → ℕ → α) :
+  (⨆ n : ℕ, f n.unpair.1 n.unpair.2) = ⨆ i j : ℕ, f i j :=
+by rw [← (supr_prod : (⨆ i : ℕ × ℕ, f i.1 i.2) = _), ← nat.surjective_unpair.supr_comp]
 
-lemma infi_unpair_sup {α} [complete_distrib_lattice α] {s t : ℕ → α} :
-  (⨅ n : ℕ, s n.unpair.1 ⊔ t n.unpair.2) = (⨅ i : ℕ, s i) ⊔ ⨅ j, t j :=
-begin
-  simp_rw [infi_sup_eq, sup_infi_eq, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊔ t i.2) = _),
-           ← nat.surjective_unpair.infi_comp],
-end
-
-lemma infi_unpair_inf {α} [complete_lattice α] {s t : ℕ → α} :
-  (⨅ n : ℕ, s n.unpair.1 ⊓ t n.unpair.2) = (⨅ i : ℕ, s i) ⊓ ⨅ j, t j :=
-begin
-  simp_rw [infi_inf, inf_infi, ← (infi_prod : (⨅ i : ℕ × ℕ, s i.1 ⊓ t i.2) = _),
-           ← nat.surjective_unpair.infi_comp],
-end
+lemma infi_unpair {α} [complete_lattice α] (f : ℕ → ℕ → α) :
+  (⨅ n : ℕ, f n.unpair.1 n.unpair.2) = ⨅ i j : ℕ, f i j :=
+by rw [← (infi_prod : (⨅ i : ℕ × ℕ, f i.1 i.2) = _), ← nat.surjective_unpair.infi_comp]
 
 end complete_lattice

From 16d2b83044d371b20d65a147a66dcb93f944fca6 Mon Sep 17 00:00:00 2001
From: Kexing <kexing.ying19@imperial.ac.uk>
Date: Wed, 18 Aug 2021 17:28:34 +0200
Subject: [PATCH 4/5] golf

---
 src/data/nat/pairing.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index 3f292b2aed738..ca6676202ab20 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -141,6 +141,6 @@ by rw [← (supr_prod : (⨆ i : ℕ × ℕ, f i.1 i.2) = _), ← nat.surjective
 
 lemma infi_unpair {α} [complete_lattice α] (f : ℕ → ℕ → α) :
   (⨅ n : ℕ, f n.unpair.1 n.unpair.2) = ⨅ i j : ℕ, f i j :=
-by rw [← (infi_prod : (⨅ i : ℕ × ℕ, f i.1 i.2) = _), ← nat.surjective_unpair.infi_comp]
+supr_unpair (show ℕ → ℕ → order_dual α, from f)
 
 end complete_lattice

From cdf93271470a9eee5d41bd376ccbb615d280b4e0 Mon Sep 17 00:00:00 2001
From: Kexing <kexing.ying19@imperial.ac.uk>
Date: Wed, 18 Aug 2021 19:37:24 +0200
Subject: [PATCH 5/5] add set version

---
 src/data/nat/pairing.lean | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean
index ca6676202ab20..070f78b56d355 100644
--- a/src/data/nat/pairing.lean
+++ b/src/data/nat/pairing.lean
@@ -125,14 +125,6 @@ end
 end nat
 open nat
 
-namespace set
-
-lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
-  (⋃ n : ℕ, (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ n, s n).prod (⋃ n, t n) :=
-by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
-
-end set
-
 section complete_lattice
 
 lemma supr_unpair {α} [complete_lattice α] (f : ℕ → ℕ → α) :
@@ -144,3 +136,19 @@ lemma infi_unpair {α} [complete_lattice α] (f : ℕ → ℕ → α) :
 supr_unpair (show ℕ → ℕ → order_dual α, from f)
 
 end complete_lattice
+
+namespace set
+
+lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
+  (⋃ n : ℕ, (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ n, s n).prod (⋃ n, t n) :=
+by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
+
+lemma Union_unpair {α} (f : ℕ → ℕ → set α) :
+  (⋃ n : ℕ, f n.unpair.1 n.unpair.2) = ⋃ i j : ℕ, f i j :=
+supr_unpair f
+
+lemma Inter_unpair {α} (f : ℕ → ℕ → set α) :
+  (⋂ n : ℕ, f n.unpair.1 n.unpair.2) = ⋂ i j : ℕ, f i j :=
+infi_unpair f
+
+end set