From f93df69aa733b384239a72b5f814542bcc50caf4 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 28 May 2023 08:49:44 +0000
Subject: [PATCH] chore: rename `Ulower` to `ULower` (#4430)

ref #4354
---
 Mathlib/Computability/Primrec.lean | 10 ++---
 Mathlib/Computability/Reduce.lean  |  8 ++--
 Mathlib/Logic/Encodable/Basic.lean | 60 +++++++++++++++---------------
 3 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean
index 4c8fbb042b410..2914096c2cdf2 100644
--- a/Mathlib/Computability/Primrec.lean
+++ b/Mathlib/Computability/Primrec.lean
@@ -1195,7 +1195,7 @@ instance finArrow {n} : Primcodable (Fin n → α) :=
 --   ofEquiv _ (Equiv.arrayEquivFin _ _)
 -- #align primcodable.array Primcodable.array
 
-section Ulower
+section ULower
 
 attribute [local instance] Encodable.decidableRangeEncode Encodable.decidableEqOfEncodable
 
@@ -1209,11 +1209,11 @@ theorem mem_range_encode : PrimrecPred (fun n => n ∈ Set.range (encode : α 
         (.const _))
   this.of_eq fun _ => decode₂_ne_none_iff
 
-instance ulower : Primcodable (Ulower α) :=
+instance ulower : Primcodable (ULower α) :=
   Primcodable.subtype mem_range_encode
 #align primcodable.ulower Primcodable.ulower
 
-end Ulower
+end ULower
 
 end Primcodable
 
@@ -1256,13 +1256,13 @@ theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} :
   cases x <;> simp
 #align primrec.option_get Primrec.option_get
 
-theorem ulower_down : Primrec (Ulower.down : α → Ulower α) :=
+theorem ulower_down : Primrec (ULower.down : α → ULower α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
   subtype_mk .encode
 
 #align primrec.ulower_down Primrec.ulower_down
 
-theorem ulower_up : Primrec (Ulower.up : Ulower α → α) :=
+theorem ulower_up : Primrec (ULower.up : ULower α → α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
   option_get (Primrec.decode₂.comp subtype_val)
 #align primrec.ulower_up Primrec.ulower_up
diff --git a/Mathlib/Computability/Reduce.lean b/Mathlib/Computability/Reduce.lean
index 87a6cc991f652..61bfb5b4ae749 100644
--- a/Mathlib/Computability/Reduce.lean
+++ b/Mathlib/Computability/Reduce.lean
@@ -285,12 +285,12 @@ theorem OneOneEquiv.congr_right {α β γ} [Primcodable α] [Primcodable β] [Pr
 #align one_one_equiv.congr_right OneOneEquiv.congr_right
 
 @[simp]
-theorem Ulower.down_computable {α} [Primcodable α] : (Ulower.equiv α).Computable :=
+theorem ULower.down_computable {α} [Primcodable α] : (ULower.equiv α).Computable :=
   ⟨Primrec.ulower_down.to_comp, Primrec.ulower_up.to_comp⟩
-#align ulower.down_computable Ulower.down_computable
+#align ulower.down_computable ULower.down_computable
 
-theorem manyOneEquiv_up {α} [Primcodable α] {p : α → Prop} : ManyOneEquiv (p ∘ Ulower.up) p :=
-  ManyOneEquiv.of_equiv Ulower.down_computable.symm
+theorem manyOneEquiv_up {α} [Primcodable α] {p : α → Prop} : ManyOneEquiv (p ∘ ULower.up) p :=
+  ManyOneEquiv.of_equiv ULower.down_computable.symm
 #align many_one_equiv_up manyOneEquiv_up
 
 -- mathport name: «expr ⊕' »
diff --git a/Mathlib/Logic/Encodable/Basic.lean b/Mathlib/Logic/Encodable/Basic.lean
index d6ff735d71da4..bf2dddd5a142d 100644
--- a/Mathlib/Logic/Encodable/Basic.lean
+++ b/Mathlib/Logic/Encodable/Basic.lean
@@ -30,8 +30,8 @@ The difference with `Denumerable` is that finite types are encodable. For infini
   partial inverse `decode : ℕ → Option α`.
 * `decode₂`: Version of `decode` that is equal to `none` outside of the range of `encode`. Useful as
   we do not require this in the definition of `decode`.
-* `Ulower α`: Any encodable type has an equivalent type living in the lowest universe, namely a
-  subtype of `ℕ`. `Ulower α` finds it.
+* `ULower α`: Any encodable type has an equivalent type living in the lowest universe, namely a
+  subtype of `ℕ`. `ULower α` finds it.
 
 ## Implementation notes
 
@@ -479,73 +479,73 @@ theorem nonempty_encodable (α : Type _) [Countable α] : Nonempty (Encodable α
 instance : Countable ℕ+ := by delta PNat; infer_instance
 
 -- short-circuit instance search
-section Ulower
+section ULower
 
 attribute [local instance] Encodable.decidableRangeEncode
 
 /-- `ULower α : Type` is an equivalent type in the lowest universe, given `Encodable α`. -/
-def Ulower (α : Type _) [Encodable α] : Type :=
+def ULower (α : Type _) [Encodable α] : Type :=
   Set.range (Encodable.encode : α → ℕ)
-#align ulower Ulower
+#align ulower ULower
 
-instance {α : Type _} [Encodable α] : DecidableEq (Ulower α) :=
-  by delta Ulower; exact Encodable.decidableEqOfEncodable _
+instance {α : Type _} [Encodable α] : DecidableEq (ULower α) :=
+  by delta ULower; exact Encodable.decidableEqOfEncodable _
 
-instance {α : Type _} [Encodable α] : Encodable (Ulower α) :=
-  by delta Ulower; infer_instance
+instance {α : Type _} [Encodable α] : Encodable (ULower α) :=
+  by delta ULower; infer_instance
 
-end Ulower
+end ULower
 
-namespace Ulower
+namespace ULower
 
 variable (α : Type _) [Encodable α]
 
-/-- The equivalence between the encodable type `α` and `Ulower α : Type`. -/
-def equiv : α ≃ Ulower α :=
+/-- The equivalence between the encodable type `α` and `ULower α : Type`. -/
+def equiv : α ≃ ULower α :=
   Encodable.equivRangeEncode α
-#align ulower.equiv Ulower.equiv
+#align ulower.equiv ULower.equiv
 
 variable {α}
 
-/-- Lowers an `a : α` into `Ulower α`. -/
-def down (a : α) : Ulower α :=
+/-- Lowers an `a : α` into `ULower α`. -/
+def down (a : α) : ULower α :=
   equiv α a
-#align ulower.down Ulower.down
+#align ulower.down ULower.down
 
-instance [Inhabited α] : Inhabited (Ulower α) :=
+instance [Inhabited α] : Inhabited (ULower α) :=
   ⟨down default⟩
 
-/-- Lifts an `a : Ulower α` into `α`. -/
-def up (a : Ulower α) : α :=
+/-- Lifts an `a : ULower α` into `α`. -/
+def up (a : ULower α) : α :=
   (equiv α).symm a
-#align ulower.up Ulower.up
+#align ulower.up ULower.up
 
 @[simp]
-theorem down_up {a : Ulower α} : down a.up = a :=
+theorem down_up {a : ULower α} : down a.up = a :=
   Equiv.right_inv _ _
-#align ulower.down_up Ulower.down_up
+#align ulower.down_up ULower.down_up
 
 @[simp]
 theorem up_down {a : α} : (down a).up = a := by
   simp [up, down,Equiv.left_inv _ _, Equiv.symm_apply_apply]
-#align ulower.up_down Ulower.up_down
+#align ulower.up_down ULower.up_down
 
 @[simp]
-theorem up_eq_up {a b : Ulower α} : a.up = b.up ↔ a = b :=
+theorem up_eq_up {a b : ULower α} : a.up = b.up ↔ a = b :=
   Equiv.apply_eq_iff_eq _
-#align ulower.up_eq_up Ulower.up_eq_up
+#align ulower.up_eq_up ULower.up_eq_up
 
 @[simp]
 theorem down_eq_down {a b : α} : down a = down b ↔ a = b :=
   Equiv.apply_eq_iff_eq _
-#align ulower.down_eq_down Ulower.down_eq_down
+#align ulower.down_eq_down ULower.down_eq_down
 
 @[ext]
-protected theorem ext {a b : Ulower α} : a.up = b.up → a = b :=
+protected theorem ext {a b : ULower α} : a.up = b.up → a = b :=
   up_eq_up.1
-#align ulower.ext Ulower.ext
+#align ulower.ext ULower.ext
 
-end Ulower
+end ULower
 
 /-
 Choice function for encodable types and decidable predicates.