fix more

mattrobball · mattrobball · commit 9095a3816ff0 · 2023-08-04T13:41:49.000-04:00
diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -238,7 +238,7 @@ theorem mk_neg {M : Type*} [AddCommGroup M] [Module R M] {m : M} {s : S} : mk (-
 #align localized_module.mk_neg LocalizedModule.mk_neg
 
 set_option maxHeartbeats 400000 in
-instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
+instance {A : Type _} [Semiring A] [Algebra R A] {S : Submonoid R} :
     Semiring (LocalizedModule S A) :=
   { show (AddCommMonoid (LocalizedModule S A)) by infer_instance with
     mul := fun m₁ m₂ =>
@@ -297,7 +297,7 @@ instance {A : Type} [Ring A] [Algebra R A] {S : Submonoid R} :
     { inferInstanceAs (AddCommGroup (LocalizedModule S A)),
       inferInstanceAs (Semiring (LocalizedModule S A)) with }
 
-instance {A : Type*} [CommRing A] [Algebra R A] {S : Submonoid R} :
+instance {A : Type _} [CommRing A] [Algebra R A] {S : Submonoid R} :
     CommRing (LocalizedModule S A) :=
   { show (Ring (LocalizedModule S A)) by infer_instance with
     mul_comm := by
diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean
@@ -199,7 +199,7 @@ theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoi
       · exact fun a => (fun i => (Option.rec (pOrder hN (s j)) k i : ℕ)) (finSuccEquiv d a)
       · refine (((@lequivProdOfRightSplitExact _ _ _ _ _ _ _ _ _ _ _ _
           ((f.trans ULift.moduleEquiv.{u, u, v}.symm).toLinearMap.comp <| mkQ _)
-          ((DirectSum.toModule _ _ _ fun i => (liftQSpanSingleton.{u, u} (p ^ k i)
+          ((DirectSum.toModule _ _ _ fun i => (liftQSpanSingleton (p ^ k i)
               (LinearMap.toSpanSingleton _ _ _) (this i).choose_spec.left : R ⧸ _ →ₗ[R] _)).comp
             ULift.moduleEquiv.toLinearMap) (R ∙ s j).injective_subtype ?_ ?_).symm.trans
           (((quotTorsionOfEquivSpanSingleton R N (s j)).symm.trans
diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean
@@ -236,7 +236,7 @@ theorem ι_isoCarrier_inv (i : D.J) :
 
 /-- An equivalence relation on `Σ i, D.U i` that holds iff `𝖣 .ι i x = 𝖣 .ι j y`.
 See `AlgebraicGeometry.Scheme.GlueData.ι_eq_iff`. -/
-def Rel (a b : Σ i, ((D.U i).carrier : Type*)) : Prop :=
+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
 #align algebraic_geometry.Scheme.glue_data.rel AlgebraicGeometry.Scheme.GlueData.Rel
diff --git a/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean b/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean
@@ -59,8 +59,8 @@ def toTopCat : TopCat :=
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.to_Top AlgebraicGeometry.LocallyRingedSpace.toTopCat
 
-instance : CoeSort LocallyRingedSpace (Type*) :=
-  ⟨fun X : LocallyRingedSpace => (X.toTopCat : Type*)⟩
+instance : CoeSort LocallyRingedSpace (Type _) :=
+  ⟨fun X : LocallyRingedSpace => (X.toTopCat : Type _)⟩
 
 instance (x : X) : LocalRing (X.stalk x) :=
   X.localRing x
@@ -76,7 +76,7 @@ set_option linter.uppercaseLean3 false in
 /-- A morphism of locally ringed spaces is a morphism of ringed spaces
  such that the morphisms induced on stalks are local ring homomorphisms. -/
 @[ext]
-structure Hom (X Y : LocallyRingedSpace) : Type* where
+structure Hom (X Y : LocallyRingedSpace) : Type _ where
   /-- the underlying morphism between ringed spaces -/
   val : X.toSheafedSpace ⟶ Y.toSheafedSpace
   /-- the underlying morphism induces a local ring homomorphism on stalks -/
diff --git a/Mathlib/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean b/Mathlib/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean
@@ -127,7 +127,7 @@ noncomputable def coproductCofanIsColimit : IsColimit (coproductCofan F) where
 instance : HasCoproducts.{u} LocallyRingedSpace.{u} := fun _ =>
   ⟨fun F => ⟨⟨⟨_, coproductCofanIsColimit F⟩⟩⟩⟩
 
-noncomputable instance (J : Type*) :
+noncomputable instance (J : Type _) :
     PreservesColimitsOfShape (Discrete.{u} J) forgetToSheafedSpace.{u} :=
   ⟨fun {G} =>
     preservesColimitOfPreservesColimitCocone (coproductCofanIsColimit G)
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
@@ -188,7 +188,7 @@ end
 
 /-- The structure sheaf (valued in `Type`, not yet `CommRing`) is the subsheaf consisting of
 functions satisfying `isLocallyFraction`.-/
-def structureSheafInType : Sheaf (Type*) (ProjectiveSpectrum.top 𝒜) :=
+def structureSheafInType : Sheaf (Type _) (ProjectiveSpectrum.top 𝒜) :=
   subsheafToTypes (isLocallyFraction 𝒜)
 #align algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType
 
diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean
@@ -340,7 +340,7 @@ theorem sbtw_iff_mem_image_Ioo_and_ne [NoZeroSMulDivisors R V] {x y z : P} :
   rw [lineMap_apply, ← @vsub_ne_zero V, ← @vsub_ne_zero V _ _ _ _ z, vadd_vsub_assoc, vsub_self,
     vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z x, ← @neg_one_smul R, ← add_smul, ← sub_eq_add_neg]
   have : z -ᵥ x ≠ 0 := by simpa using hxz.symm
-  simp [smul_ne_zero, this, sub_eq_zero, ht.1.ne.symm, ht.2.ne]
+  simp [smul_ne_zero, this, sub_eq_zero, ht.1.ne.symm, ht.2.ne, hxz.symm]
 #align sbtw_iff_mem_image_Ioo_and_ne sbtw_iff_mem_image_Ioo_and_ne
 
 variable (R)
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -111,7 +111,7 @@ theorem PiLp.inner_apply {ι : Type*} [Fintype ι] {f : ι → Type*} [∀ i, No
 /-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
 space use `EuclideanSpace 𝕜 (Fin n)`. -/
 @[reducible, nolint unusedArguments]
-def EuclideanSpace (𝕜 : Type*) [IsROrC 𝕜] (n : Type*) [Fintype n] : Type* :=
+def EuclideanSpace (𝕜 : Type*) [IsROrC 𝕜] (n : Type*) [Fintype n] : Type _ :=
   PiLp 2 fun _ : n => 𝕜
 #align euclidean_space EuclideanSpace
 
diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -201,7 +201,7 @@ theorem LipschitzOnWith.extend_finite_dimension {α : Type*} [PseudoMetricSpace
     ∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s := by
   /- This result is already known for spaces `ι → ℝ`. We use a continuous linear equiv between
     `E'` and such a space to transfer the result to `E'`. -/
-  let ι : Type* := Basis.ofVectorSpaceIndex ℝ E'
+  let ι : Type _ := Basis.ofVectorSpaceIndex ℝ E'
   let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
   have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
   have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
@@ -569,8 +569,8 @@ theorem tangentMap_tangentBundle_pure (p : TangentBundle I M) :
     apply (LocalHomeomorph.open_target _).preimage I.continuous_invFun
     simp only [mfld_simps]
   have A : MDifferentiableAt I I.tangent (fun x => @TotalSpace.mk M E (TangentSpace I) x 0) x :=
-    haveI : Smooth I (I.prod 𝓘(𝕜, E)) (zeroSection E (TangentSpace I : M → Type*)) :=
-      Bundle.smooth_zeroSection 𝕜 (TangentSpace I : M → Type*)
+    haveI : Smooth I (I.prod 𝓘(𝕜, E)) (zeroSection E (TangentSpace I : M → Type _)) :=
+      Bundle.smooth_zeroSection 𝕜 (TangentSpace I : M → Type _)
     this.mdifferentiableAt
   have B :
     fderivWithin 𝕜 (fun x' : E => (x', (0 : E))) (Set.range I) (I ((chartAt H x) x)) v = (v, 0)
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
@@ -145,7 +145,7 @@ variable (M)
 `Bundle.TotalSpace` to be able to put a suitable topology on it. -/
 @[reducible] -- porting note: was nolint has_nonempty_instance
 def TangentBundle :=
-  Bundle.TotalSpace E (TangentSpace I : M → Type*)
+  Bundle.TotalSpace E (TangentSpace I : M → Type _)
 #align tangent_bundle TangentBundle
 
 local notation "TM" => TangentBundle I M
@@ -170,10 +170,10 @@ end
 instance : TopologicalSpace TM :=
   (tangentBundleCore I M).toTopologicalSpace
 
-instance TangentSpace.fiberBundle : FiberBundle E (TangentSpace I : M → Type*) :=
+instance TangentSpace.fiberBundle : FiberBundle E (TangentSpace I : M → Type _) :=
   (tangentBundleCore I M).fiberBundle
 
-instance TangentSpace.vectorBundle : VectorBundle 𝕜 E (TangentSpace I : M → Type*) :=
+instance TangentSpace.vectorBundle : VectorBundle 𝕜 E (TangentSpace I : M → Type _) :=
   (tangentBundleCore I M).vectorBundle
 
 namespace TangentBundle
@@ -307,13 +307,13 @@ instance tangentBundleCore.isSmooth : (tangentBundleCore I M).IsSmooth I := by
   rw [SmoothOn, contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas I i.2),
     contMDiffOn_iff_contDiffOn]
   refine' ((contDiffOn_fderiv_coord_change I i j).congr fun x hx => _).mono _
-  · rw [LocalEquiv.trans_source'] at hx 
+  · rw [LocalEquiv.trans_source'] at hx
     simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
   · exact (i.1.extend_image_source_inter j.1 I).subset
   · apply inter_subset_left
 #align tangent_bundle_core.is_smooth tangentBundleCore.isSmooth
 
-instance TangentBundle.smoothVectorBundle : SmoothVectorBundle E (TangentSpace I : M → Type*) I :=
+instance TangentBundle.smoothVectorBundle : SmoothVectorBundle E (TangentSpace I : M → Type _) I :=
   (tangentBundleCore I M).smoothVectorBundle _
 #align tangent_bundle.smooth_vector_bundle TangentBundle.smoothVectorBundle
 
diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@@ -80,7 +80,7 @@ def HasEigenvalue (f : End R M) (a : R) : Prop :=
 #align module.End.has_eigenvalue Module.End.HasEigenvalue
 
 /-- The eigenvalues of the endomorphism `f`, as a subtype of `R`. -/
-def Eigenvalues (f : End R M) : Type* :=
+def Eigenvalues (f : End R M) : Type _ :=
   { μ : R // f.HasEigenvalue μ }
 #align module.End.eigenvalues Module.End.Eigenvalues
 
diff --git a/Mathlib/MeasureTheory/Covering/LiminfLimsup.lean b/Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
@@ -76,7 +76,7 @@ theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux (p : ℕ → Prop) {s
   intros i
   set W := atTop.blimsup Y₁ p \ Z i
   by_contra contra
-  obtain ⟨d, hd, hd'⟩ : ∃ d, d ∈ W ∧ ∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
+  obtain ⟨d, hd, hd'⟩ : ∃ d, d ∈ W ∧ ∀ {ι : Type _} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
       Tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closedBall (w j) (2 * δ j)) →
         Tendsto (fun j => μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1) :=
     Measure.exists_mem_of_measure_ne_zero_of_ae contra
diff --git a/Mathlib/MeasureTheory/Function/AEEqFun.lean b/Mathlib/MeasureTheory/Function/AEEqFun.lean
@@ -98,7 +98,7 @@ variable (α)
 /-- The space of equivalence classes of almost everywhere strongly measurable functions, where two
     strongly measurable functions are equivalent if they agree almost everywhere, i.e.,
     they differ on a set of measure `0`.  -/
-def AEEqFun (μ : Measure α) : Type* :=
+def AEEqFun (μ : Measure α) : Type _ :=
   Quotient (μ.aeEqSetoid β)
 #align measure_theory.ae_eq_fun MeasureTheory.AEEqFun
 
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
@@ -107,7 +107,7 @@ variable {Ω : Type*} [MeasurableSpace Ω]
 
 /-- Finite measures are defined as the subtype of measures that have the property of being finite
 measures (i.e., their total mass is finite). -/
-def _root_.MeasureTheory.FiniteMeasure (Ω : Type*) [MeasurableSpace Ω] : Type* :=
+def _root_.MeasureTheory.FiniteMeasure (Ω : Type*) [MeasurableSpace Ω] : Type _ :=
   { μ : Measure Ω // IsFiniteMeasure μ }
 #align measure_theory.finite_measure MeasureTheory.FiniteMeasure
 
diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
@@ -382,8 +382,8 @@ theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionS
     Fubini. Along this coordinate (and when all the other coordinates are fixed), it acts like a
     translation, and therefore preserves Lebesgue. -/
   let p : ι → Prop := fun i => i ≠ t.i
-  let α : Type* := { x // p x }
-  let β : Type* := { x // ¬p x }
+  let α : Type _ := { x // p x }
+  let β : Type _ := { x // ¬p x }
   let g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun _ => t.c * a ⟨t.j, t.hij.symm⟩) + b
   let F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.1, g p.1 p.2)
   let e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => ℝ) p
diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
@@ -97,7 +97,7 @@ finite measure, this is implemented as the induced topology from the mapping
 
 /-- Probability measures are defined as the subtype of measures that have the property of being
 probability measures (i.e., their total mass is one). -/
-def ProbabilityMeasure (Ω : Type*) [MeasurableSpace Ω] : Type* :=
+def ProbabilityMeasure (Ω : Type*) [MeasurableSpace Ω] : Type _ :=
   { μ : Measure Ω // IsProbabilityMeasure μ }
 #align measure_theory.probability_measure MeasureTheory.ProbabilityMeasure
 
diff --git a/Mathlib/Order/Category/FrmCat.lean b/Mathlib/Order/Category/FrmCat.lean
@@ -34,7 +34,7 @@ def FrmCat :=
 
 namespace FrmCat
 
-instance : CoeSort FrmCat (Type*) :=
+instance : CoeSort FrmCat (Type _) :=
   Bundled.coeSort
 
 instance (X : FrmCat) : Frame X :=
@@ -54,7 +54,7 @@ instance : Inhabited FrmCat :=
 
 /-- An abbreviation of `FrameHom` that assumes `Frame` instead of the weaker `CompleteLattice`.
 Necessary for the category theory machinery. -/
-abbrev Hom (α β : Type*) [Frame α] [Frame β] : Type* :=
+abbrev Hom (α β : Type*) [Frame α] [Frame β] : Type _ :=
   FrameHom α β
 #align Frm.hom FrmCat.Hom
 
diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean
@@ -141,7 +141,7 @@ To view elements as a linear combination of the form `s • D s'`, use
 We also provide the notation `Ω[S⁄R]` for `KaehlerDifferential R S`.
 Note that the slash is `\textfractionsolidus`.
 -/
-def KaehlerDifferential : Type* :=
+def KaehlerDifferential : Type _ :=
   (KaehlerDifferential.ideal R S).Cotangent
 #align kaehler_differential KaehlerDifferential
 
diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean
@@ -20,7 +20,7 @@ open scoped TensorProduct
 
 open TensorProduct Algebra.TensorProduct
 
-local notation "surjective" => fun {X Y : Type*} [CommRing X] [CommRing Y] => fun f : X →+* Y =>
+local notation "surjective" => fun {X Y : Type _} [CommRing X] [CommRing Y] => fun f : X →+* Y =>
   Function.Surjective f
 
 theorem surjective_stableUnderComposition : StableUnderComposition surjective := by
diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean
@@ -62,8 +62,8 @@ theorem RespectsIso.cancel_right_isIso (hP : RespectsIso @P) {R S T : CommRingCa
     simp, hP.1 f (asIso g).commRingCatIsoToRingEquiv⟩
 #align ring_hom.respects_iso.cancel_right_is_iso RingHom.RespectsIso.cancel_right_isIso
 
-theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type*}
-    (R' S' : Type*) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R']
+theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type _}
+    (R' S' : Type _) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R']
     [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] :
     P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r) := by
   let e₁ : R' ≃+* Localization.Away r :=
@@ -105,7 +105,7 @@ def StableUnderComposition : Prop :=
 variable {P}
 
 theorem StableUnderComposition.respectsIso (hP : RingHom.StableUnderComposition @P)
-    (hP' : ∀ {R S : Type*} [CommRing R] [CommRing S] (e : R ≃+* S), P e.toRingHom) :
+    (hP' : ∀ {R S : Type _} [CommRing R] [CommRing S] (e : R ≃+* S), P e.toRingHom) :
     RingHom.RespectsIso @P := by
   constructor
   · introv H
diff --git a/Mathlib/RingTheory/WittVector/Isocrystal.lean b/Mathlib/RingTheory/WittVector/Isocrystal.lean
@@ -169,7 +169,7 @@ of slope `m : ℤ`.
 @[nolint unusedArguments]
 -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5171):
 -- removed @[nolint has_nonempty_instance]
-def StandardOneDimIsocrystal (_m : ℤ) : Type* :=
+def StandardOneDimIsocrystal (_m : ℤ) : Type _ :=
   K(p, k)
 #align witt_vector.standard_one_dim_isocrystal WittVector.StandardOneDimIsocrystal
 
diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean
@@ -256,7 +256,7 @@ def limitCone {J : Type u} [SmallCategory J] (F : J ⥤ Profinite.{u}) : Limits.
   pt :=
     { toCompHaus := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).pt
       IsTotallyDisconnected := by
-        change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type*)
+        change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
         exact Subtype.totallyDisconnectedSpace }
   π :=
   { app := (CompHaus.limitCone.{u, u} (F ⋙ profiniteToCompHaus)).π.app
