chore: tidy various files (#4997)

Author: Ruben-VandeVelde

Mathlib/Algebra/Order/CompleteField.lean

@@ -17,8 +17,8 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 This file shows that the reals are unique, or, more formally, given a type satisfying the common
 axioms of the reals (field, conditionally complete, linearly ordered) that there is an isomorphism
-preserving these properties to the reals. This is `rat.induced_order_ring_iso`. Moreover this
-isomorphism is unique.
+preserving these properties to the reals. This is `LinearOrderedField.inducedOrderRingIso` for `ℚ`.
+Moreover this isomorphism is unique.
 
 We introduce definitions of conditionally complete linear ordered fields, and show all such are
 archimedean. We also construct the natural map from a `LinearOrderedField` to such a field.
@@ -79,7 +79,7 @@ instance (priority := 100) ConditionallyCompleteLinearOrderedField.to_archimedea
 
 /-- The reals are a conditionally complete linearly ordered field. -/
 instance : ConditionallyCompleteLinearOrderedField ℝ :=
-  { (inferInstance : LinearOrderedField  ℝ),
+  { (inferInstance : LinearOrderedField ℝ),
     (inferInstance : ConditionallyCompleteLinearOrder ℝ) with }
 
 namespace LinearOrderedField
@@ -290,8 +290,8 @@ theorem exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (ha : 0 < a) (b : 
 variable (α β)
 
 /-- `inducedMap` as an additive homomorphism. -/
-def inducedAddHom : α →+ β := by
-  refine ⟨⟨inducedMap α β, inducedMap_zero α β⟩, inducedMap_add α β⟩
+def inducedAddHom : α →+ β :=
+  ⟨⟨inducedMap α β, inducedMap_zero α β⟩, inducedMap_add α β⟩
 #align linear_ordered_field.induced_add_hom LinearOrderedField.inducedAddHom
 
 /-- `inducedMap` as an `OrderRingHom`. -/

Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

@@ -42,7 +42,7 @@ def punitEquivDiscretePUnit : FundamentalGroupoid PUnit.{u + 1} ≌ Discrete PUn
   CategoryTheory.Equivalence.mk (Functor.star _) ((CategoryTheory.Functor.const _).obj PUnit.unit)
     -- Porting note: was `by decide`
     (NatIso.ofComponents fun _ => eqToIso (by simp))
-    (Functor.pUnitExt _ _)
+    (Functor.punitExt _ _)
 #align fundamental_groupoid.punit_equiv_discrete_punit FundamentalGroupoid.punitEquivDiscretePUnit
 
 end FundamentalGroupoid

Mathlib/CategoryTheory/Closed/Zero.lean

@@ -63,14 +63,14 @@ attribute [local instance] uniqueHomsetOfZero
 /-- A cartesian closed category with a zero object is equivalent to the category with one object and
 one morphism.
 -/
-def equivPunit [HasZeroObject C] : C ≌ Discrete PUnit :=
+def equivPUnit [HasZeroObject C] : C ≌ Discrete PUnit :=
   Equivalence.mk (Functor.star C) (Functor.fromPUnit 0)
     (NatIso.ofComponents
       (fun X =>
         { hom := default
           inv := default })
       fun f => Subsingleton.elim _ _)
-    (Functor.pUnitExt _ _)
-#align category_theory.equiv_punit CategoryTheory.equivPunit
+    (Functor.punitExt _ _)
+#align category_theory.equiv_punit CategoryTheory.equivPUnit
 
 end CategoryTheory

Mathlib/CategoryTheory/IsConnected.lean

@@ -306,13 +306,13 @@ theorem equiv_relation [IsConnected J] (r : J → J → Prop) (hr : _root_.Equiv
   apply hr.3 (hr.2 (z _)) (z _)
 #align category_theory.equiv_relation CategoryTheory.equiv_relation
 
-/-- In a connected category, any two objects are related by `zigzag`. -/
+/-- In a connected category, any two objects are related by `Zigzag`. -/
 theorem isConnected_zigzag [IsConnected J] (j₁ j₂ : J) : Zigzag j₁ j₂ :=
   equiv_relation _ zigzag_equivalence
     (@fun _ _ f => Relation.ReflTransGen.single (Or.inl (Nonempty.intro f))) _ _
 #align category_theory.is_connected_zigzag CategoryTheory.isConnected_zigzag
 
-/-- If any two objects in a nonempty category are related by `zigzag`, the category is connected.
+/-- If any two objects in a nonempty category are related by `Zigzag`, the category is connected.
 -/
 theorem zigzag_isConnected [Nonempty J] (h : ∀ j₁ j₂ : J, Zigzag j₁ j₂) : IsConnected J := by
   apply IsConnected.of_induct
@@ -348,13 +348,13 @@ theorem isConnected_of_zigzag [Nonempty J] (h : ∀ j₁ j₂ : J, ∃ l,
 #align category_theory.is_connected_of_zigzag CategoryTheory.isConnected_of_zigzag
 
 /-- If `Discrete α` is connected, then `α` is (type-)equivalent to `PUnit`. -/
-def discreteIsConnectedEquivPunit {α : Type u₁} [IsConnected (Discrete α)] : α ≃ PUnit :=
+def discreteIsConnectedEquivPUnit {α : Type u₁} [IsConnected (Discrete α)] : α ≃ PUnit :=
   Discrete.equivOfEquivalence.{u₁, u₁}
     { functor := Functor.star (Discrete α)
       inverse := Discrete.functor fun _ => Classical.arbitrary _
       unitIso := isoConstant _ (Classical.arbitrary _)
-      counitIso := Functor.pUnitExt _ _ }
-#align category_theory.discrete_is_connected_equiv_punit CategoryTheory.discreteIsConnectedEquivPunit
+      counitIso := Functor.punitExt _ _ }
+#align category_theory.discrete_is_connected_equiv_punit CategoryTheory.discreteIsConnectedEquivPUnit
 
 variable {C : Type u₂} [Category.{u₁} C]
 

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -72,8 +72,8 @@ def coneOfPreserves [PreservesLimit (F ⋙ snd L R) R] (c₁ : Cone (F ⋙ fst L
           w := ((isLimitOfPreserves R t₂).fac (limitAuxiliaryCone F c₁) j).symm }
       naturality := fun j₁ j₂ t => by
         ext
-        . simp [← c₁.w t]
-        . simp [← c₂.w t] }
+        · simp [← c₁.w t]
+        · simp [← c₂.w t] }
 #align category_theory.comma.cone_of_preserves CategoryTheory.Comma.coneOfPreserves
 
 /-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a
@@ -92,8 +92,8 @@ def coneOfPreservesIsLimit [PreservesLimit (F ⋙ snd L R) R] {c₁ : Cone (F 
           exact (s.π.app j).w }
   uniq s m w := by
     apply CommaMorphism.ext
-    . exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])
-    . exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])
+    · exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])
+    · exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])
 #align category_theory.comma.cone_of_preserves_is_limit CategoryTheory.Comma.coneOfPreservesIsLimit
 
 /-- (Implementation). An auxiliary cocone which is useful in order to construct colimits
@@ -123,8 +123,8 @@ def coconeOfPreserves [PreservesColimit (F ⋙ fst L R) L] {c₁ : Cocone (F ⋙
           w := (isColimitOfPreserves L t₁).fac (colimitAuxiliaryCocone _ c₂) j }
       naturality := fun j₁ j₂ t => by
         ext
-        . simp [← c₁.w t]
-        . simp [← c₂.w t] }
+        · simp [← c₁.w t]
+        · simp [← c₂.w t] }
 #align category_theory.comma.cocone_of_preserves CategoryTheory.Comma.coconeOfPreserves
 
 /-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is
@@ -143,8 +143,8 @@ def coconeOfPreservesIsColimit [PreservesColimit (F ⋙ fst L R) L] {c₁ : Coco
           exact (s.ι.app j).w }
   uniq s m w := by
     apply CommaMorphism.ext
-    . exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])
-    . exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])
+    · exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])
+    · exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])
 #align category_theory.comma.cocone_of_preserves_is_colimit CategoryTheory.Comma.coconeOfPreservesIsColimit
 
 instance hasLimit (F : J ⥤ Comma L R) [HasLimit (F ⋙ fst L R)] [HasLimit (F ⋙ snd L R)]
@@ -231,8 +231,8 @@ noncomputable instance createsLimit [i : PreservesLimit (F ⋙ proj X G) G] :
     CreatesLimit F (proj X G) :=
   letI : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) G := i
   createsLimitOfReflectsIso fun _ t =>
-    { liftedCone := Comma.coneOfPreserves F pUnitCone t
-      makesLimit := Comma.coneOfPreservesIsLimit _ pUnitConeIsLimit _
+    { liftedCone := Comma.coneOfPreserves F punitCone t
+      makesLimit := Comma.coneOfPreservesIsLimit _ punitConeIsLimit _
       validLift := Cones.ext (Iso.refl _) fun _ => (id_comp _).symm }
 #align category_theory.structured_arrow.creates_limit CategoryTheory.StructuredArrow.createsLimit
 
@@ -278,8 +278,8 @@ noncomputable instance createsColimit [i : PreservesColimit (F ⋙ proj G X) G]
     CreatesColimit F (proj G X) :=
   letI : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) G := i
   createsColimitOfReflectsIso fun _ t =>
-    { liftedCocone := Comma.coconeOfPreserves F t pUnitCocone
-      makesColimit := Comma.coconeOfPreservesIsColimit _ _ pUnitCoconeIsColimit
+    { liftedCocone := Comma.coconeOfPreserves F t punitCocone
+      makesColimit := Comma.coconeOfPreservesIsColimit _ _ punitCoconeIsColimit
       validLift := Cocones.ext (Iso.refl _) fun _ => comp_id _ }
 #align category_theory.costructured_arrow.creates_colimit CategoryTheory.CostructuredArrow.createsColimit
 

Mathlib/CategoryTheory/Limits/Unit.lean

@@ -28,32 +28,32 @@ namespace CategoryTheory.Limits
 
 variable {J : Type v} [Category.{v'} J] {F : J ⥤ Discrete PUnit}
 
-/-- A trivial cone for a functor into `PUnit`. `pUnitConeIsLimit` shows it is a limit. -/
-def pUnitCone : Cone F :=
-  ⟨⟨⟨⟩⟩, (Functor.pUnitExt _ _).hom⟩
-#align category_theory.limits.punit_cone CategoryTheory.Limits.pUnitCone
+/-- A trivial cone for a functor into `PUnit`. `punitConeIsLimit` shows it is a limit. -/
+def punitCone : Cone F :=
+  ⟨⟨⟨⟩⟩, (Functor.punitExt _ _).hom⟩
+#align category_theory.limits.punit_cone CategoryTheory.Limits.punitCone
 
-/-- A trivial cocone for a functor into `PUnit`. `pUnitCoconeIsLimit` shows it is a colimit. -/
-def pUnitCocone : Cocone F :=
-  ⟨⟨⟨⟩⟩, (Functor.pUnitExt _ _).hom⟩
-#align category_theory.limits.punit_cocone CategoryTheory.Limits.pUnitCocone
+/-- A trivial cocone for a functor into `PUnit`. `punitCoconeIsLimit` shows it is a colimit. -/
+def punitCocone : Cocone F :=
+  ⟨⟨⟨⟩⟩, (Functor.punitExt _ _).hom⟩
+#align category_theory.limits.punit_cocone CategoryTheory.Limits.punitCocone
 
 /-- Any cone over a functor into `PUnit` is a limit cone.
 -/
-def pUnitConeIsLimit {c : Cone F} : IsLimit c where
+def punitConeIsLimit {c : Cone F} : IsLimit c where
   lift := fun s => eqToHom (by simp)
-#align category_theory.limits.punit_cone_is_limit CategoryTheory.Limits.pUnitConeIsLimit
+#align category_theory.limits.punit_cone_is_limit CategoryTheory.Limits.punitConeIsLimit
 
 /-- Any cocone over a functor into `PUnit` is a colimit cocone.
 -/
-def pUnitCoconeIsColimit {c : Cocone F} : IsColimit c where
+def punitCoconeIsColimit {c : Cocone F} : IsColimit c where
   desc := fun s => eqToHom (by simp)
-#align category_theory.limits.punit_cocone_is_colimit CategoryTheory.Limits.pUnitCoconeIsColimit
+#align category_theory.limits.punit_cocone_is_colimit CategoryTheory.Limits.punitCoconeIsColimit
 
 instance : HasLimitsOfSize.{v', v} (Discrete PUnit) :=
-  ⟨fun _ _ => ⟨fun _ => ⟨pUnitCone, pUnitConeIsLimit⟩⟩⟩
+  ⟨fun _ _ => ⟨fun _ => ⟨punitCone, punitConeIsLimit⟩⟩⟩
 
 instance : HasColimitsOfSize.{v', v} (Discrete PUnit) :=
-  ⟨fun _ _ => ⟨fun _ => ⟨pUnitCocone, pUnitCoconeIsColimit⟩⟩⟩
+  ⟨fun _ _ => ⟨fun _ => ⟨punitCocone, punitCoconeIsColimit⟩⟩⟩
 
 end CategoryTheory.Limits

Mathlib/CategoryTheory/PUnit.lean

@@ -40,17 +40,17 @@ variable {C}
 
 /-- Any two functors to `Discrete PUnit` are isomorphic. -/
 @[simps!]
-def pUnitExt (F G : C ⥤ Discrete PUnit) : F ≅ G :=
+def punitExt (F G : C ⥤ Discrete PUnit) : F ≅ G :=
   NatIso.ofComponents fun X => eqToIso (by simp only [eq_iff_true_of_subsingleton])
-#align category_theory.functor.punit_ext CategoryTheory.Functor.pUnitExt
+#align category_theory.functor.punit_ext CategoryTheory.Functor.punitExt
 -- Porting note: simp does indeed fire for these despite the linter warning
-attribute [nolint simpNF] pUnitExt_hom_app_down_down pUnitExt_inv_app_down_down
+attribute [nolint simpNF] punitExt_hom_app_down_down punitExt_inv_app_down_down
 
 /-- Any two functors to `Discrete PUnit` are *equal*.
-You probably want to use `pUnitExt` instead of this. -/
-theorem pUnit_ext' (F G : C ⥤ Discrete PUnit) : F = G :=
+You probably want to use `punitExt` instead of this. -/
+theorem punit_ext' (F G : C ⥤ Discrete PUnit) : F = G :=
   Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]
-#align category_theory.functor.punit_ext' CategoryTheory.Functor.pUnit_ext'
+#align category_theory.functor.punit_ext' CategoryTheory.Functor.punit_ext'
 
 /-- The functor from `Discrete PUnit` sending everything to the given object. -/
 abbrev fromPUnit (X : C) : Discrete PUnit.{v + 1} ⥤ C :=
@@ -73,7 +73,7 @@ end Functor
 /-- A category being equivalent to `PUnit` is equivalent to it having a unique morphism between
   any two objects. (In fact, such a category is also a groupoid;
   see `CategoryTheory.Groupoid.ofHomUnique`) -/
-theorem equiv_pUnit_iff_unique :
+theorem equiv_punit_iff_unique :
     Nonempty (C ≌ Discrete PUnit) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y) := by
   constructor
   · rintro ⟨h⟩
@@ -98,11 +98,11 @@ theorem equiv_pUnit_iff_unique :
     refine'
       Nonempty.intro
         (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
-          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.pUnitExt))
+          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))
     exact
       NatIso.ofComponents fun _ =>
         { hom := default
           inv := default }
-#align category_theory.equiv_punit_iff_unique CategoryTheory.equiv_pUnit_iff_unique
+#align category_theory.equiv_punit_iff_unique CategoryTheory.equiv_punit_iff_unique
 
 end CategoryTheory

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -98,7 +98,7 @@ theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z := by
 #align is_alg_closed.exists_eq_mul_self IsAlgClosed.exists_eq_mul_self
 
 theorem roots_eq_zero_iff [IsAlgClosed k] {p : k[X]} :
-  p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) := by
+    p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) := by
   refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
   cases' le_or_lt (degree p) 0 with hd hd
   · exact eq_C_of_degree_le_zero hd
@@ -159,10 +159,10 @@ theorem algebraMap_surjective_of_isIntegral {k K : Type _} [Field k] [Ring K] [I
   exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
 #align is_alg_closed.algebra_map_surjective_of_is_integral IsAlgClosed.algebraMap_surjective_of_isIntegral
 
-theorem algebra_map_surjective_of_is_integral' {k K : Type _} [Field k] [CommRing K] [IsDomain K]
+theorem algebraMap_surjective_of_isIntegral' {k K : Type _} [Field k] [CommRing K] [IsDomain K]
     [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) : Function.Surjective f :=
   @algebraMap_surjective_of_isIntegral k K _ _ _ _ f.toAlgebra hf
-#align is_alg_closed.algebra_map_surjective_of_is_integral' IsAlgClosed.algebra_map_surjective_of_is_integral'
+#align is_alg_closed.algebra_map_surjective_of_is_integral' IsAlgClosed.algebraMap_surjective_of_isIntegral'
 
 theorem algebraMap_surjective_of_isAlgebraic {k K : Type _} [Field k] [Ring K] [IsDomain K]
     [IsAlgClosed k] [Algebra k K] (hf : Algebra.IsAlgebraic k K) :