chore: tidy various files (#3483)

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -78,16 +78,16 @@ instance densely_ordered [Preorder α] [DenselyOrdered α] {a : α} :
   show DenselyOrdered (Ici a) from instDenselyOrderedElemLtToLTMemSetInstMembershipSet
 #align nonneg.densely_ordered Nonneg.densely_ordered
 
-/-- If `Sup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`. -/
+/-- If `supₛ ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`. -/
 @[reducible]
 protected noncomputable def conditionallyCompleteLinearOrder [ConditionallyCompleteLinearOrder α]
     {a : α} : ConditionallyCompleteLinearOrder { x : α // a ≤ x } :=
   { @ordConnectedSubsetConditionallyCompleteLinearOrder α (Set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ with }
 #align nonneg.conditionally_complete_linear_order Nonneg.conditionallyCompleteLinearOrder
 
-/-- If `Sup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrderBot`.
+/-- If `supₛ ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrderBot`.
 
-This instance uses data fields from `Subtype.LinearOrder` to help type-class inference.
+This instance uses data fields from `Subtype.linearOrder` to help type-class inference.
 The `Set.Ici` data fields are definitionally equal, but that requires unfolding semireducible
 definitions, so type-class inference won't see this. -/
 @[reducible]
@@ -122,10 +122,10 @@ theorem mk_eq_zero [Zero α] [Preorder α] {x : α} (hx : 0 ≤ x) :
   Subtype.ext_iff
 #align nonneg.mk_eq_zero Nonneg.mk_eq_zero
 
-instance hasAdd [AddZeroClass α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] :
+instance add [AddZeroClass α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] :
     Add { x : α // 0 ≤ x } :=
   ⟨fun x y => ⟨x + y, add_nonneg x.2 y.2⟩⟩
-#align nonneg.has_add Nonneg.hasAdd
+#align nonneg.has_add Nonneg.add
 
 @[simp]
 theorem mk_add_mk [AddZeroClass α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] {x y : α}
@@ -140,10 +140,10 @@ protected theorem coe_add [AddZeroClass α] [Preorder α] [CovariantClass α α
   rfl
 #align nonneg.coe_add Nonneg.coe_add
 
-instance NSMul [AddMonoid α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] :
+instance nsmul [AddMonoid α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] :
     SMul ℕ { x : α // 0 ≤ x } :=
   ⟨fun n x => ⟨n • (x : α), nsmul_nonneg x.prop n⟩⟩
-#align nonneg.has_nsmul Nonneg.NSMul
+#align nonneg.has_nsmul Nonneg.nsmul
 
 @[simp]
 theorem nsmul_mk [AddMonoid α] [Preorder α] [CovariantClass α α (· + ·) (· ≤ ·)] (n : ℕ) {x : α}
@@ -180,7 +180,7 @@ instance linearOrderedCancelAddCommMonoid [LinearOrderedCancelAddCommMonoid α]
     (fun _ _ => rfl) fun _ _ => rfl
 #align nonneg.linear_ordered_cancel_add_comm_monoid Nonneg.linearOrderedCancelAddCommMonoid
 
-/-- Coercion `{x : α // 0 ≤ x} → α` as a `add_monoid_hom`. -/
+/-- Coercion `{x : α // 0 ≤ x} → α` as a `AddMonoidHom`. -/
 def coeAddMonoidHom [OrderedAddCommMonoid α] : { x : α // 0 ≤ x } →+ α :=
   { toFun := ((↑) : { x : α // 0 ≤ x } → α)
     map_zero' := Nonneg.coe_zero
@@ -311,19 +311,15 @@ instance linearOrderedSemiring [LinearOrderedSemiring α] :
     (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 #align nonneg.linear_ordered_semiring Nonneg.linearOrderedSemiring
 
--- Porting note: was
--- `{ Nonneg.linearOrderedSemiring, Nonneg.orderedCommSemiring with`
--- changing the order somehow prevented a timeout... also adding `(α := α)`
--- helped. Both can be reverted once stuff is fixed.
 instance linearOrderedCommMonoidWithZero [LinearOrderedCommRing α] :
     LinearOrderedCommMonoidWithZero { x : α // 0 ≤ x } :=
-  { Nonneg.orderedCommSemiring, Nonneg.linearOrderedSemiring with
-    mul_le_mul_left := fun _ _ h c ↦ mul_le_mul_of_nonneg_left h c.prop (α := α) }
+  { Nonneg.linearOrderedSemiring, Nonneg.orderedCommSemiring with
+    mul_le_mul_left := fun _ _ h c ↦ mul_le_mul_of_nonneg_left h c.prop }
 #align nonneg.linear_ordered_comm_monoid_with_zero Nonneg.linearOrderedCommMonoidWithZero
 
 /-- Coercion `{x : α // 0 ≤ x} → α` as a `RingHom`. -/
 def coeRingHom [OrderedSemiring α] : { x : α // 0 ≤ x } →+* α :=
-  { toFun :=((↑) : { x : α // 0 ≤ x } → α)
+  { toFun := ((↑) : { x : α // 0 ≤ x } → α)
     map_one' := Nonneg.coe_one
     map_mul' := Nonneg.coe_mul
     map_zero' := Nonneg.coe_zero,
@@ -334,7 +330,7 @@ instance canonicallyOrderedAddMonoid [OrderedRing α] :
     CanonicallyOrderedAddMonoid { x : α // 0 ≤ x } :=
   { Nonneg.orderedAddCommMonoid, Nonneg.orderBot with
     le_self_add := fun _ b => le_add_of_nonneg_right b.2
-    exists_add_of_le := @fun a b h =>
+    exists_add_of_le := fun {a b} h =>
       ⟨⟨b - a, sub_nonneg_of_le h⟩, Subtype.ext (add_sub_cancel'_right _ _).symm⟩ }
 #align nonneg.canonically_ordered_add_monoid Nonneg.canonicallyOrderedAddMonoid
 
@@ -381,8 +377,7 @@ theorem toNonneg_le {a : α} {b : { x : α // 0 ≤ x }} : toNonneg a ≤ b ↔
 #align nonneg.to_nonneg_le Nonneg.toNonneg_le
 
 @[simp]
-theorem toNonneg_lt {a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b :=
-  by
+theorem toNonneg_lt {a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b := by
   cases' a with a ha
   simp [toNonneg, ha.not_lt]
 #align nonneg.to_nonneg_lt Nonneg.toNonneg_lt

Mathlib/CategoryTheory/Arrow.lean

@@ -123,7 +123,7 @@ theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) :
   sq.w
 #align category_theory.arrow.w_mk_right CategoryTheory.Arrow.w_mk_right
 
-theorem isIso_of_iso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
+theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
     [IsIso ff.right] : IsIso ff where
   out := by
     let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
@@ -135,7 +135,7 @@ theorem isIso_of_iso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso f
     · apply CommaMorphism.ext
       · rw [Comma.comp_left, IsIso.inv_hom_id, ←Comma.id_left]
       · rw [Comma.comp_right, IsIso.inv_hom_id, ←Comma.id_right]
-#align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right
+#align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right
 
 /-- Create an isomorphism between arrows,
 by providing isomorphisms between the domains and codomains,

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -16,23 +16,23 @@ import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 # Concrete categories
 
 A concrete category is a category `C` with a fixed faithful functor
-`forget : C ⥤ Type*`.  We define concrete categories using `class
+`forget : C ⥤ Type _`.  We define concrete categories using `class
 concrete_category`.  In particular, we impose no restrictions on the
 carrier type `C`, so `Type` is a concrete category with the identity
 forgetful functor.
 
 Each concrete category `C` comes with a canonical faithful functor
-`forget C : C ⥤ Type*`.  We say that a concrete category `C` admits a
+`forget C : C ⥤ Type _`.  We say that a concrete category `C` admits a
 *forgetful functor* to a concrete category `D`, if it has a functor
 `forget₂ C D : C ⥤ D` such that `(forget₂ C D) ⋙ (forget D) = forget C`,
-see `class has_forget₂`.  Due to `faithful.div_comp`, it suffices
+see `class HasForget₂`.  Due to `Faithful.div_comp`, it suffices
 to verify that `forget₂.obj` and `forget₂.map` agree with the equality
 above; then `forget₂` will satisfy the functor laws automatically, see
-`has_forget₂.mk'`.
+`HasForget₂.mk'`.
 
 Two classes helping construct concrete categories in the two most
-common cases are provided in the files `bundled_hom` and
-`unbundled_hom`, see their documentation for details.
+common cases are provided in the files `BundledHom` and
+`UnbundledHom`, see their documentation for details.
 
 ## References
 

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

@@ -314,7 +314,7 @@ variable {f g : X ⟶ Y}
 /-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms
     `t.π.app zero : t.pt ⟶ X`
     and `t.π.app one : t.pt ⟶ Y`. Of these, only the first one is interesting, and we give it the
-    shorter name `fork.ι t`. -/
+    shorter name `Fork.ι t`. -/
 def Fork.ι (t : Fork f g) :=
   t.π.app zero
 #align category_theory.limits.fork.ι CategoryTheory.Limits.Fork.ι
@@ -326,7 +326,7 @@ theorem Fork.app_zero_eq_ι (t : Fork f g) : t.π.app zero = t.ι :=
 
 /-- A cofork `t` on the parallelPair `f g : X ⟶ Y` consists of two morphisms
     `t.ι.app zero : X ⟶ t.pt` and `t.ι.app one : Y ⟶ t.pt`. Of these, only the second one is
-    interesting, and we give it the shorter name `cofork.π t`. -/
+    interesting, and we give it the shorter name `Cofork.π t`. -/
 def Cofork.π (t : Cofork f g) :=
   t.ι.app one
 #align category_theory.limits.cofork.π CategoryTheory.Limits.Cofork.π
@@ -359,8 +359,7 @@ theorem Cofork.app_zero_eq_comp_π_right (s : Cofork f g) : s.ι.app zero = g 
 /-- A fork on `f g : X ⟶ Y` is determined by the morphism `ι : P ⟶ X` satisfying `ι ≫ f = ι ≫ g`.
 -/
 @[simps]
-def Fork.ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g
-    where
+def Fork.ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g where
   pt := P
   π :=
     { app := fun X => by cases X; exact ι; exact ι ≫ f
@@ -371,8 +370,7 @@ def Fork.ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g
 /-- A cofork on `f g : X ⟶ Y` is determined by the morphism `π : Y ⟶ P` satisfying
     `f ≫ π = g ≫ π`. -/
 @[simps]
-def Cofork.ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : Cofork f g
-    where
+def Cofork.ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : Cofork f g where
   pt := P
   ι :=
     { app := fun X => WalkingParallelPair.casesOn X (f ≫ π) π
@@ -595,7 +593,7 @@ theorem Cofork.IsColimit.homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Cofork f
     `parallelPair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`,
     we get a cone on `F`.
 
-    If you're thinking about using this, have a look at `has_equalizers_of_has_limit_parallel_pair`,
+    If you're thinking about using this, have a look at `hasEqualizers_of_hasLimit_parallelPair`,
     which you may find to be an easier way of achieving your goal. -/
 def Cone.ofFork {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) : Cone F
     where
@@ -732,7 +730,7 @@ def Cofork.ext {s t : Cofork f g} (i : s.pt ≅ t.pt) (w : s.π ≫ i.hom = t.π
   inv := Cofork.mkHom i.inv (by rw [Iso.comp_inv_eq, w])
 #align category_theory.limits.cofork.ext CategoryTheory.Limits.Cofork.ext
 
-/-- Every cofork is isomorphic to one of the form `cofork.of_π _ _`. -/
+/-- Every cofork is isomorphic to one of the form `Cofork.ofπ _ _`. -/
 def Cofork.isoCoforkOfπ (c : Cofork f g) : c ≅ Cofork.ofπ c.π c.condition :=
   Cofork.ext (by simp only [Cofork.ofπ_pt, Functor.const_obj_obj]; rfl) (by dsimp; simp)
 #align category_theory.limits.cofork.iso_cofork_of_π CategoryTheory.Limits.Cofork.isoCoforkOfπ
@@ -852,8 +850,7 @@ def idFork (h : f = g) : Fork f g :=
 
 /-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`. -/
 def isLimitIdFork (h : f = g) : IsLimit (idFork h) :=
-  Fork.IsLimit.mk _ (fun s => Fork.ι s) (fun s => Category.comp_id _) fun s m h =>
-    by
+  Fork.IsLimit.mk _ (fun s => Fork.ι s) (fun s => Category.comp_id _) fun s m h => by
     convert h
     exact (Category.comp_id _).symm
 #align category_theory.limits.is_limit_id_fork CategoryTheory.Limits.isLimitIdFork
@@ -1042,8 +1039,7 @@ def idCofork (h : f = g) : Cofork f g :=
 
 /-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`.  -/
 def isColimitIdCofork (h : f = g) : IsColimit (idCofork h) :=
-  Cofork.IsColimit.mk _ (fun s => Cofork.π s) (fun s => Category.id_comp _) fun s m h =>
-    by
+  Cofork.IsColimit.mk _ (fun s => Cofork.π s) (fun s => Category.id_comp _) fun s m h => by
     convert h
     exact (Category.id_comp _).symm
 #align category_theory.limits.is_colimit_id_cofork CategoryTheory.Limits.isColimitIdCofork

Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

@@ -91,7 +91,7 @@ This is often called 'finitely cocomplete'.
 -/
 class HasFiniteColimits : Prop where
   /-- `C` has all colimits over any type `J` whose objects and morphisms lie in the same universe
-  and which has `FinType` objects and morphisms-/
+  and which has `Fintype` objects and morphisms-/
   out (J : Type) [𝒥 : SmallCategory J] [@FinCategory J 𝒥] : @HasColimitsOfShape J 𝒥 C _
 #align category_theory.limits.has_finite_colimits CategoryTheory.Limits.HasFiniteColimits
 
@@ -213,12 +213,12 @@ instance fintypeHom (j j' : WidePushoutShape J) : Fintype (j ⟶ j') where
 
 end WidePushoutShape
 
-instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J)
-    where fintypeHom := WidePullbackShape.fintypeHom
+instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J) where
+  fintypeHom := WidePullbackShape.fintypeHom
 #align category_theory.limits.fin_category_wide_pullback CategoryTheory.Limits.finCategoryWidePullback
 
-instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J)
-    where fintypeHom := WidePushoutShape.fintypeHom
+instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J) where
+  fintypeHom := WidePushoutShape.fintypeHom
 #align category_theory.limits.fin_category_wide_pushout CategoryTheory.Limits.finCategoryWidePushout
 
 -- We can't just made this an `abbreviation`

Mathlib/GroupTheory/OrderOfElement.lean

@@ -59,7 +59,7 @@ theorem isPeriodicPt_mul_iff_pow_eq_one (x : G) : IsPeriodicPt ((· * ·) x) n 1
 
 /-- `IsOfFinOrder` is a predicate on an element `x` of a monoid to be of finite order, i.e. there
 exists `n ≥ 1` such that `x ^ n = 1`.-/
-@[to_additive "`isOfFinAddOrder` is a predicate on an element `a` of an
+@[to_additive "`IsOfFinAddOrder` is a predicate on an element `a` of an
 additive monoid to be of finite order, i.e. there exists `n ≥ 1` such that `n • a = 0`."]
 def IsOfFinOrder (x : G) : Prop :=
   (1 : G) ∈ periodicPts ((· * ·) x)

Mathlib/LinearAlgebra/Dimension.lean

@@ -919,7 +919,7 @@ variable (R)
 
 @[simp]
 theorem rank_self : Module.rank R R = 1 := by
-  rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_pUnit]
+  rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
 #align rank_self rank_self
 
 end StrongRankCondition

Mathlib/MeasureTheory/MeasurableSpace.lean

@@ -21,7 +21,7 @@ import Mathlib.Data.Set.UnionLift
 # Measurable spaces and measurable functions
 
 This file provides properties of measurable spaces and the functions and isomorphisms
-between them. The definition of a measurable space is in `measure_theory.measurable_space_def`.
+between them. The definition of a measurable space is in `MeasureTheory.MeasurableSpaceDef`.
 
 A measurable space is a set equipped with a σ-algebra, a collection of
 subsets closed under complementation and countable union. A function
@@ -358,8 +358,7 @@ theorem Measurable.measurable_of_countable_ne [MeasurableSingletonClass α] (hf
     simp [← inter_union_distrib_left]
   rw [this]
   refine (h.mono (inter_subset_right _ _)).measurableSet.union ?_
-  have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } :=
-    by
+  have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } := by
     ext x
     simp (config := { contextual := true })
   rw [this]
@@ -412,15 +411,15 @@ theorem measurable_to_nat {f : α → ℕ} : (∀ y, MeasurableSet (f ⁻¹' {f
   measurable_to_countable
 #align measurable_to_nat measurable_to_nat
 
-theorem measurable_find_greatest' {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N : ℕ}
+theorem measurable_findGreatest' {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N : ℕ}
     (hN : ∀ k ≤ N, MeasurableSet { x | Nat.findGreatest (p x) N = k }) :
     Measurable fun x => Nat.findGreatest (p x) N :=
   measurable_to_nat fun _ => hN _ N.findGreatest_le
-#align measurable_find_greatest' measurable_find_greatest'
+#align measurable_find_greatest' measurable_findGreatest'
 
 theorem measurable_findGreatest {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] {N}
     (hN : ∀ k ≤ N, MeasurableSet { x | p x k }) : Measurable fun x => Nat.findGreatest (p x) N := by
-  refine' measurable_find_greatest' fun k hk => _
+  refine' measurable_findGreatest' fun k hk => _
   simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]
   repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.interᵢ,
     MeasurableSet.compl, hN] <;> try intros
@@ -894,13 +893,13 @@ theorem measurable_piEquivPiSubtypeProd (p : δ → Prop) [DecidablePred p] :
 
 end Pi
 
-instance Tprod.measurableSpace (π : δ → Type _) [∀ x, MeasurableSpace (π x)] :
+instance TProd.measurableSpace (π : δ → Type _) [∀ x, MeasurableSpace (π x)] :
     ∀ l : List δ, MeasurableSpace (List.TProd π l)
   | [] => instMeasurableSpacePUnit
-  | _::is => @instMeasurableSpaceProd _ _ _ (Tprod.measurableSpace π is)
-#align tprod.measurable_space Tprod.measurableSpace
+  | _::is => @instMeasurableSpaceProd _ _ _ (TProd.measurableSpace π is)
+#align tprod.measurable_space TProd.measurableSpace
 
-section Tprod
+section TProd
 
 open List
 
@@ -935,7 +934,7 @@ theorem MeasurableSet.tProd (l : List δ) {s : ∀ i, Set (π i)} (hs : ∀ i, M
   exact (hs i).prod ih
 #align measurable_set.tprod MeasurableSet.tProd
 
-end Tprod
+end TProd
 
 instance {α β} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] : MeasurableSpace (α ⊕ β) :=
   m₁.map Sum.inl ⊓ m₂.map Sum.inr
@@ -1294,8 +1293,7 @@ protected def cast {α β} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace 
 protected theorem measurable_comp_iff {f : β → γ} (e : α ≃ᵐ β) :
     Measurable (f ∘ e) ↔ Measurable f :=
   Iff.intro
-    (fun hfe =>
-      by
+    (fun hfe => by
       have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
       rwa [coe_toEquiv, symm_trans_self] at this)
     fun h => h.comp e.measurable
@@ -1431,12 +1429,12 @@ def piCongrRight (e : ∀ a, π a ≃ᵐ π' a) : (∀ a, π a) ≃ᵐ ∀ a, π
 
 /-- Pi-types are measurably equivalent to iterated products. -/
 @[simps! (config := { fullyApplied := false })]
-def piMeasurableEquivTprod [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ i, i ∈ l) :
+def piMeasurableEquivTProd [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ i, i ∈ l) :
     (∀ i, π i) ≃ᵐ List.TProd π l where
   toEquiv := List.TProd.piEquivTProd hnd h
   measurable_toFun := measurable_tProd_mk l
   measurable_invFun := measurable_tProd_elim' h
-#align measurable_equiv.pi_measurable_equiv_tprod MeasurableEquiv.piMeasurableEquivTprod
+#align measurable_equiv.pi_measurable_equiv_tprod MeasurableEquiv.piMeasurableEquivTProd
 
 /-- If `α` has a unique term, then the type of function `α → β` is measurably equivalent to `β`. -/
 @[simps! (config := { fullyApplied := false })]
@@ -1660,7 +1658,7 @@ end Filter
 /-- We say that a collection of sets is countably spanning if a countable subset spans the
   whole type. This is a useful condition in various parts of measure theory. For example, it is
   a needed condition to show that the product of two collections generate the product sigma algebra,
-  see `generate_from_prod_eq`. -/
+  see `generateFrom_prod_eq`. -/
 def IsCountablySpanning (C : Set (Set α)) : Prop :=
   ∃ s : ℕ → Set α, (∀ n, s n ∈ C) ∧ (⋃ n, s n) = univ
 #align is_countably_spanning IsCountablySpanning