From 228404dfdc9f825713ff40594ef1f4e89b04fb0d Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sun, 6 Nov 2022 02:20:28 +0000
Subject: [PATCH] chore(data/nat/order): move some results about range succ
 (#17365)

Extracted lemmas that were added in #4199 and #16918.
---
 src/data/nat/order.lean         | 36 --------------------------
 src/data/nat/set.lean           | 46 +++++++++++++++++++++++++++++++++
 src/order/complete_lattice.lean | 15 +++++------
 3 files changed, 52 insertions(+), 45 deletions(-)
 create mode 100644 src/data/nat/set.lean

diff --git a/src/data/nat/order.lean b/src/data/nat/order.lean
index 8b7d5fefd34e0..67c4f7731bb65 100644
--- a/src/data/nat/order.lean
+++ b/src/data/nat/order.lean
@@ -351,42 +351,6 @@ set_induction_bounded hb h_ind (zero_le n)
 lemma set_eq_univ {S : set ℕ} : S = set.univ ↔ 0 ∈ S ∧ ∀ k : ℕ, k ∈ S → k + 1 ∈ S :=
 ⟨by rintro rfl; simp, λ ⟨h0, hs⟩, set.eq_univ_of_forall (set_induction h0 hs)⟩
 
-/-!
-### Recursion and `set.range`
--/
-
-section set
-
-open set
-
-theorem zero_union_range_succ : {0} ∪ range succ = univ :=
-by { ext n, cases n; simp }
-
-@[simp] protected lemma range_succ : range succ = {i | 0 < i} := by ext (_ | i); simp [succ_pos]
-
-variables {α : Type*}
-
-theorem range_of_succ (f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f :=
-by rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-
-theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
-  (set.range (λ n, nat.rec x f n) : set α) =
-    {x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=
-begin
-  convert (range_of_succ _).symm,
-  ext n,
-  induction n with n ihn,
-  { refl },
-  { dsimp at ihn ⊢,
-    rw ihn }
-end
-
-theorem range_cases_on {α : Type*} (x : α) (f : ℕ → α) :
-  (set.range (λ n, nat.cases_on n x f) : set α) = {x} ∪ set.range f :=
-(range_of_succ _).symm
-
-end set
-
 /-! ### `div` -/
 
 
diff --git a/src/data/nat/set.lean b/src/data/nat/set.lean
new file mode 100644
index 0000000000000..3d64d83810525
--- /dev/null
+++ b/src/data/nat/set.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+
+import data.set.basic
+
+/-!
+### Recursion on the natural numbers and `set.range`
+-/
+
+namespace nat
+section set
+
+open set
+
+theorem zero_union_range_succ : {0} ∪ range succ = univ :=
+by { ext n, cases n; simp }
+
+@[simp] protected lemma range_succ : range succ = {i | 0 < i} :=
+by ext (_ | i); simp [succ_pos, succ_ne_zero]
+
+variables {α : Type*}
+
+theorem range_of_succ (f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f :=
+by rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
+
+theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
+  (set.range (λ n, nat.rec x f n) : set α) =
+    {x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=
+begin
+  convert (range_of_succ _).symm,
+  ext n,
+  induction n with n ihn,
+  { refl },
+  { dsimp at ihn ⊢,
+    rw ihn }
+end
+
+theorem range_cases_on {α : Type*} (x : α) (f : ℕ → α) :
+  (set.range (λ n, nat.cases_on n x f) : set α) = {x} ∪ set.range f :=
+(range_of_succ _).symm
+
+end set
+end nat
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index 3b78845d0fc5a..83817a54446ad 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 import data.bool.set
 import data.ulift
-import data.nat.order
+import data.nat.set
 import order.bounds
 
 /-!
@@ -1167,20 +1167,17 @@ end
 @supr_infi_ge_nat_add αᵒᵈ _
 
 lemma sup_supr_nat_succ (u : ℕ → α) : u 0 ⊔ (⨆ i, u (i + 1)) = ⨆ i, u i :=
-begin
-  refine eq_of_forall_ge_iff (λ c, _),
-  simp only [sup_le_iff, supr_le_iff],
-  refine ⟨λ h, _, λ h, ⟨h _, λ i, h _⟩⟩,
-  rintro (_|i),
-  exacts [h.1, h.2 i]
-end
+calc u 0 ⊔ (⨆ i, u (i + 1)) = (⨆ (x ∈ {0} ∪ range nat.succ), u x)
+      : by rw [supr_union, supr_singleton, supr_range]
+... = ⨆ i, u i
+      : by rw [nat.zero_union_range_succ, supr_univ]
 
 lemma inf_infi_nat_succ (u : ℕ → α) : u 0 ⊓ (⨅ i, u (i + 1)) = ⨅ i, u i :=
 @sup_supr_nat_succ αᵒᵈ _ u
 
 lemma infi_nat_gt_zero_eq (f : ℕ → α) :
   (⨅ (i > 0), f i) = ⨅ i, f (i + 1) :=
-by simpa only [(by simp : ∀ i, i > 0 ↔ i ∈ range nat.succ)] using infi_range
+by { rw [←infi_range, nat.range_succ], simp only [mem_set_of] }
 
 lemma supr_nat_gt_zero_eq (f : ℕ → α) :
   (⨆ (i > 0), f i) = ⨆ i, f (i + 1) :=