chore: tidy various files

Mathlib/Algebra/AlgebraicCard.lean

@@ -81,10 +81,10 @@ protected theorem countable : Set.Countable { x : A | IsAlgebraic R x } := by
 #align algebraic.countable Algebraic.countable
 
 @[simp]
-theorem cardinal_mk_of_countble_of_charZero [CharZero A] [IsDomain R] :
+theorem cardinal_mk_of_countable_of_charZero [CharZero A] [IsDomain R] :
     (#{ x : A // IsAlgebraic R x }) = ℵ₀ :=
   (Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinal_mk_of_charZero R A)
-#align algebraic.cardinal_mk_of_countble_of_char_zero Algebraic.cardinal_mk_of_countble_of_charZero
+#align algebraic.cardinal_mk_of_countble_of_char_zero Algebraic.cardinal_mk_of_countable_of_charZero
 
 end lift
 

Mathlib/Algebra/Category/ModuleCat/Limits.lean

@@ -50,7 +50,7 @@ instance moduleObj (F : J ⥤ ModuleCatMax.{v, w, u} R) (j) :
   infer_instance
 #align Module.module_obj ModuleCat.moduleObj
 
-/-- The flat sections of a functor into `Module R` form a submodule of all sections.
+/-- The flat sections of a functor into `ModuleCat R` form a submodule of all sections.
 -/
 def sectionsSubmodule (F : J ⥤ ModuleCatMax.{v, w, u} R) : Submodule R (∀ j, F.obj j) :=
   { AddGroupCat.sectionsAddSubgroup.{v, w}
@@ -91,10 +91,10 @@ def limitπLinearMap (F : J ⥤ ModuleCatMax.{v, w, u} R) (j) :
 
 namespace HasLimits
 
--- The next two definitions are used in the construction of `HasLimits (Module R)`.
+-- The next two definitions are used in the construction of `HasLimits (ModuleCat R)`.
 -- After that, the limits should be constructed using the generic limits API,
 -- e.g. `limit F`, `limit.cone F`, and `limit.isLimit F`.
-/-- Construction of a limit cone in `Module R`.
+/-- Construction of a limit cone in `ModuleCat R`.
 (Internal use only; use the limits API.)
 -/
 def limitCone (F : J ⥤ ModuleCatMax.{v, w, u} R) : Cone F where
@@ -105,7 +105,7 @@ def limitCone (F : J ⥤ ModuleCatMax.{v, w, u} R) : Cone F where
         LinearMap.coe_injective ((Types.limitCone (F ⋙ forget _)).π.naturality f) }
 #align Module.has_limits.limit_cone ModuleCat.HasLimits.limitCone
 
-/-- Witness that the limit cone in `Module R` is a limit cone.
+/-- Witness that the limit cone in `ModuleCat R` is a limit cone.
 (Internal use only; use the limits API.)
 -/
 def limitConeIsLimit (F : J ⥤ ModuleCatMax.{v, w, u} R) : IsLimit (limitCone.{v, w} F) := by

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -229,9 +229,8 @@ alias hasDerivAt_iff_hasFDerivAt ↔ HasDerivAt.hasFDerivAt _
 theorem derivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
     derivWithin f s x = 0 := by
   unfold derivWithin
-  rw [fderivWithin_zero_of_not_differentiableWithinAt]
+  rw [fderivWithin_zero_of_not_differentiableWithinAt h]
   simp
-  assumption
 #align deriv_within_zero_of_not_differentiable_within_at derivWithin_zero_of_not_differentiableWithinAt
 
 theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithin f s x ≠ 0) :
@@ -241,9 +240,8 @@ theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithin f s x ≠
 
 theorem deriv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : deriv f x = 0 := by
   unfold deriv
-  rw [fderiv_zero_of_not_differentiableAt]
+  rw [fderiv_zero_of_not_differentiableAt h]
   simp
-  assumption
 #align deriv_zero_of_not_differentiable_at deriv_zero_of_not_differentiableAt
 
 theorem differentiableAt_of_deriv_ne_zero (h : deriv f x ≠ 0) : DifferentiableAt 𝕜 f x :=
@@ -731,4 +729,3 @@ protected theorem HasDerivAt.continuousOn {f f' : 𝕜 → F} (hderiv : ∀ x 
 #align has_deriv_at.continuous_on HasDerivAt.continuousOn
 
 end Continuous
-

Mathlib/Analysis/Complex/UnitDisc/Basic.lean

@@ -19,9 +19,7 @@ introduce some basic operations on this disc.
 -/
 
 
-open Set Function Metric
-
-open BigOperators
+open Set Function Metric BigOperators
 
 noncomputable section
 
@@ -34,15 +32,15 @@ def UnitDisc : Type :=
   ball (0 : ℂ) 1 deriving TopologicalSpace
 #align complex.unit_disc Complex.UnitDisc
 
-instance : CommSemigroup UnitDisc := by unfold UnitDisc; infer_instance
-instance : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance
-instance : Coe UnitDisc ℂ := ⟨Subtype.val⟩
-
 scoped[UnitDisc] notation "𝔻" => Complex.UnitDisc
 open UnitDisc
 
 namespace UnitDisc
 
+instance instCommSemigroup : CommSemigroup UnitDisc := by unfold UnitDisc; infer_instance
+instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance
+instance instCoe : Coe UnitDisc ℂ := ⟨Subtype.val⟩
+
 theorem coe_injective : Injective ((↑) : 𝔻 → ℂ) :=
   Subtype.coe_injective
 #align complex.unit_disc.coe_injective Complex.UnitDisc.coe_injective
@@ -101,7 +99,7 @@ theorem mk_neg (z : ℂ) (hz : abs (-z) < 1) : mk (-z) hz = -mk z (abs.map_neg z
 #align complex.unit_disc.mk_neg Complex.UnitDisc.mk_neg
 
 instance : SemigroupWithZero 𝔻 :=
-  { instCommSemigroupUnitDisc with
+  { instCommSemigroup with
     zero := mk 0 <| (map_zero _).trans_lt one_pos
     zero_mul := fun _ => coe_injective <| MulZeroClass.zero_mul _
     mul_zero := fun _ => coe_injective <| MulZeroClass.mul_zero _ }
@@ -131,13 +129,13 @@ instance isScalarTower_circle : IsScalarTower circle 𝔻 𝔻 :=
   isScalarTower_sphere_ball_ball
 #align complex.unit_disc.is_scalar_tower_circle Complex.UnitDisc.isScalarTower_circle
 
-instance sMulCommClass_circle : SMulCommClass circle 𝔻 𝔻 :=
-  sMulCommClass_sphere_ball_ball
-#align complex.unit_disc.smul_comm_class_circle Complex.UnitDisc.sMulCommClass_circle
+instance instSMulCommClass_circle : SMulCommClass circle 𝔻 𝔻 :=
+  instSMulCommClass_sphere_ball_ball
+#align complex.unit_disc.smul_comm_class_circle Complex.UnitDisc.instSMulCommClass_circle
 
-instance sMulCommClass_circle' : SMulCommClass 𝔻 circle 𝔻 :=
+instance instSMulCommClass_circle' : SMulCommClass 𝔻 circle 𝔻 :=
   SMulCommClass.symm _ _ _
-#align complex.unit_disc.smul_comm_class_circle' Complex.UnitDisc.sMulCommClass_circle'
+#align complex.unit_disc.smul_comm_class_circle' Complex.UnitDisc.instSMulCommClass_circle'
 
 @[simp, norm_cast]
 theorem coe_smul_circle (z : circle) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
@@ -157,21 +155,21 @@ instance isScalarTower_closedBall : IsScalarTower (closedBall (0 : ℂ) 1) 𝔻
   isScalarTower_closedBall_ball_ball
 #align complex.unit_disc.is_scalar_tower_closed_ball Complex.UnitDisc.isScalarTower_closedBall
 
-instance sMulCommClass_closedBall : SMulCommClass (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
+instance instSMulCommClass_closedBall : SMulCommClass (closedBall (0 : ℂ) 1) 𝔻 𝔻 :=
   ⟨fun _ _ _ => Subtype.ext <| mul_left_comm _ _ _⟩
-#align complex.unit_disc.smul_comm_class_closed_ball Complex.UnitDisc.sMulCommClass_closedBall
+#align complex.unit_disc.smul_comm_class_closed_ball Complex.UnitDisc.instSMulCommClass_closedBall
 
-instance sMulCommClass_closed_ball' : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
+instance instSMulCommClass_closedBall' : SMulCommClass 𝔻 (closedBall (0 : ℂ) 1) 𝔻 :=
   SMulCommClass.symm _ _ _
-#align complex.unit_disc.smul_comm_class_closed_ball' Complex.UnitDisc.sMulCommClass_closed_ball'
+#align complex.unit_disc.smul_comm_class_closed_ball' Complex.UnitDisc.instSMulCommClass_closedBall'
 
-instance sMulCommClass_circle_closedBall : SMulCommClass circle (closedBall (0 : ℂ) 1) 𝔻 :=
-  sMulCommClass_sphere_closedBall_ball
-#align complex.unit_disc.smul_comm_class_circle_closed_ball Complex.UnitDisc.sMulCommClass_circle_closedBall
+instance instSMulCommClass_circle_closedBall : SMulCommClass circle (closedBall (0 : ℂ) 1) 𝔻 :=
+  instSMulCommClass_sphere_closedBall_ball
+#align complex.unit_disc.smul_comm_class_circle_closed_ball Complex.UnitDisc.instSMulCommClass_circle_closedBall
 
-instance sMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : ℂ) 1) circle 𝔻 :=
+instance instSMulCommClass_closedBall_circle : SMulCommClass (closedBall (0 : ℂ) 1) circle 𝔻 :=
   SMulCommClass.symm _ _ _
-#align complex.unit_disc.smul_comm_class_closed_ball_circle Complex.UnitDisc.sMulCommClass_closedBall_circle
+#align complex.unit_disc.smul_comm_class_closed_ball_circle Complex.UnitDisc.instSMulCommClass_closedBall_circle
 
 @[simp, norm_cast]
 theorem coe_smul_closedBall (z : closedBall (0 : ℂ) 1) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=

Mathlib/Analysis/NormedSpace/BallAction.lean

@@ -157,45 +157,45 @@ section SMulCommClass
 
 variable [SMulCommClass 𝕜 𝕜' E]
 
-instance sMulCommClass_closedBall_closedBall_closedBall :
+instance instSMulCommClass_closedBall_closedBall_closedBall :
     SMulCommClass (closedBall (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (closedBall (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_closed_ball_closed_ball_closed_ball sMulCommClass_closedBall_closedBall_closedBall
+#align smul_comm_class_closed_ball_closed_ball_closed_ball instSMulCommClass_closedBall_closedBall_closedBall
 
-instance sMulCommClass_closedBall_closedBall_ball :
+instance instSMulCommClass_closedBall_closedBall_ball :
     SMulCommClass (closedBall (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (ball (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_closed_ball_closed_ball_ball sMulCommClass_closedBall_closedBall_ball
+#align smul_comm_class_closed_ball_closed_ball_ball instSMulCommClass_closedBall_closedBall_ball
 
-instance sMulCommClass_sphere_closedBall_closedBall :
+instance instSMulCommClass_sphere_closedBall_closedBall :
     SMulCommClass (sphere (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (closedBall (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_sphere_closed_ball_closed_ball sMulCommClass_sphere_closedBall_closedBall
+#align smul_comm_class_sphere_closed_ball_closed_ball instSMulCommClass_sphere_closedBall_closedBall
 
-instance sMulCommClass_sphere_closedBall_ball :
+instance instSMulCommClass_sphere_closedBall_ball :
     SMulCommClass (sphere (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (ball (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_sphere_closed_ball_ball sMulCommClass_sphere_closedBall_ball
+#align smul_comm_class_sphere_closed_ball_ball instSMulCommClass_sphere_closedBall_ball
 
-instance sMulCommClass_sphere_ball_ball [NormedAlgebra 𝕜 𝕜'] :
+instance instSMulCommClass_sphere_ball_ball [NormedAlgebra 𝕜 𝕜'] :
     SMulCommClass (sphere (0 : 𝕜) 1) (ball (0 : 𝕜') 1) (ball (0 : 𝕜') 1) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩
-#align smul_comm_class_sphere_ball_ball sMulCommClass_sphere_ball_ball
+#align smul_comm_class_sphere_ball_ball instSMulCommClass_sphere_ball_ball
 
-instance sMulCommClass_sphere_sphere_closedBall :
+instance instSMulCommClass_sphere_sphere_closedBall :
     SMulCommClass (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (closedBall (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_sphere_sphere_closed_ball sMulCommClass_sphere_sphere_closedBall
+#align smul_comm_class_sphere_sphere_closed_ball instSMulCommClass_sphere_sphere_closedBall
 
-instance sMulCommClass_sphere_sphere_ball :
+instance instSMulCommClass_sphere_sphere_ball :
     SMulCommClass (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (ball (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_sphere_sphere_ball sMulCommClass_sphere_sphere_ball
+#align smul_comm_class_sphere_sphere_ball instSMulCommClass_sphere_sphere_ball
 
-instance sMulCommClass_sphere_sphere_sphere :
+instance instSMulCommClass_sphere_sphere_sphere :
     SMulCommClass (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (sphere (0 : E) r) :=
   ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
-#align smul_comm_class_sphere_sphere_sphere sMulCommClass_sphere_sphere_sphere
+#align smul_comm_class_sphere_sphere_sphere instSMulCommClass_sphere_sphere_sphere
 
 end SMulCommClass
 

Mathlib/CategoryTheory/Bicategory/Coherence.lean

@@ -48,8 +48,6 @@ namespace CategoryTheory
 
 open Bicategory Category
 
-open Bicategory
-
 universe v u
 
 namespace FreeBicategory
@@ -155,47 +153,47 @@ theorem normalizeAux_congr {a b c : B} (p : Path a b) {f g : Hom b c} (η : f 
   rcases η with ⟨η'⟩
   apply @congr_fun _ _ fun p => normalizeAux p f
   clear p η
-  induction η'
-  case vcomp => apply Eq.trans <;> assumption
-  -- p ≠ nil required! See the docstring of `normalizeAux`.
-  case whisker_left _ _ _ _ _ _ _ ih => funext; apply congr_fun ih
-  case whisker_right _ _ _ _ _ _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
-  all_goals funext; rfl
+  induction η' with
+  | vcomp _ _ _ _ => apply Eq.trans <;> assumption
+  | whisker_left _ _ ih => funext; apply congr_fun ih
+  | whisker_right _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih _) rfl
+  | _ => funext; rfl
 #align category_theory.free_bicategory.normalize_aux_congr CategoryTheory.FreeBicategory.normalizeAux_congr
 
 /-- The 2-isomorphism `normalizeIso p f` is natural in `f`. -/
 theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
     (preinclusion B).map ⟨p⟩ ◁ η ≫ (normalizeIso p g).hom =
       (normalizeIso p f).hom ≫
         (preinclusion B).map₂ (eqToHom (Discrete.ext _ _ (normalizeAux_congr p η))) := by
-  rcases η with ⟨η'⟩; clear η; induction η'
-  case id => simp
-  case vcomp _ _ _ _ _ η θ ihf ihg =>
+  rcases η with ⟨η'⟩; clear η;
+  induction η' with
+  | id => simp
+  | vcomp η θ ihf ihg =>
     simp only [mk_vcomp, Bicategory.whiskerLeft_comp]
     slice_lhs 2 3 => rw [ihg]
     slice_lhs 1 2 => rw [ihf]
     simp
   -- p ≠ nil required! See the docstring of `normalizeAux`.
-  case whisker_left _ _ _ _ _ _ _ ih =>
+  | whisker_left _ _ ih =>
     dsimp
     rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
     simp
-  case whisker_right _ _ _ _ _ h η' ih =>
+  | whisker_right h η' ih =>
     dsimp
     rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
     have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
     dsimp at this; simp [this]
-  all_goals simp
+  | _ => simp
 #align category_theory.free_bicategory.normalize_naturality CategoryTheory.FreeBicategory.normalize_naturality
 
 -- Porting note: the left-hand side is not in simp-normal form.
 -- @[simp]
 theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
     normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g) := by
-  induction g generalizing a
-  case id => rfl
-  case of => rfl
-  case comp _ _ _ g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
+  induction g generalizing a with
+  | id => rfl
+  | of => rfl
+  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
 #align category_theory.free_bicategory.normalize_aux_nil_comp CategoryTheory.FreeBicategory.normalizeAux_nil_comp
 
 /-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/

Mathlib/CategoryTheory/Limits/Fubini.lean

@@ -339,8 +339,7 @@ theorem limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {j} {k} :
   simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_inv_π,
     Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
   erw [NatTrans.id_app]
-  -- Why can't `simp` do this`?
-  dsimp;
+  -- Porting note: `simp` can do this in lean 4.
   simp
 #align category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_inv_π_π CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π
 

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -22,9 +22,7 @@ are irreducible, and uniquely determined by their defining property.
 -/
 
 
-open Classical Polynomial
-
-open Polynomial Set Function minpoly
+open Classical Polynomial Set Function minpoly
 
 namespace minpoly
 
@@ -37,8 +35,8 @@ section Ring
 variable [Ring B] [Algebra A B] (x : B)
 
 /-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
-degree of the minimal polynomial of `x`. See also `gcd_domain_degree_le_of_ne_zero` which relaxes
-the assumptions on `A` in exchange for stronger assumptions on `B`. -/
+degree of the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.degree_le_of_ne_zero`
+which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`. -/
 theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x p = 0) :
     degree (minpoly A x) ≤ degree p :=
   calc
@@ -53,8 +51,8 @@ theorem ne_zero_of_finite_field_extension (e : B) [FiniteDimensional A B] : minp
 
 /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
 if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
-is equal to the minimal polynomial of `x`. See also `minpoly.gcd_unique` which relaxes the
-assumptions on `A` in exchange for stronger assumptions on `B`. -/
+is equal to the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.Minpoly.unique`
+which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`. -/
 theorem unique {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0)
     (pmin : ∀ q : A[X], q.Monic → Polynomial.aeval x q = 0 → degree p ≤ degree q) :
     p = minpoly A x := by
@@ -69,8 +67,8 @@ theorem unique {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0)
 #align minpoly.unique minpoly.unique
 
 /-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
-See also `minpoly.gcd_domain_dvd` which relaxes the assumptions on `A` in exchange for stronger
-assumptions on `B`. -/
+See also `minpoly.isIntegrallyClosed_dvd` which relaxes the assumptions on `A` in exchange for
+stronger assumptions on `B`. -/
 theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p := by
   by_cases hp0 : p = 0
   · simp only [hp0, dvd_zero]
@@ -92,14 +90,14 @@ theorem dvd_map_of_isScalarTower (A K : Type _) {R : Type _} [CommRing A] [Field
   rw [aeval_map_algebraMap, minpoly.aeval]
 #align minpoly.dvd_map_of_is_scalar_tower minpoly.dvd_map_of_isScalarTower
 
-theorem dvd_map_of_is_scalar_tower' (R : Type _) {S : Type _} (K L : Type _) [CommRing R]
+theorem dvd_map_of_isScalarTower' (R : Type _) {S : Type _} (K L : Type _) [CommRing R]
     [CommRing S] [Field K] [CommRing L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L]
     [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) :
     minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (minpoly R s) := by
   apply minpoly.dvd K (algebraMap S L s)
   rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
   rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-#align minpoly.dvd_map_of_is_scalar_tower' minpoly.dvd_map_of_is_scalar_tower'
+#align minpoly.dvd_map_of_is_scalar_tower' minpoly.dvd_map_of_isScalarTower'
 
 /-- If `y` is a conjugate of `x` over a field `K`, then it is a conjugate over a subring `R`. -/
 theorem aeval_of_isScalarTower (R : Type _) {K T U : Type _} [CommRing R] [Field K] [CommRing T]
@@ -176,10 +174,10 @@ noncomputable def Fintype.subtypeProd {E : Type _} {X : Set E} (hX : X.Finite) {
 variable (F E K : Type _) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K]
   [FiniteDimensional F E]
 
--- Marked as `noncomputable!` since this definition takes multiple seconds to compile,
--- and isn't very computable in practice (since neither `finrank` nor `finBasis` are).
+-- Porting note: removed `noncomputable!` since it seems not to be slow in lean 4,
+-- though it isn't very computable in practice (since neither `finrank` nor `finBasis` are).
 /-- Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x -/
-noncomputable def rootsOfMinPolyPiType (φ : E →ₐ[F] K)
+def rootsOfMinPolyPiType (φ : E →ₐ[F] K)
     (x : range (FiniteDimensional.finBasis F E : _ → E)) :
     { l : K // l ∈ (((minpoly F x.1).map (algebraMap F K)).roots : Multiset K) } :=
   ⟨φ x, by