chore: tidy various files (#5458)

Archive/Examples/PropEncodable.lean

@@ -14,8 +14,8 @@ import Mathlib.Data.Fin.VecNotation
 /-!
 # W types
 
-The file `data/W.lean` shows that if `α` is an an encodable fintype and for every `a : α`,
-`β a` is encodable, then `W β` is encodable.
+The file `Mathlib/Data/W/Basic.lean` shows that if `α` is an an encodable fintype and for every
+`a : α`, `β a` is encodable, then `W β` is encodable.
 
 As an example of how this can be used, we show that the type of propositional formulas with
 variables labeled from an encodable type is encodable.
@@ -42,7 +42,7 @@ inductive PropForm (α : Type _)
 
 /-!
 The next three functions make it easier to construct functions from a small
-`fin`.
+`Fin`.
 -/
 
 -- porting note: using `![_, _]` notation instead

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -18,10 +18,10 @@ Forgetful functors from algebraic categories usually don't preserve colimits. Ho
 to preserve _filtered_ colimits.
 
 In this file, we start with a ring `R`, a small filtered category `J` and a functor
-`F : J ⥤ Module R`. We show that the colimit of `F ⋙ forget₂ (Module R) AddCommGroup`
-(in `AddCommGroup`) carries the structure of an `R`-module, thereby showing that the forgetful
-functor `forget₂ (Module R) AddCommGroup` preserves filtered colimits. In particular, this implies
-that `forget (Module R)` preserves filtered colimits.
+`F : J ⥤ ModuleCat R`. We show that the colimit of `F ⋙ forget₂ (ModuleCat R) AddCommGroupCat`
+(in `AddCommGroupCat`) carries the structure of an `R`-module, thereby showing that the forgetful
+functor `forget₂ (ModuleCat R) AddCommGroupCat` preserves filtered colimits. In particular, this
+implies that `forget (ModuleCat R)` preserves filtered colimits.
 
 -/
 
@@ -46,7 +46,7 @@ variable {R : Type u} [Ring R] {J : Type v} [SmallCategory J] [IsFiltered J]
 
 variable (F : J ⥤ ModuleCatMax.{v, u, u} R)
 
-/-- The colimit of `F ⋙ forget₂ (Module R) AddCommGroup` in the category `AddCommGroup`.
+/-- The colimit of `F ⋙ forget₂ (ModuleCat R) AddCommGroupCat` in the category `AddCommGroupCat`.
 In the following, we will show that this has the structure of an `R`-module.
 -/
 abbrev M : AddCommGroupCat :=
@@ -68,28 +68,28 @@ set_option linter.uppercaseLean3 false in
 #align Module.filtered_colimits.M.mk_eq ModuleCat.FilteredColimits.M.mk_eq
 
 /-- The "unlifted" version of scalar multiplication in the colimit. -/
-def colimitSmulAux (r : R) (x : Σ j, F.obj j) : M F :=
+def colimitSMulAux (r : R) (x : Σ j, F.obj j) : M F :=
   M.mk F ⟨x.1, r • x.2⟩
 set_option linter.uppercaseLean3 false in
-#align Module.filtered_colimits.colimit_smul_aux ModuleCat.FilteredColimits.colimitSmulAux
+#align Module.filtered_colimits.colimit_smul_aux ModuleCat.FilteredColimits.colimitSMulAux
 
-theorem colimitSmulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
+theorem colimitSMulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
     (h : Types.FilteredColimit.Rel.{v, u} (F ⋙ forget (ModuleCat R)) x y) :
-    colimitSmulAux F r x = colimitSmulAux F r y := by
+    colimitSMulAux F r x = colimitSMulAux F r y := by
   apply M.mk_eq
   obtain ⟨k, f, g, hfg⟩ := h
   use k, f, g
   simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
   simp [hfg]
 set_option linter.uppercaseLean3 false in
-#align Module.filtered_colimits.colimit_smul_aux_eq_of_rel ModuleCat.FilteredColimits.colimitSmulAux_eq_of_rel
+#align Module.filtered_colimits.colimit_smul_aux_eq_of_rel ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel
 
-/-- Scalar multiplication in the colimit. See also `colimitSmulAux`. -/
+/-- Scalar multiplication in the colimit. See also `colimitSMulAux`. -/
 instance colimitHasSmul : SMul R (M F) where
   smul r x := by
-    refine' Quot.lift (colimitSmulAux F r) _ x
+    refine' Quot.lift (colimitSMulAux F r) _ x
     intro x y h
-    apply colimitSmulAux_eq_of_rel
+    apply colimitSMulAux_eq_of_rel
     apply Types.FilteredColimit.rel_of_quot_rel
     exact h
 set_option linter.uppercaseLean3 false in
@@ -189,7 +189,7 @@ def colimitDesc (t : Cocone F) : colimit F ⟶ t.pt :=
 set_option linter.uppercaseLean3 false in
 #align Module.filtered_colimits.colimit_desc ModuleCat.FilteredColimits.colimitDesc
 
-/-- The proposed colimit cocone is a colimit in `Module R`. -/
+/-- The proposed colimit cocone is a colimit in `ModuleCat R`. -/
 def colimitCoconeIsColimit : IsColimit (colimitCocone F) where
   desc := colimitDesc F
   fac t j :=

Mathlib/AlgebraicGeometry/OpenImmersion/Basic.lean

@@ -24,7 +24,7 @@ Abbreviations are also provided for `SheafedSpace`, `LocallyRingedSpace` and `Sc
 
 * `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion`: the `Prop`-valued typeclass asserting
   that a PresheafedSpace hom `f` is an open_immersion.
-* `algebraic_geometry.is_open_immersion`: the `Prop`-valued typeclass asserting
+* `AlgebraicGeometry.IsOpenImmersion`: the `Prop`-valued typeclass asserting
   that a Scheme morphism `f` is an open_immersion.
 * `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict`: The source of an
   open immersion is isomorphic to the restriction of the target onto the image.
@@ -98,13 +98,13 @@ namespace PresheafedSpace.IsOpenImmersion
 
 open PresheafedSpace
 
-local notation "is_open_immersion" => PresheafedSpace.IsOpenImmersion
+local notation "IsOpenImmersion" => PresheafedSpace.IsOpenImmersion
 
 attribute [instance] IsOpenImmersion.c_iso
 
 section
 
-variable {X Y : PresheafedSpace C} {f : X ⟶ Y} (H : is_open_immersion f)
+variable {X Y : PresheafedSpace C} {f : X ⟶ Y} (H : IsOpenImmersion f)
 
 /-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
 abbrev openFunctor :=
@@ -149,13 +149,13 @@ theorem isoRestrict_inv_ofRestrict : H.isoRestrict.inv ≫ f = Y.ofRestrict _ :=
   rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_inv_of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict
 
-instance mono [H : is_open_immersion f] : Mono f := by
+instance mono [H : IsOpenImmersion f] : Mono f := by
   rw [← H.isoRestrict_hom_ofRestrict]; apply mono_comp
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.mono AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono
 
 /-- The composition of two open immersions is an open immersion. -/
-instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : is_open_immersion f] (g : Y ⟶ Z)
-    [hg : is_open_immersion g] : is_open_immersion (f ≫ g) where
+instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : IsOpenImmersion f] (g : Y ⟶ Z)
+    [hg : IsOpenImmersion g] : IsOpenImmersion (f ≫ g) where
   base_open := hg.base_open.comp hf.base_open
   c_iso U := by
     generalize_proofs h
@@ -270,19 +270,19 @@ theorem app_inv_app' (U : Opens Y) (hU : (U : Set Y) ⊆ Set.range f.base) :
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app' AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'
 
 /-- An isomorphism is an open immersion. -/
-instance ofIso {X Y : PresheafedSpace C} (H : X ≅ Y) : is_open_immersion H.hom where
+instance ofIso {X Y : PresheafedSpace C} (H : X ≅ Y) : IsOpenImmersion H.hom where
   base_open := (TopCat.homeoOfIso ((forget C).mapIso H)).openEmbedding
   -- Porting note : `inferInstance` will fail if Lean is not told that `H.hom.c` is iso
   c_iso _ := letI : IsIso H.hom.c := c_isIso_of_iso H.hom; inferInstance
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.of_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso
 
 instance (priority := 100) ofIsIso {X Y : PresheafedSpace C} (f : X ⟶ Y) [IsIso f] :
-    is_open_immersion f :=
+    IsOpenImmersion f :=
   AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso (asIso f)
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.of_is_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso
 
 instance ofRestrict {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier}
-    (hf : OpenEmbedding f) : is_open_immersion (Y.ofRestrict hf) where
+    (hf : OpenEmbedding f) : IsOpenImmersion (Y.ofRestrict hf) where
   base_open := hf
   c_iso U := by
     dsimp
@@ -313,7 +313,7 @@ theorem ofRestrict_invApp {C : Type _} [Category C] (X : PresheafedSpace C) {Y :
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict_inv_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp
 
 /-- An open immersion is an iso if the underlying continuous map is epi. -/
-theorem to_iso (f : X ⟶ Y) [h : is_open_immersion f] [h' : Epi f.base] : IsIso f := by
+theorem to_iso (f : X ⟶ Y) [h : IsOpenImmersion f] [h' : Epi f.base] : IsIso f := by
   -- Porting Note : was `apply (config := { instances := False }) ...`
   -- See https://github.com/leanprover/lean4/issues/2273
   have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U)
@@ -338,7 +338,7 @@ theorem to_iso (f : X ⟶ Y) [h : is_open_immersion f] [h' : Epi f.base] : IsIso
   apply isIso_of_components
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.to_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
 
-instance stalk_iso [HasColimits C] [H : is_open_immersion f] (x : X) : IsIso (stalkMap f x) := by
+instance stalk_iso [HasColimits C] [H : IsOpenImmersion f] (x : X) : IsIso (stalkMap f x) := by
   rw [← H.isoRestrict_hom_ofRestrict]
   rw [PresheafedSpace.stalkMap.comp]
   infer_instance
@@ -348,7 +348,7 @@ end
 
 noncomputable section Pullback
 
-variable {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : is_open_immersion f] (g : Y ⟶ Z)
+variable {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z)
 
 /-- (Implementation.) The projection map when constructing the pullback along an open immersion.
 -/
@@ -481,7 +481,7 @@ theorem pullbackConeOfLeftLift_snd :
     · rw [s.pt.presheaf.map_id]; erw [Category.comp_id]
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift_snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd
 
-instance pullbackConeSndIsOpenImmersion : is_open_immersion (pullbackConeOfLeft f g).snd := by
+instance pullbackConeSndIsOpenImmersion : IsOpenImmersion (pullbackConeOfLeft f g).snd := by
   erw [CategoryTheory.Limits.PullbackCone.mk_snd]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_snd_is_open_immersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion
@@ -507,20 +507,20 @@ instance hasPullback_of_right : HasPullback g f :=
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.has_pullback_of_right AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right
 
 /-- Open immersions are stable under base-change. -/
-instance pullbackSndOfLeft : is_open_immersion (pullback.snd : pullback f g ⟶ _) := by
+instance pullbackSndOfLeft : IsOpenImmersion (pullback.snd : pullback f g ⟶ _) := by
   delta pullback.snd
   rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft
 
 /-- Open immersions are stable under base-change. -/
-instance pullbackFstOfRight : is_open_immersion (pullback.fst : pullback g f ⟶ _) := by
+instance pullbackFstOfRight : IsOpenImmersion (pullback.fst : pullback g f ⟶ _) := by
   rw [← pullbackSymmetry_hom_comp_snd]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_fst_of_right AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight
 
-instance pullbackToBaseIsOpenImmersion [is_open_immersion g] :
-    is_open_immersion (limit.π (cospan f g) WalkingCospan.one) := by
+instance pullbackToBaseIsOpenImmersion [IsOpenImmersion g] :
+    IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one) := by
   rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_to_base_is_open_immersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion
@@ -579,7 +579,7 @@ theorem lift_uniq (H : Set.range g.base ⊆ Set.range f.base) (l : Y ⟶ X) (hl
 
 /-- Two open immersions with equal range is isomorphic. -/
 @[simps]
-def isoOfRangeEq [is_open_immersion g] (e : Set.range f.base = Set.range g.base) : X ≅ Y where
+def isoOfRangeEq [IsOpenImmersion g] (e : Set.range f.base = Set.range g.base) : X ≅ Y where
   hom := lift g f (le_of_eq e)
   inv := lift f g (le_of_eq e.symm)
   hom_inv_id := by rw [← cancel_mono f]; simp
@@ -594,7 +594,7 @@ section ToSheafedSpace
 
 variable {X : PresheafedSpace C} (Y : SheafedSpace C)
 
-variable (f : X ⟶ Y.toPresheafedSpace) [H : is_open_immersion f]
+variable (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f]
 
 /-- If `X ⟶ Y` is an open immersion, and `Y` is a SheafedSpace, then so is `X`. -/
 def toSheafedSpace : SheafedSpace C where
@@ -632,7 +632,7 @@ instance toSheafedSpace_isOpenImmersion : SheafedSpace.IsOpenImmersion (toSheafe
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_is_open_immersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_isOpenImmersion
 
 @[simp]
-theorem sheafedSpace_toSheafedSpace {X Y : SheafedSpace C} (f : X ⟶ Y) [is_open_immersion f] :
+theorem sheafedSpace_toSheafedSpace {X Y : SheafedSpace C} (f : X ⟶ Y) [IsOpenImmersion f] :
     toSheafedSpace Y f = X := by cases X; rfl
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.SheafedSpace_to_SheafedSpace AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace
 
@@ -642,7 +642,7 @@ section ToLocallyRingedSpace
 
 variable {X : PresheafedSpace CommRingCat} (Y : LocallyRingedSpace)
 
-variable (f : X ⟶ Y.toPresheafedSpace) [H : is_open_immersion f]
+variable (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f]
 
 /-- If `X ⟶ Y` is an open immersion, and `Y` is a LocallyRingedSpace, then so is `X`. -/
 def toLocallyRingedSpace : LocallyRingedSpace where
@@ -775,7 +775,6 @@ instance sheafedSpaceForgetPreservesOfLeft : PreservesLimit (cospan f g) (Sheafe
       . dsimp
         infer_instance
       apply preservesLimitOfIsoDiagram _ (diagramIsoCospan _).symm
-
 #align algebraic_geometry.SheafedSpace.is_open_immersion.SheafedSpace_forget_preserves_of_left AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpaceForgetPreservesOfLeft
 
 instance sheafedSpaceForgetPreservesOfRight : PreservesLimit (cospan g f) (SheafedSpace.forget C) :=
@@ -995,7 +994,7 @@ def pullbackConeOfLeft : PullbackCone f g := by
 instance : LocallyRingedSpace.IsOpenImmersion (pullbackConeOfLeft f g).snd :=
   show PresheafedSpace.IsOpenImmersion (Y.toPresheafedSpace.ofRestrict _) by infer_instance
 
-/-- The constructed `pullback_cone_of_left` is indeed limiting. -/
+/-- The constructed `pullbackConeOfLeft` is indeed limiting. -/
 def pullbackConeOfLeftIsLimit : IsLimit (pullbackConeOfLeft f g) :=
   PullbackCone.isLimitAux' _ fun s => by
     refine' ⟨LocallyRingedSpace.Hom.mk (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift

Mathlib/Analysis/Complex/CauchyIntegral.lean

@@ -29,7 +29,7 @@ Banach space with second countable topology.
 In the following theorems, if the name ends with `off_countable`, then the actual theorem assumes
 differentiability at all but countably many points of the set mentioned below.
 
-* `complex.integral_boundary_rect_of_has_fderiv_within_at_real_off_countable`: If a function
+* `Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable`: If a function
   `f : ℂ → E` is continuous on a closed rectangle and *real* differentiable on its interior, then
   its integral over the boundary of this rectangle is equal to the integral of
   `I • f' (x + y * I) 1 - f' (x + y * I) I` over the rectangle, where `f' z w : E` is the derivative
@@ -72,7 +72,7 @@ differentiability at all but countably many points of the set mentioned below.
   on a neighborhood of a point, then it is analytic at this point. In particular, if `f : ℂ → E`
   is differentiable on the whole `ℂ`, then it is analytic at every point `z : ℂ`.
 
-* `differentiable.has_power_series_on_ball`: If `f : ℂ → E` is differentiable everywhere then the
+* `Differentiable.hasFPowerSeriesOnBall`: If `f : ℂ → E` is differentiable everywhere then the
   `cauchyPowerSeries f z R` is a formal power series representing `f` at `z` with infinite
   radius of convergence (this holds for any choice of `0 < R`).
 

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -22,17 +22,17 @@ Fourier transform of `f`, under the following hypotheses:
 * `f` is a continuous function `ℝ → ℂ`.
 * The sum `∑ (n : ℤ), 𝓕 f n` is convergent.
 * For all compacts `K ⊂ ℝ`, the sum `∑ (n : ℤ), sup { ‖f(x + n)‖ | x ∈ K }` is convergent.
-See `real.tsum_eq_tsum_fourier_integral` for this formulation.
+See `Real.tsum_eq_tsum_fourierIntegral` for this formulation.
 
 These hypotheses are potentially a little awkward to apply, so we also provide the less general but
-easier-to-use result `real.tsum_eq_tsum_fourier_integral_of_rpow_decay`, in which we assume `f` and
+easier-to-use result `Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay`, in which we assume `f` and
 `𝓕 f` both decay as `|x| ^ (-b)` for some `b > 1`, and the even more specific result
-`schwartz_map.tsum_eq_tsum_fourier_integral`, where we assume that both `f` and `𝓕 f` are Schwartz
+`SchwartzMap.tsum_eq_tsum_fourierIntegral`, where we assume that both `f` and `𝓕 f` are Schwartz
 functions.
 
 ## TODO
 
-At the moment `schwartz_map.tsum_eq_tsum_fourier_integral` requires separate proofs that both `f`
+At the moment `SchwartzMap.tsum_eq_tsum_fourierIntegral` requires separate proofs that both `f`
 and `𝓕 f` are Schwartz functions. In fact, `𝓕 f` is automatically Schwartz if `f` is; and once
 we have this lemma in the library, we should adjust the hypotheses here accordingly.
 -/
@@ -179,7 +179,6 @@ theorem isBigO_norm_Icc_restrict_atTop {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
 set_option linter.uppercaseLean3 false in
 #align is_O_norm_Icc_restrict_at_top isBigO_norm_Icc_restrict_atTop
 
-set_option autoImplicit false in
 theorem isBigO_norm_Icc_restrict_atBot {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
     (hf : IsBigO atBot f fun x : ℝ => |x| ^ (-b)) (R S : ℝ) :
     IsBigO atBot (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) fun x : ℝ => |x| ^ (-b) := by

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -33,7 +33,7 @@ Letting `T` be a self-adjoint operator on a finite-dimensional inner product spa
 * The definition `LinearMap.IsSymmetric.eigenvectorBasis` provides an orthonormal basis for `E`
   consisting of eigenvectors of `T`, with `LinearMap.IsSymmetric.eigenvalues` giving the
   corresponding list of eigenvalues, as real numbers.  The definition
-  `linear_map.is_symmetric.eigenvector_basis` gives the associated linear isometry equivalence
+  `LinearMap.IsSymmetric.eigenvectorBasis` gives the associated linear isometry equivalence
   from `E` to Euclidean space, and the theorem
   `LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply` states that, when `T` is
   transferred via this equivalence to an operator on Euclidean space, it acts diagonally.