chore: tidy various files (#5628)

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -124,12 +124,12 @@ instance : Full (forget₂ (FGModuleCat R) (ModuleCat.{u} R)) where
 variable {R}
 
 /-- Converts and isomorphism in the category `FGModuleCat R` to
-a `linear_equiv` between the underlying modules. -/
+a `LinearEquiv` between the underlying modules. -/
 def isoToLinearEquiv {V W : FGModuleCat R} (i : V ≅ W) : V ≃ₗ[R] W :=
   ((forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).mapIso i).toLinearEquiv
 #align fgModule.iso_to_linear_equiv FGModuleCat.isoToLinearEquiv
 
-/-- Converts a `linear_equiv` to an isomorphism in the category `FGModuleCat R`. -/
+/-- Converts a `LinearEquiv` to an isomorphism in the category `FGModuleCat R`. -/
 @[simps]
 def _root_.LinearEquiv.toFGModuleCatIso
     {V W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V]

Mathlib/Algebra/CharP/Basic.lean

@@ -664,14 +664,13 @@ theorem charP_of_ne_zero (hn : Fintype.card R = n) (hR : ∀ i < n, (i : R) = 0
 #align char_p_of_ne_zero charP_of_ne_zero
 
 theorem charP_of_prime_pow_injective (R) [Ring R] [Fintype R] (p : ℕ) [hp : Fact p.Prime] (n : ℕ)
-    (hn : Fintype.card R = p ^ n) (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) : CharP R (p ^ n) := by
+    (hn : Fintype.card R = p ^ n) (hR : ∀ i ≤ n, (p : R) ^ i = 0 → i = n) : CharP R (p ^ n) := by
   obtain ⟨c, hc⟩ := CharP.exists R
-  skip
   have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
   obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
   obtain rfl : i = n := by
     apply hR i hi
-    rw [← hc, CharP.cast_eq_zero]
+    rw [← Nat.cast_pow, ← hc, CharP.cast_eq_zero]
   rwa [← hc]
 #align char_p_of_prime_pow_injective charP_of_prime_pow_injective
 
@@ -695,12 +694,12 @@ instance Prod.charP [CharP S p] : CharP (R × S) p := by
 
 end Prod
 
-instance ULift.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift.{v} R) p
-    where cast_eq_zero_iff' n := Iff.trans (ULift.ext_iff _ _) <| CharP.cast_eq_zero_iff R p n
+instance ULift.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift.{v} R) p where
+  cast_eq_zero_iff' n := Iff.trans (ULift.ext_iff _ _) <| CharP.cast_eq_zero_iff R p n
 #align ulift.char_p ULift.charP
 
-instance MulOpposite.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p
-    where cast_eq_zero_iff' n := MulOpposite.unop_inj.symm.trans <| CharP.cast_eq_zero_iff R p n
+instance MulOpposite.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p where
+  cast_eq_zero_iff' n := MulOpposite.unop_inj.symm.trans <| CharP.cast_eq_zero_iff R p n
 #align mul_opposite.char_p MulOpposite.charP
 
 section

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -261,7 +261,6 @@ theorem IsAffineOpen.imageIsOpenImmersion {X Y : Scheme} {U : Opens X} (hU : IsA
   exact Set.image_eq_range _ _
 #align algebraic_geometry.is_affine_open.image_is_open_immersion AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion
 
-set_option maxHeartbeats 0 in
 theorem isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f]
     (U : Opens X) : IsAffineOpen (H.openFunctor.obj U) ↔ IsAffineOpen U := by
   -- Porting note : add this instance explicitly
@@ -364,7 +363,7 @@ theorem IsAffineOpen.basicOpenIsAffine {X : Scheme} {U : Opens X} (hU : IsAffine
     exact Scheme.basicOpen_le _ _
   rw [Scheme.Hom.opensRange_coe, Scheme.comp_val_base, ← this, coe_comp, Set.range_comp]
   -- Porting note : `congr 1` did not work
-  apply congr_arg (_ '' .)
+  apply congr_arg (_ '' ·)
   refine' (Opens.coe_inj.mpr <| Scheme.preimage_basicOpen hU.fromSpec f).trans _
   refine' Eq.trans _ (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm
   congr 1
@@ -474,7 +473,7 @@ theorem IsAffineOpen.opens_map_fromSpec_basicOpen {X : Scheme} {U : Opens X}
       (Scheme.Spec.obj <| op <| X.presheaf.obj (op U)).toLocallyRingedSpace.toRingedSpace
       (eqToHom hU.fromSpec_base_preimage).op _)
   -- Porting note : `congr` does not work
-  refine congr_arg (RingedSpace.basicOpen _ .) ?_
+  refine congr_arg (RingedSpace.basicOpen _ ·) ?_
   -- Porting note : change `rw` to `erw`
   erw [← comp_apply]
   congr
@@ -699,7 +698,7 @@ theorem IsAffineOpen.isLocalization_stalk {X : Scheme} {U : Opens X} (hU : IsAff
   convert hU.isLocalization_stalk' y hx
 #align algebraic_geometry.is_affine_open.is_localization_stalk AlgebraicGeometry.IsAffineOpen.isLocalization_stalk
 
-/-- The basic open set of a section `f` on an an affine open as an `X.affine_opens`. -/
+/-- The basic open set of a section `f` on an an affine open as an `X.affineOpens`. -/
 @[simps]
 def Scheme.affineBasicOpen (X : Scheme) {U : X.affineOpens} (f : X.presheaf.obj <| op U) :
     X.affineOpens :=
@@ -758,7 +757,7 @@ theorem IsAffineOpen.basicOpen_union_eq_self_iff {X : Scheme} {U : Opens X}
     -- Porting note : need an extra rewrite here, after simp, it is in `↔` form
     rw [iff_iff_eq]
     congr 3
-    · refine congr_arg (Set.iUnion .) ?_
+    · refine congr_arg (Set.iUnion ·) ?_
       ext1 x
       exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
     · exact congr_arg Opens.carrier hU.fromSpec_base_preimage

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -25,8 +25,8 @@ Given a family of gluing data of schemes, we may glue them together.
 * `AlgebraicGeometry.Scheme.GlueData.ι`: The immersion `ι i : U i ⟶ glued` for each `i : J`.
 * `AlgebraicGeometry.Scheme.GlueData.isoCarrier`: The isomorphism between the underlying space
   of the glued scheme and the gluing of the underlying topological spaces.
-* `algebraic_geometry.Scheme.OpenCover.gluedCover`: The glue data associated with an open cover.
-* `algebraic_geometry.Scheme.OpenCover.fromGlued`: The canonical morphism
+* `AlgebraicGeometry.Scheme.OpenCover.gluedCover`: The glue data associated with an open cover.
+* `AlgebraicGeometry.Scheme.OpenCover.fromGlued`: The canonical morphism
   `𝒰.gluedCover.glued ⟶ X`. This has an `is_iso` instance.
 * `AlgebraicGeometry.Scheme.OpenCover.glueMorphisms`: We may glue a family of compatible
   morphisms defined on an open cover of a scheme.
@@ -39,7 +39,7 @@ Given a family of gluing data of schemes, we may glue them together.
   `ι i : U i ⟶ glued` are jointly surjective.
 * `AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimit` : `V i j` is the pullback
   (intersection) of `U i` and `U j` over the glued space.
-* `algebraic_geometry.Scheme.glue_data.ι_eq_iff_rel` : `ι i x = ι j y` if and only if they coincide
+* `AlgebraicGeometry.Scheme.GlueData.ι_eq_iff` : `ι i x = ι j y` if and only if they coincide
   when restricted to `V i i`.
 * `AlgebraicGeometry.Scheme.GlueData.isOpen_iff` : An subset of the glued scheme is open iff
   all its preimages in `U i` are open.
@@ -125,7 +125,7 @@ instance (i : 𝖣.J) :
   apply LocallyRingedSpace.GlueData.ι_isOpenImmersion
 
 /-- (Implementation). The glued scheme of a glue data.
-This should not be used outside this file. Use `Scheme.glue_data.glued` instead. -/
+This should not be used outside this file. Use `AlgebraicGeometry.Scheme.GlueData.glued` instead. -/
 def gluedScheme : Scheme := by
   apply LocallyRingedSpace.IsOpenImmersion.scheme
     D.toLocallyRingedSpaceGlueData.toGlueData.glued
@@ -190,7 +190,7 @@ theorem glue_condition (i j : D.J) : D.t i j ≫ D.f j i ≫ D.ι j = D.f i j 
 #align algebraic_geometry.Scheme.glue_data.glue_condition AlgebraicGeometry.Scheme.GlueData.glue_condition
 
 /-- The pullback cone spanned by `V i j ⟶ U i` and `V i j ⟶ U j`.
-This is a pullback diagram (`V_pullback_cone_is_limit`). -/
+This is a pullback diagram (`vPullbackConeIsLimit`). -/
 def vPullbackCone (i j : D.J) : PullbackCone (D.ι i) (D.ι j) :=
   PullbackCone.mk (D.f i j) (D.t i j ≫ D.f j i) (by simp)
 #align algebraic_geometry.Scheme.glue_data.V_pullback_cone AlgebraicGeometry.Scheme.GlueData.vPullbackCone
@@ -238,7 +238,7 @@ theorem ι_isoCarrier_inv (i : D.J) :
 #align algebraic_geometry.Scheme.glue_data.ι_iso_carrier_inv AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv
 
 /-- An equivalence relation on `Σ i, D.U i` that holds iff `𝖣 .ι i x = 𝖣 .ι j y`.
-See `Scheme.gluing_data.ι_eq_iff`. -/
+See `AlgebraicGeometry.Scheme.GlueData.ι_eq_iff`. -/
 def Rel (a b : Σ i, ((D.U i).carrier : Type _)) : Prop :=
   a = b ∨
     ∃ x : (D.V (a.1, b.1)).carrier, (D.f _ _).1.base x = a.2 ∧ (D.t _ _ ≫ D.f _ _).1.base x = b.2
@@ -337,7 +337,7 @@ theorem glued_cover_cocycle (x y z : 𝒰.J) :
 #align algebraic_geometry.Scheme.open_cover.glued_cover_cocycle AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle
 
 /-- The glue data associated with an open cover.
-The canonical isomorphism `𝒰.glued_cover.glued ⟶ X` is provided by `𝒰.from_glued`. -/
+The canonical isomorphism `𝒰.gluedCover.glued ⟶ X` is provided by `𝒰.fromGlued`. -/
 @[simps]
 def gluedCover : Scheme.GlueData.{u} where
   J := 𝒰.J
@@ -355,7 +355,7 @@ def gluedCover : Scheme.GlueData.{u} where
 #align algebraic_geometry.Scheme.open_cover.glued_cover AlgebraicGeometry.Scheme.OpenCover.gluedCover
 
 /-- The canonical morphism from the gluing of an open cover of `X` into `X`.
-This is an isomorphism, as witnessed by an `is_iso` instance. -/
+This is an isomorphism, as witnessed by an `IsIso` instance. -/
 def fromGlued : 𝒰.gluedCover.glued ⟶ X := by
   fapply Multicoequalizer.desc
   exact fun x => 𝒰.map x

Mathlib/AlgebraicGeometry/Limits.lean

@@ -16,7 +16,7 @@ import Mathlib.AlgebraicGeometry.AffineScheme
 
 We construct various limits and colimits in the category of schemes.
 
-* The existence of fibred products was shown in `algebraic_geometry/pullbacks.lean`.
+* The existence of fibred products was shown in `Mathlib/AlgebraicGeometry/Pullbacks.lean`.
 * `Spec ℤ` is the terminal object.
 * The preceding two results imply that `Scheme` has all finite limits.
 * The empty scheme is the (strict) initial object.
@@ -87,11 +87,11 @@ theorem emptyIsInitial_to : emptyIsInitial.to = Scheme.emptyTo :=
 instance : IsEmpty Scheme.empty.carrier :=
   show IsEmpty PEmpty by infer_instance
 
-instance spec_pUnit_isEmpty : IsEmpty (Scheme.Spec.obj (op <| CommRingCat.of PUnit)).carrier :=
+instance spec_punit_isEmpty : IsEmpty (Scheme.Spec.obj (op <| CommRingCat.of PUnit)).carrier :=
   ⟨PrimeSpectrum.pUnit⟩
-#align algebraic_geometry.Spec_punit_is_empty AlgebraicGeometry.spec_pUnit_isEmpty
+#align algebraic_geometry.Spec_punit_is_empty AlgebraicGeometry.spec_punit_isEmpty
 
-instance (priority := 100) isOpenImmersionCat_of_isEmpty {X Y : Scheme} (f : X ⟶ Y)
+instance (priority := 100) isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶ Y)
     [IsEmpty X.carrier] : IsOpenImmersion f := by
   apply (config := { allowSynthFailures := true }) IsOpenImmersion.of_stalk_iso
   · apply openEmbedding_of_continuous_injective_open
@@ -102,7 +102,7 @@ instance (priority := 100) isOpenImmersionCat_of_isEmpty {X Y : Scheme} (f : X 
     · intro U _; convert isOpen_empty (α := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff]
       exact fun x => isEmptyElim (show X.carrier from x.choose)
   · rintro (i : X.carrier); exact isEmptyElim i
-#align algebraic_geometry.is_open_immersion_of_is_empty AlgebraicGeometry.isOpenImmersionCat_of_isEmpty
+#align algebraic_geometry.is_open_immersion_of_is_empty AlgebraicGeometry.isOpenImmersion_of_isEmpty
 
 instance (priority := 100) isIso_of_isEmpty {X Y : Scheme} (f : X ⟶ Y) [IsEmpty Y.carrier] :
     IsIso f := by

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -305,7 +305,7 @@ variable (s : PullbackCone f g)
 /-- (Implementation)
 The canonical map `(s.X ×[X] Uᵢ) ×[s.X] (s.X ×[X] Uⱼ) ⟶ (Uᵢ ×[Z] Y) ×[X] Uⱼ`
 
-This is used in `glued_lift`. -/
+This is used in `gluedLift`. -/
 def gluedLiftPullbackMap (i j : 𝒰.J) :
     pullback ((𝒰.pullbackCover s.fst).map i) ((𝒰.pullbackCover s.fst).map j) ⟶
       (gluing 𝒰 f g).V ⟨i, j⟩ := by
@@ -326,7 +326,7 @@ theorem gluedLiftPullbackMap_fst (i j : 𝒰.J) :
           pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition := by
   delta gluedLiftPullbackMap
   -- Porting note : the original set of simp lemma is not sufficient, but as this is terminal
-  -- I just let `simp` does it work
+  -- I just let `simp` do its work
   simp
 #align algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_fst AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
 
@@ -335,7 +335,7 @@ theorem gluedLiftPullbackMap_snd (i j : 𝒰.J) :
     gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.snd = pullback.snd ≫ pullback.snd := by
   delta gluedLiftPullbackMap
   -- Porting note : the original set of simp lemma is not sufficient, but as this is terminal
-  -- I just let `simp` does it work
+  -- I just let `simp` do its work
   simp
 #align algebraic_geometry.Scheme.pullback.glued_lift_pullback_map_snd AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd
 
@@ -347,7 +347,7 @@ Given a pullback cone `s`, we have the maps `s.fst ⁻¹' Uᵢ ⟶ Uᵢ` and
 
 to glue these into a map `s.X ⟶ Uᵢ ×[Z] Y`, we need to show that the maps agree on
 `(s.fst ⁻¹' Uᵢ) ×[s.X] (s.fst ⁻¹' Uⱼ) ⟶ Uᵢ ×[Z] Y`. This is achieved by showing that both of these
-maps factors through `glued_lift_pullback_map`.
+maps factors through `gluedLiftPullbackMap`.
 -/
 def gluedLift : s.pt ⟶ (gluing 𝒰 f g).glued := by
   fapply (𝒰.pullbackCover s.fst).glueMorphisms
@@ -540,8 +540,7 @@ def gluedIsLimit : IsLimit (PullbackCone.mk _ _ (p_comm 𝒰 f g)) := by
   simp_rw [← Category.assoc]
   congr 1
   apply pullback.hom_ext
-  ·
-    simp only [Category.comp_id, pullbackRightPullbackFstIso_hom_snd, Category.assoc,
+  · simp only [Category.comp_id, pullbackRightPullbackFstIso_hom_snd, Category.assoc,
       pullbackP1Iso_hom_fst, pullback.lift_snd, pullback.lift_fst, pullbackSymmetry_hom_comp_fst]
   · simp only [Category.comp_id, pullbackRightPullbackFstIso_hom_fst_assoc,
       pullbackP1Iso_hom_snd, Category.assoc, pullback.lift_fst_assoc,
@@ -654,7 +653,7 @@ def openCoverOfLeftRight (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶
   apply pullback.hom_ext <;> simp
 #align algebraic_geometry.Scheme.pullback.open_cover_of_left_right AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight
 
-/-- (Implementation). Use `open_cover_of_base` instead. -/
+/-- (Implementation). Use `openCoverOfBase` instead. -/
 @[simps! map]
 def openCoverOfBase' (𝒰 : OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCover (pullback f g) := by
   apply (openCoverOfLeft (𝒰.pullbackCover f) f g).bind