chore: tidy various files (#4304)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -24,9 +24,7 @@ the underlying types are just the limits in the category of types.
 -/
 
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 universe v u
 
@@ -52,15 +50,12 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.add_group_obj AddGroupCat.addGroupObj
 
-/-- The flat sections of a functor into `Group` form a subgroup of all sections.
+/-- The flat sections of a functor into `GroupCat` form a subgroup of all sections.
 -/
 @[to_additive
-  "The flat sections of a functor into `AddGroup` form an additive subgroup of all sections."]
+  "The flat sections of a functor into `AddGroupCat` form an additive subgroup of all sections."]
 def sectionsSubgroup (F : J ⥤ GroupCat) : Subgroup (∀ j, F.obj j) :=
-  {
-    MonCat.sectionsSubmonoid
-      (F ⋙ forget₂ GroupCat
-          MonCat) with
+  { MonCat.sectionsSubmonoid (F ⋙ forget₂ GroupCat MonCat) with
     carrier := (F ⋙ forget GroupCat).sections
     inv_mem' := fun {a} ah j j' f => by
       simp only [Functor.comp_map, Pi.inv_apply, MonoidHom.map_inv, inv_inj]
@@ -81,17 +76,17 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.limit_add_group AddGroupCat.limitAddGroup
 
-/-- We show that the forgetful functor `Group ⥤ Mon` creates limits.
+/-- We show that the forgetful functor `GroupCat ⥤ MonCat` creates limits.
 
-All we need to do is notice that the limit point has a `group` instance available, and then reuse
+All we need to do is notice that the limit point has a `Group` instance available, and then reuse
 the existing limit. -/
-@[to_additive "We show that the forgetful functor `AddGroup ⥤ AddMon` creates limits.
+@[to_additive "We show that the forgetful functor `AddGroupCat ⥤ AddMonCat` creates limits.
 
-All we need to do is notice that the limit point has an `add_group` instance available, and then
+All we need to do is notice that the limit point has an `AddGroup` instance available, and then
 reuse the existing limit."]
 noncomputable instance Forget₂.createsLimit (F : J ⥤ GroupCatMax.{v, u}) :
     CreatesLimit F (forget₂ GroupCatMax.{v, u} MonCatMax.{v, u}) :=
-  -- Porting note: need to add `forget₂ Grp Mon` reflects isomorphism
+  -- Porting note: need to add `forget₂ GrpCat MonCat` reflects isomorphism
   letI : ReflectsIsomorphisms (forget₂ GroupCatMax.{v, u} MonCatMax.{v, u}) :=
     CategoryTheory.reflectsIsomorphisms_forget₂ _ _
   createsLimitOfReflectsIso (K := F) (F := (forget₂ GroupCat.{max v u} MonCat.{max v u}))
@@ -112,10 +107,10 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.forget₂.creates_limit AddGroupCat.Forget₂.createsLimit
 
-/-- A choice of limit cone for a functor into `Group`.
+/-- A choice of limit cone for a functor into `GroupCat`.
 (Generally, you'll just want to use `limit F`.)
 -/
-@[to_additive "A choice of limit cone for a functor into `Group`.
+@[to_additive "A choice of limit cone for a functor into `GroupCat`.
   (Generally, you'll just want to use `limit F`.)"]
 noncomputable def limitCone (F : J ⥤ GroupCatMax.{v, u}) : Cone F :=
   -- Porting note: add this instance to help Lean unify universe levels
@@ -172,8 +167,8 @@ This means the underlying monoid of a limit can be computed as a limit in the ca
   This means the underlying additive monoid of a limit can be computed as a limit in the category of
   additive monoids."]
 noncomputable instance forget₂MonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ GroupCatMax.{v, u} MonCat.{max v u})
-    where preservesLimitsOfShape {J _} := { preservesLimit := fun {F} =>
+    PreservesLimitsOfSize.{v, v} (forget₂ GroupCatMax.{v, u} MonCat.{max v u}) where
+  preservesLimitsOfShape {J _} := { preservesLimit := fun {F} =>
       -- Porting note: add this instance to help Lean unify universe levels
       letI : HasLimit (F ⋙ forget₂ GroupCatMax.{v, u} MonCat.{max v u}) :=
         (MonCat.hasLimitsOfSize.{v, u}.1 J).1 _
@@ -255,14 +250,14 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.limit_add_comm_group AddCommGroupCat.limitAddCommGroup
 
-/-- We show that the forgetful functor `CommGroup ⥤ Group` creates limits.
+/-- We show that the forgetful functor `CommGroupCat ⥤ GroupCat` creates limits.
 
-All we need to do is notice that the limit point has a `comm_group` instance available,
+All we need to do is notice that the limit point has a `CommGroup` instance available,
 and then reuse the existing limit.
 -/
-@[to_additive "We show that the forgetful functor `AddCommGroup ⥤ AddGroup` creates limits.
+@[to_additive "We show that the forgetful functor `AddCommGroupCat ⥤ AddGroupCat` creates limits.
 
-  All we need to do is notice that the limit point has an `add_comm_group` instance available,
+  All we need to do is notice that the limit point has an `AddCommGroup` instance available,
   and then reuse the existing limit."]
 noncomputable instance Forget₂.createsLimit (F : J ⥤ CommGroupCatMax.{v, u}) :
     CreatesLimit F (forget₂ CommGroupCat GroupCatMax.{v, u}) :=
@@ -284,11 +279,11 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.forget₂.creates_limit AddCommGroupCat.Forget₂.createsLimit
 
-/-- A choice of limit cone for a functor into `CommGroup`.
+/-- A choice of limit cone for a functor into `CommGroupCat`.
 (Generally, you'll just want to use `limit F`.)
 -/
 @[to_additive
-  "A choice of limit cone for a functor into `CommGroup`.
+  "A choice of limit cone for a functor into `AddCommGroupCat`.
   (Generally, you'll just want to use `limit F`.)"]
 noncomputable def limitCone (F : J ⥤ CommGroupCat.{max v u}) : Cone F :=
   liftLimit (limit.isLimit (F ⋙ forget₂ CommGroupCatMax.{v, u} GroupCatMax.{v, u}))
@@ -302,7 +297,7 @@ set_option linter.uppercaseLean3 false in
 -/
 @[to_additive
   "The chosen cone is a limit cone.
-  (Generally, you'll just wantto use `limit.cone F`.)"]
+  (Generally, you'll just want to use `limit.cone F`.)"]
 noncomputable def limitConeIsLimit (F : J ⥤ CommGroupCatMax.{v, u}) :
     IsLimit (limitCone.{v, u} F) :=
   liftedLimitIsLimit _
@@ -376,10 +371,9 @@ in the category of commutative monoids.)
   preserves all limits. (That is, the underlying additive commutative monoids could have been
   computed instead as limits in the category of additive commutative monoids.)"]
 noncomputable instance forget₂CommMonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCat CommMonCat.{max v u})
-    where preservesLimitsOfShape :=
-    {
-      preservesLimit := fun {F} =>
+    PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCat CommMonCat.{max v u}) where
+  preservesLimitsOfShape :=
+    { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit.{v, u} F)
           (forget₂CommMonPreservesLimitsAux.{v, u} F) }
 set_option linter.uppercaseLean3 false in
@@ -395,8 +389,8 @@ underlying types could have been computed instead as limits in the category of t
   (That is, the underlying types could have been computed instead as limits in the category of
   types.)"]
 noncomputable instance forgetPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget CommGroupCatMax.{v, u})
-  where preservesLimitsOfShape {J _} :=
+    PreservesLimitsOfSize.{v, v} (forget CommGroupCatMax.{v, u}) where
+  preservesLimitsOfShape {J _} :=
   { preservesLimit := fun {F} =>
     -- Porting note : add these instance to help Lean unify universe levels
     letI : HasLimit (F ⋙ forget₂ CommGroupCatMax.{v, u} GroupCat.{max v u}) :=
@@ -416,7 +410,7 @@ end CommGroupCat
 
 namespace AddCommGroupCat
 
-/-- The categorical kernel of a morphism in `AddCommGroup`
+/-- The categorical kernel of a morphism in `AddCommGroupCat`
 agrees with the usual group-theoretical kernel.
 -/
 def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :

Mathlib/Algebra/Category/Ring/Instances.lean

@@ -24,11 +24,11 @@ instance localization_unit_isIso (R : CommRingCat) :
   IsIso.of_iso (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso
 #align localization_unit_is_iso localization_unit_isIso
 
-instance localization_unit_is_iso' (R : CommRingCat) :
+instance localization_unit_isIso' (R : CommRingCat) :
     @IsIso CommRingCat _ R _ (CommRingCat.ofHom <| algebraMap R (Localization.Away (1 : R))) := by
   cases R
   exact localization_unit_isIso _
-#align localization_unit_is_iso' localization_unit_is_iso'
+#align localization_unit_is_iso' localization_unit_isIso'
 
 theorem IsLocalization.epi {R : Type _} [CommRing R] (M : Submonoid R) (S : Type _) [CommRing S]
     [Algebra R S] [IsLocalization M S] : Epi (CommRingCat.ofHom <| algebraMap R S) :=

Mathlib/Algebra/Module/Bimodule.lean

@@ -39,22 +39,22 @@ This file is a place to collect results which are specific to bimodules.
 
 ## Main definitions
 
- * `subbimodule.mk`
- * `subbimodule.smul_mem`
- * `subbimodule.smul_mem'`
- * `subbimodule.to_submodule`
- * `subbimodule.to_submodule'`
+ * `Subbimodule.mk`
+ * `Subbimodule.smul_mem`
+ * `Subbimodule.smul_mem'`
+ * `Subbimodule.toSubmodule`
+ * `Subbimodule.toSubmodule'`
 
 ## Implementation details
 
 For many definitions and lemmas it is preferable to set things up without opposites, i.e., as:
-`[module S M] [smul_comm_class R S M]` rather than `[module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]`.
+`[Module S M] [SMulCommClass R S M]` rather than `[Module Sᵐᵒᵖ M] [SMulCommClass R Sᵐᵒᵖ M]`.
 The corresponding results for opposites then follow automatically and do not require taking
 advantage of the fact that `(Sᵐᵒᵖ)ᵐᵒᵖ` is defeq to `S`.
 
 ## TODO
 
-Develop the theory of two-sided ideals, which have type `submodule (R ⊗[ℕ] Rᵐᵒᵖ) R`.
+Develop the theory of two-sided ideals, which have type `Submodule (R ⊗[ℕ] Rᵐᵒᵖ) R`.
 
 -/
 
@@ -83,7 +83,7 @@ variable [SMulCommClass A B M]
 individually, rather than jointly via their tensor product.
 
 Note that `R` plays no role but it is convenient to make this generalisation to support the cases
-`R = ℕ` and `R = ℤ` which both show up naturally. See also `base_change`. -/
+`R = ℕ` and `R = ℤ` which both show up naturally. See also `Subbimodule.baseChange`. -/
 @[simps]
 def mk (p : AddSubmonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p)
     (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) : Submodule (A ⊗[R] B) M :=
@@ -155,4 +155,3 @@ def toSubbimoduleNat (p : Submodule (R ⊗[ℤ] S) M) : Submodule (R ⊗[ℕ] S)
 end Ring
 
 end Subbimodule
-

Mathlib/Analysis/Complex/Basic.lean

@@ -292,12 +292,12 @@ theorem imClm_apply (z : ℂ) : (imClm : ℂ → ℝ) z = z.im :=
   rfl
 #align complex.im_clm_apply Complex.imClm_apply
 
-theorem restrictScalars_one_smul_right' (x : E) :
+theorem restrictScalars_one_smulRight' (x : E) :
     ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] E) =
       reClm.smulRight x + I • imClm.smulRight x := by
   ext ⟨a, b⟩
   simp [mk_eq_add_mul_I, mul_smul, smul_comm I b x]
-#align complex.restrict_scalars_one_smul_right' Complex.restrictScalars_one_smul_right'
+#align complex.restrict_scalars_one_smul_right' Complex.restrictScalars_one_smulRight'
 
 theorem restrictScalars_one_smulRight (x : ℂ) :
     ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] ℂ) =

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -108,9 +108,9 @@ theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
 #align category_theory.hom_of_le_le_of_hom CategoryTheory.homOfLE_leOfHom
 
 /-- Construct a morphism in the opposite of a preorder category from an inequality. -/
-def opHomOfLe {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
+def opHomOfLE {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
   (homOfLE h).op
-#align category_theory.op_hom_of_le CategoryTheory.opHomOfLe
+#align category_theory.op_hom_of_le CategoryTheory.opHomOfLE
 
 theorem le_of_op_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x :=
   h.unop.le

Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

@@ -116,8 +116,8 @@ def conesEquivCounitIso (B : C) (F : Discrete J ⥤ Over B) :
     (by aesop_cat)
 #align category_theory.over.construct_products.cones_equiv_counit_iso CategoryTheory.Over.ConstructProducts.conesEquivCounitIso
 
--- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and
---       `cones.ext`?
+-- TODO: Can we add `:= by aesop` to the second arguments of `NatIso.ofComponents` and
+--       `Cones.ext`?
 /-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`.
 -/
 @[simps]

Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

@@ -282,7 +282,7 @@ theorem infinite_iff_in_eventualRange {K : (Finset V)ᵒᵖ} (C : G.componentCom
     Set.mem_range, componentComplFunctor_map]
   exact
     ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
-      h (Opposite.op L) (opHomOfLe KL)⟩
+      h (Opposite.op L) (opHomOfLE KL)⟩
 #align simple_graph.infinite_iff_in_eventual_range SimpleGraph.infinite_iff_in_eventualRange
 
 end Ends

Mathlib/Computability/Partrec.lean

@@ -178,22 +178,25 @@ theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Partrec f) (H : ∀
 #align nat.partrec.of_eq_tot Nat.Partrec.of_eq_tot
 
 theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Partrec f := by
-  induction hf
-  case zero => exact zero
-  case succ => exact succ
-  case left => exact left
-  case right => exact right
-  case pair f g _ _ pf pg =>
+  induction hf with
+  | zero => exact zero
+  | succ => exact succ
+  | left => exact left
+  | right => exact right
+  | pair _ _ pf pg =>
     refine' (pf.pair pg).of_eq_tot fun n => _
     simp [Seq.seq]
-  case comp f g _ _ pf pg =>
+  | comp _ _ pf pg =>
     refine' (pf.comp pg).of_eq_tot fun n => _
     simp
-  case prec f g _ _ pf pg =>
+  | prec _ _ pf pg =>
     refine' (pf.prec pg).of_eq_tot fun n => _
-    simp
-    induction' n.unpair.2 with m IH; · simp
-    simp; exact ⟨_, IH, rfl⟩
+    simp only [unpaired, PFun.coe_val, bind_eq_bind]
+    induction n.unpair.2 with
+    | zero => simp
+    | succ m IH =>
+      simp only [mem_bind_iff, mem_some_iff]
+      exact ⟨_, IH, rfl⟩
 #align nat.partrec.of_primrec Nat.Partrec.of_primrec
 
 protected theorem some : Partrec some :=
@@ -764,14 +767,10 @@ open Computable
 
 theorem option_some_iff {f : α →. σ} : (Partrec fun a => (f a).map Option.some) ↔ Partrec f :=
   ⟨fun h => (Nat.Partrec.ppred.comp h).of_eq fun n => by
-      simp [Part.bind_assoc]
-      -- Porting note: `simp` can't match `Part.some ∘ f` with `fun x => Part.some (f x)`,
-      --               so `conv` & `erw` are needed.
-      conv_lhs =>
-        congr
-        · skip
-        · ext x
-          erw [bind_some_eq_map],
+      -- Porting note: needed to help with applying bind_some_eq_map because `Function.comp` got
+      -- less reducible.
+      simp [Part.bind_assoc, ← Function.comp_apply (f := Part.some) (g := encode), bind_some_eq_map,
+        -Function.comp_apply],
     fun hf => hf.map (option_some.comp snd).to₂⟩
 #align partrec.option_some_iff Partrec.option_some_iff
 

Mathlib/Data/Fin/VecNotation.lean

@@ -338,10 +338,11 @@ theorem vecAlt0_vecAppend (v : Fin n → α) : vecAlt0 rfl (vecAppend rfl v v) =
 theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) : vecAlt1 rfl (vecAppend rfl v v) = v ∘ bit1 := by
   ext i
   simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
-  cases n
-  · cases' i with i hi
+  cases n with
+  | zero =>
+    cases' i with i hi
     simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi; subst i; rfl
-  case succ n =>
+  | succ n =>
     split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
     · simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk]
       rw [Fin.val_mk] at h

Mathlib/GroupTheory/Congruence.lean

@@ -1275,7 +1275,7 @@ instance zpowinst : Pow c.Quotient ℤ :=
 
 /-- The quotient of a group by a congruence relation is a group. -/
 @[to_additive "The quotient of an `AddGroup` by an additive congruence relation is
-an `add_group`."]
+an `AddGroup`."]
 instance group : Group c.Quotient :=
   Function.Surjective.group Quotient.mk''
     Quotient.surjective_Quotient_mk'' rfl (fun _ _ => rfl) (fun _ => rfl)

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -59,9 +59,7 @@ We use this to prove several versions of the Borel isomorphism theorem.
 -/
 
 
-open Set Function PolishSpace PiNat TopologicalSpace Metric Filter
-
-open Topology MeasureTheory Filter
+open Set Function PolishSpace PiNat TopologicalSpace Metric Filter Topology MeasureTheory
 
 variable {α : Type _} [TopologicalSpace α] {ι : Type _}
 
@@ -713,7 +711,7 @@ end MeasureTheory
 /-! ### The Borel Isomorphism Theorem -/
 
 
---Note: Move to topology/metric_space/polish when porting.
+-- Porting note: Move to topology/metric_space/polish when porting.
 instance (priority := 50) polish_of_countable [h : Countable α] [DiscreteTopology α] :
     PolishSpace α := by
   obtain ⟨f, hf⟩ := h.exists_injective_nat
@@ -725,7 +723,7 @@ instance (priority := 50) polish_of_countable [h : Countable α] [DiscreteTopolo
 
 namespace PolishSpace
 
-/-Note: This is to avoid a loop in TC inference. When ported to Lean 4, this will not
+/- Porting note: This is to avoid a loop in TC inference. When ported to Lean 4, this will not
 be necessary, and `secondCountable_of_polish` should probably
 just be added as an instance soon after the definition of `PolishSpace`.-/
 private theorem secondCountable_of_polish [h : PolishSpace α] : SecondCountableTopology α :=
@@ -765,8 +763,7 @@ noncomputable def measurableEquivOfNotCountable (hα : ¬Countable α) (hβ : ¬
 they are Borel isomorphic.-/
 noncomputable def Equiv.measurableEquiv (e : α ≃ β) : α ≃ᵐ β := by
   by_cases h : Countable α
-  · letI := h
-    letI := Countable.of_equiv α e
+  · letI := Countable.of_equiv α e
     refine ⟨e, ?_, ?_⟩ <;> apply measurable_of_countable
   refine' measurableEquivOfNotCountable h _
   rwa [e.countable_iff] at h
@@ -776,7 +773,7 @@ end PolishSpace
 
 namespace MeasureTheory
 
--- todo after the port: move to topology/metric_space/polish
+-- Porting note: todo after the port: move to topology/metric_space/polish
 instance instPolishSpaceUniv [PolishSpace α] : PolishSpace (univ : Set α) :=
   isClosed_univ.polishSpace
 #align measure_theory.set.univ.polish_space MeasureTheory.instPolishSpaceUniv