bump to nightly-2023-05-28-12

mathlib commit leanprover-community/mathlib@917c3c0

Mathbin/CategoryTheory/Bicategory/Coherence.lean

@@ -56,20 +56,25 @@ namespace FreeBicategory
 
 variable {B : Type u} [Quiver.{v + 1} B]
 
+#print CategoryTheory.FreeBicategory.inclusionPathAux /-
 /-- Auxiliary definition for `inclusion_path`. -/
 @[simp]
 def inclusionPathAux {a : B} : ∀ {b : B}, Path a b → Hom a b
   | _, nil => Hom.id a
   | _, cons p f => (inclusion_path_aux p).comp (Hom.of f)
 #align category_theory.free_bicategory.inclusion_path_aux CategoryTheory.FreeBicategory.inclusionPathAux
+-/
 
+#print CategoryTheory.FreeBicategory.inclusionPath /-
 /-- The discrete category on the paths includes into the category of 1-morphisms in the free
 bicategory.
 -/
 def inclusionPath (a b : B) : Discrete (Path.{v + 1} a b) ⥤ Hom a b :=
   Discrete.functor inclusionPathAux
 #align category_theory.free_bicategory.inclusion_path CategoryTheory.FreeBicategory.inclusionPath
+-/
 
+#print CategoryTheory.FreeBicategory.preinclusion /-
 /-- The inclusion from the locally discrete bicategory on the path category into the free bicategory
 as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem.
 See `inclusion`.
@@ -81,6 +86,7 @@ def preinclusion (B : Type u) [Quiver.{v + 1} B] :
   map a b := (inclusionPath a b).obj
   zipWith a b f g η := (inclusionPath a b).map η
 #align category_theory.free_bicategory.preinclusion CategoryTheory.FreeBicategory.preinclusion
+-/
 
 @[simp]
 theorem preinclusion_obj (a : B) : (preinclusion B).obj a = a :=
@@ -96,6 +102,7 @@ theorem preinclusion_map₂ {a b : B} (f g : Discrete (Path.{v + 1} a b)) (η :
   exact (inclusion_path a b).map_id _
 #align category_theory.free_bicategory.preinclusion_map₂ CategoryTheory.FreeBicategory.preinclusion_map₂
 
+#print CategoryTheory.FreeBicategory.normalizeAux /-
 /-- The normalization of the composition of `p : path a b` and `f : hom b c`.
 `p` will eventually be taken to be `nil` and we then get the normalization
 of `f` alone, but the auxiliary `p` is necessary for Lean to accept the definition of
@@ -107,6 +114,7 @@ def normalizeAux {a : B} : ∀ {b c : B}, Path a b → Hom b c → Path a c
   | _, _, p, hom.id b => p
   | _, _, p, hom.comp f g => normalize_aux (normalize_aux p f) g
 #align category_theory.free_bicategory.normalize_aux CategoryTheory.FreeBicategory.normalizeAux
+-/
 
 /-
 We may define
@@ -140,6 +148,7 @@ def normalizeIso {a : B} :
     (α_ _ _ _).symm ≪≫ whiskerRightIso (normalize_iso p f) g ≪≫ normalize_iso (normalizeAux p f) g
 #align category_theory.free_bicategory.normalize_iso CategoryTheory.FreeBicategory.normalizeIso
 
+#print CategoryTheory.FreeBicategory.normalizeAux_congr /-
 /-- Given a 2-morphism between `f` and `g` in the free bicategory, we have the equality
 `normalize_aux p f = normalize_aux p g`.
 -/
@@ -156,6 +165,7 @@ theorem normalizeAux_congr {a b c : B} (p : Path a b) {f g : Hom b c} (η : f 
   case whisker_right _ _ _ _ _ _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih p) rfl
   all_goals funext; rfl
 #align category_theory.free_bicategory.normalize_aux_congr CategoryTheory.FreeBicategory.normalizeAux_congr
+-/
 
 /-- The 2-isomorphism `normalize_iso p f` is natural in `f`. -/
 theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
@@ -183,6 +193,7 @@ theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f
   all_goals dsimp; dsimp [id_def, comp_def]; simp
 #align category_theory.free_bicategory.normalize_naturality CategoryTheory.FreeBicategory.normalize_naturality
 
+#print CategoryTheory.FreeBicategory.normalizeAux_nil_comp /-
 @[simp]
 theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
     normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g) :=
@@ -192,7 +203,9 @@ theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
   case of => rfl
   case comp _ _ _ g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
 #align category_theory.free_bicategory.normalize_aux_nil_comp CategoryTheory.FreeBicategory.normalizeAux_nil_comp
+-/
 
+#print CategoryTheory.FreeBicategory.normalize /-
 /-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/
 def normalize (B : Type u) [Quiver.{v + 1} B] :
     Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B))
@@ -203,7 +216,9 @@ def normalize (B : Type u) [Quiver.{v + 1} B] :
   map_id a := eqToIso <| Discrete.ext _ _ rfl
   map_comp a b c f g := eqToIso <| Discrete.ext _ _ <| normalizeAux_nil_comp f g
 #align category_theory.free_bicategory.normalize CategoryTheory.FreeBicategory.normalize
+-/
 
+#print CategoryTheory.FreeBicategory.normalizeUnitIso /-
 /-- Auxiliary definition for `normalize_equiv`. -/
 def normalizeUnitIso (a b : FreeBicategory B) :
     𝟭 (a ⟶ b) ≅ (normalize B).mapFunctor a b ⋙ inclusionPath a b :=
@@ -214,17 +229,20 @@ def normalizeUnitIso (a b : FreeBicategory B) :
       congr 1
       exact normalize_naturality nil η)
 #align category_theory.free_bicategory.normalize_unit_iso CategoryTheory.FreeBicategory.normalizeUnitIso
+-/
 
 /-- Normalization as an equivalence of categories. -/
 def normalizeEquiv (a b : B) : Hom a b ≌ Discrete (Path.{v + 1} a b) :=
   Equivalence.mk ((normalize _).mapFunctor a b) (inclusionPath a b) (normalizeUnitIso a b)
     (Discrete.natIso fun f => eqToIso (by induction f <;> induction f <;> tidy))
 #align category_theory.free_bicategory.normalize_equiv CategoryTheory.FreeBicategory.normalizeEquiv
 
+#print CategoryTheory.FreeBicategory.locally_thin /-
 /-- The coherence theorem for bicategories. -/
 instance locally_thin {a b : FreeBicategory B} : Quiver.IsThin (a ⟶ b) := fun _ _ =>
   ⟨fun η θ => (normalizeEquiv a b).Functor.map_injective (Subsingleton.elim _ _)⟩
 #align category_theory.free_bicategory.locally_thin CategoryTheory.FreeBicategory.locally_thin
+-/
 
 /-- Auxiliary definition for `inclusion`. -/
 def inclusionMapCompAux {a b : B} :
@@ -234,6 +252,7 @@ def inclusionMapCompAux {a b : B} :
   | _, f, cons g₁ g₂ => whiskerRightIso (inclusion_map_comp_aux f g₁) (Hom.of g₂) ≪≫ α_ _ _ _
 #align category_theory.free_bicategory.inclusion_map_comp_aux CategoryTheory.FreeBicategory.inclusionMapCompAux
 
+#print CategoryTheory.FreeBicategory.inclusion /-
 /-- The inclusion pseudofunctor from the locally discrete bicategory on the path category into the
 free bicategory.
 -/
@@ -245,6 +264,7 @@ def inclusion (B : Type u) [Quiver.{v + 1} B] :
     map_id := fun a => Iso.refl (𝟙 a)
     map_comp := fun a b c f g => inclusionMapCompAux f.as g.as }
 #align category_theory.free_bicategory.inclusion CategoryTheory.FreeBicategory.inclusion
+-/
 
 end FreeBicategory
 

Mathbin/Computability/Primrec.lean

@@ -1399,12 +1399,12 @@ instance array {n} : Primcodable (Array' n α) :=
   ofEquiv _ (Equiv.arrayEquivFin _ _)
 #align primcodable.array Primcodable.array
 
-section Ulower
+section ULower
 
 attribute [local instance 100] Encodable.decidableRangeEncode Encodable.decidableEqOfEncodable
 
 #print Primcodable.ulower /-
-instance ulower : Primcodable (Ulower α) :=
+instance ulower : Primcodable (ULower α) :=
   have : PrimrecPred fun n => Encodable.decode₂ α n ≠ none :=
     PrimrecPred.not
       (Primrec.eq.comp
@@ -1416,7 +1416,7 @@ instance ulower : Primcodable (Ulower α) :=
 #align primcodable.ulower Primcodable.ulower
 -/
 
-end Ulower
+end ULower
 
 end Primcodable
 
@@ -1471,14 +1471,14 @@ theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} :
 -/
 
 #print Primrec.ulower_down /-
-theorem ulower_down : Primrec (Ulower.down : α → Ulower α) :=
+theorem ulower_down : Primrec (ULower.down : α → ULower α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidable_range_encode _
   subtype_mk Primrec.encode
 #align primrec.ulower_down Primrec.ulower_down
 -/
 
 #print Primrec.ulower_up /-
-theorem ulower_up : Primrec (Ulower.up : Ulower α → α) :=
+theorem ulower_up : Primrec (ULower.up : ULower α → α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidable_range_encode _
   option_get (primrec.decode₂.comp subtype_val)
 #align primrec.ulower_up Primrec.ulower_up

Mathbin/Computability/Reduce.lean

@@ -317,16 +317,16 @@ theorem OneOneEquiv.congr_right {α β γ} [Primcodable α] [Primcodable β] [Pr
   and_congr h.le_congr_right h.le_congr_left
 #align one_one_equiv.congr_right OneOneEquiv.congr_right
 
-#print Ulower.down_computable /-
+#print ULower.down_computable /-
 @[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
 -/
 
 #print manyOneEquiv_up /-
-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
 -/
 

Mathbin/Logic/Encodable/Basic.lean

@@ -592,85 +592,85 @@ instance : Countable ℕ+ :=
   Subtype.countable
 
 -- short-circuit instance search
-section Ulower
+section ULower
 
 attribute [local instance 100] Encodable.decidableRangeEncode
 
-#print Ulower /-
+#print ULower /-
 /-- `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 : α → ℕ)deriving DecidableEq, Encodable
-#align ulower Ulower
+#align ulower ULower
 -/
 
-end Ulower
+end ULower
 
-namespace Ulower
+namespace ULower
 
 variable (α : Type _) [Encodable α]
 
-#print Ulower.equiv /-
+#print ULower.equiv /-
 /-- The equivalence between the encodable type `α` and `ulower α : Type`. -/
-def equiv : α ≃ Ulower α :=
+def equiv : α ≃ ULower α :=
   Encodable.equivRangeEncode α
-#align ulower.equiv Ulower.equiv
+#align ulower.equiv ULower.equiv
 -/
 
 variable {α}
 
-#print Ulower.down /-
+#print ULower.down /-
 /-- Lowers an `a : α` into `ulower α`. -/
-def down (a : α) : 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⟩
 
-#print Ulower.up /-
+#print ULower.up /-
 /-- Lifts an `a : ulower α` into `α`. -/
-def up (a : Ulower α) : α :=
+def up (a : ULower α) : α :=
   (equiv α).symm a
-#align ulower.up Ulower.up
+#align ulower.up ULower.up
 -/
 
-#print Ulower.down_up /-
+#print ULower.down_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
 -/
 
-#print Ulower.up_down /-
+#print ULower.up_down /-
 @[simp]
 theorem up_down {a : α} : (down a).up = a :=
   Equiv.left_inv _ _
-#align ulower.up_down Ulower.up_down
+#align ulower.up_down ULower.up_down
 -/
 
-#print Ulower.up_eq_up /-
+#print ULower.up_eq_up /-
 @[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
 -/
 
-#print Ulower.down_eq_down /-
+#print ULower.down_eq_down /-
 @[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
 -/
 
-#print Ulower.ext /-
+#print ULower.ext /-
 @[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.

Mathbin/Topology/Partial.lean

@@ -61,19 +61,19 @@ theorem ptendsto'_nhds {f : β →. α} {l : Filter β} {a : α} :
 
 variable [TopologicalSpace β]
 
-#print Pcontinuous /-
+#print PContinuous /-
 /-- Continuity of a partial function -/
-def Pcontinuous (f : α →. β) :=
+def PContinuous (f : α →. β) :=
   ∀ s, IsOpen s → IsOpen (f.Preimage s)
-#align pcontinuous Pcontinuous
+#align pcontinuous PContinuous
 -/
 
-theorem open_dom_of_pcontinuous {f : α →. β} (h : Pcontinuous f) : IsOpen f.Dom := by
+theorem open_dom_of_pcontinuous {f : α →. β} (h : PContinuous f) : IsOpen f.Dom := by
   rw [← PFun.preimage_univ] <;> exact h _ isOpen_univ
 #align open_dom_of_pcontinuous open_dom_of_pcontinuous
 
 theorem pcontinuous_iff' {f : α →. β} :
-    Pcontinuous f ↔ ∀ {x y} (h : y ∈ f x), Ptendsto' f (𝓝 x) (𝓝 y) :=
+    PContinuous f ↔ ∀ {x y} (h : y ∈ f x), Ptendsto' f (𝓝 x) (𝓝 y) :=
   by
   constructor
   · intro h x y h'

Mathbin/Topology/Sheaves/SheafOfFunctions.lean

@@ -49,14 +49,15 @@ open TopCat
 
 namespace TopCat.Presheaf
 
+#print TopCat.Presheaf.toTypes_isSheaf /-
 /-- We show that the presheaf of functions to a type `T`
 (no continuity assumptions, just plain functions)
 form a sheaf.
 
 In fact, the proof is identical when we do this for dependent functions to a type family `T`,
 so we do the more general case.
 -/
-theorem to_Types_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
+theorem toTypes_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
   isSheaf_of_isSheafUniqueGluing_types _ fun ι U sf hsf =>
     -- We use the sheaf condition in terms of unique gluing
   -- U is a family of open sets, indexed by `ι` and `sf` is a compatible family of sections.
@@ -88,32 +89,41 @@ theorem to_Types_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
       convert congr_fun (ht (index x)) ⟨x.1, index_spec x⟩
       ext
       rfl
-#align Top.presheaf.to_Types_is_sheaf TopCat.Presheaf.to_Types_isSheaf
+#align Top.presheaf.to_Types_is_sheaf TopCat.Presheaf.toTypes_isSheaf
+-/
 
+#print TopCat.Presheaf.toType_isSheaf /-
 -- We verify that the non-dependent version is an immediate consequence:
 /-- The presheaf of not-necessarily-continuous functions to
 a target type `T` satsifies the sheaf condition.
 -/
-theorem to_Type_isSheaf (T : Type u) : (presheafToType X T).IsSheaf :=
-  to_Types_isSheaf X fun _ => T
-#align Top.presheaf.to_Type_is_sheaf TopCat.Presheaf.to_Type_isSheaf
+theorem toType_isSheaf (T : Type u) : (presheafToType X T).IsSheaf :=
+  toTypes_isSheaf X fun _ => T
+#align Top.presheaf.to_Type_is_sheaf TopCat.Presheaf.toType_isSheaf
+-/
 
 end TopCat.Presheaf
 
 namespace TopCat
 
+#print TopCat.sheafToTypes /-
 /-- The sheaf of not-necessarily-continuous functions on `X` with values in type family
 `T : X → Type u`.
 -/
 def sheafToTypes (T : X → Type u) : Sheaf (Type u) X :=
-  ⟨presheafToTypes X T, Presheaf.to_Types_isSheaf _ _⟩
+  ⟨presheafToTypes X T, Presheaf.toTypes_isSheaf _ _⟩
 #align Top.sheaf_to_Types TopCat.sheafToTypes
+-/
 
+/- warning: Top.sheaf_to_Type clashes with Top.sheafToType -> TopCat.sheafToType
+Case conversion may be inaccurate. Consider using '#align Top.sheaf_to_Type TopCat.sheafToTypeₓ'. -/
+#print TopCat.sheafToType /-
 /-- The sheaf of not-necessarily-continuous functions on `X` with values in a type `T`.
 -/
 def sheafToType (T : Type u) : Sheaf (Type u) X :=
-  ⟨presheafToType X T, Presheaf.to_Type_isSheaf _ _⟩
+  ⟨presheafToType X T, Presheaf.toType_isSheaf _ _⟩
 #align Top.sheaf_to_Type TopCat.sheafToType
+-/
 
 end TopCat