chore: tidy various files (#3110)

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -132,8 +132,8 @@ instance RestrictScalars.opModule [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (Res
 #align restrict_scalars.op_module RestrictScalars.opModule
 
 instance RestrictScalars.isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] :
-    IsCentralScalar R (RestrictScalars R S M)
-    where op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) : _)
+    IsCentralScalar R (RestrictScalars R S M) where
+  op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) : _)
 #align restrict_scalars.is_central_scalar RestrictScalars.isCentralScalar
 
 /-- The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
@@ -150,18 +150,18 @@ end
 
 variable [AddCommMonoid M]
 
-/-- `RestrictScalars.add_equiv` is the additive equivalence with the original module. -/
+/-- `RestrictScalars.addEquiv` is the additive equivalence with the original module. -/
 def RestrictScalars.addEquiv : RestrictScalars R S M ≃+ M :=
   AddEquiv.refl M
 #align restrict_scalars.add_equiv RestrictScalars.addEquiv
 
 variable [CommSemiring R] [Semiring S] [Algebra R S] [Module S M]
 
-theorem restrictScalars.smul_def (c : R) (x : RestrictScalars R S M) :
+theorem RestrictScalars.smul_def (c : R) (x : RestrictScalars R S M) :
     c • x = (RestrictScalars.addEquiv R S M).symm
       (algebraMap R S c • RestrictScalars.addEquiv R S M x) :=
   rfl
-#align restrict_scalars.smul_def restrictScalars.smul_def
+#align restrict_scalars.smul_def RestrictScalars.smul_def
 
 @[simp]
 theorem RestrictScalars.addEquiv_map_smul (c : R) (x : RestrictScalars R S M) :

Mathlib/Algebra/FreeAlgebra.lean

@@ -33,7 +33,7 @@ Given a commutative semiring `R`, and a type `X`, we construct the free unital,
 3. `hom_ext` is a variant of `lift_unique` in the form of an extensionality theorem.
 4. `lift_comp_ι` is a combination of `ι_comp_lift` and `lift_unique`. It states that the lift
   of the composition of an algebra morphism with `ι` is the algebra morphism itself.
-5. `equiv_monoid_algebra_free_monoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)`
+5. `equivMonoidAlgebraFreeMonoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)`
 6. An inductive principle `induction`.
 
 ## Implementation details
@@ -162,8 +162,7 @@ namespace FreeAlgebra
 attribute [local instance] Pre.hasCoeGenerator Pre.hasCoeSemiring Pre.hasMul Pre.hasAdd
   Pre.hasZero Pre.hasOne Pre.hasSmul
 
-instance : Semiring (FreeAlgebra R X)
-    where
+instance : Semiring (FreeAlgebra R X) where
   add := Quot.map₂ (· + ·) (fun _ _ _ ↦ Rel.add_compat_right) fun _ _ _ ↦ Rel.add_compat_left
   add_assoc := by
     rintro ⟨⟩ ⟨⟩ ⟨⟩
@@ -206,11 +205,10 @@ instance : Semiring (FreeAlgebra R X)
 instance : Inhabited (FreeAlgebra R X) :=
   ⟨0⟩
 
-instance : SMul R (FreeAlgebra R X)
-    where smul r := Quot.map ((· * ·) ↑r) fun _ _ ↦ Rel.mul_compat_right
+instance : SMul R (FreeAlgebra R X) where
+  smul r := Quot.map ((· * ·) ↑r) fun _ _ ↦ Rel.mul_compat_right
 
-instance : Algebra R (FreeAlgebra R X)
-    where
+instance : Algebra R (FreeAlgebra R X) where
   toFun r := Quot.mk _ r
   map_one' := rfl
   map_mul' _ _ := Quot.sound Rel.mul_scalar
@@ -238,8 +236,7 @@ theorem quot_mk_eq_ι (m : X) : Quot.mk (FreeAlgebra.Rel R X) m = ι R m := by r
 variable {A : Type _} [Semiring A] [Algebra R A]
 
 /-- Internal definition used to define `lift` -/
-private def liftAux (f : X → A) : FreeAlgebra R X →ₐ[R] A
-    where
+private def liftAux (f : X → A) : FreeAlgebra R X →ₐ[R] A where
   toFun a :=
     Quot.liftOn a (liftFun _ _ f) fun a b h ↦
       by

Mathlib/Analysis/NormedSpace/MStructure.lean

@@ -48,7 +48,7 @@ The approach to showing that the L-projections form a Boolean algebra is inspire
 `MeasureTheory.MeasurableSpace`.
 
 Instead of using `P : X →L[𝕜] X` to represent projections, we use an arbitrary ring `M` with a
-faithful action on `X`. `continuous_linear_map.apply_module` can be used to recover the `X →L[𝕜] X`
+faithful action on `X`. `ContinuousLinearMap.apply_module` can be used to recover the `X →L[𝕜] X`
 special case.
 
 ## References
@@ -162,14 +162,12 @@ theorem mul [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLp
   refine' ⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, _⟩
   intro x
   refine' le_antisymm _ _
-  ·
-    calc
+  · calc
       ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel'_right ((P * Q) • x) x]
       _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
       _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
 
-  ·
-    calc
+  · calc
       ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
         rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
       _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
@@ -188,15 +186,15 @@ theorem join [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsL
 
 --porting note: Advice is to explicitly name instances
 -- https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#some-common-fixes
-instance IsLprojection.Subtype.HasCompl : HasCompl { f : M // IsLprojection X f } :=
+instance Subtype.hasCompl : HasCompl { f : M // IsLprojection X f } :=
   ⟨fun P => ⟨1 - P, P.prop.Lcomplement⟩⟩
 
 @[simp]
 theorem coe_compl (P : { P : M // IsLprojection X P }) : ↑(Pᶜ) = (1 : M) - ↑P :=
   rfl
 #align is_Lprojection.coe_compl IsLprojection.coe_compl
 
-instance IsLprojection.Subtype.Inf [FaithfulSMul M X] : Inf { P : M // IsLprojection X P } :=
+instance Subtype.inf [FaithfulSMul M X] : Inf { P : M // IsLprojection X P } :=
   ⟨fun P Q => ⟨P * Q, P.prop.mul Q.prop⟩⟩
 
 @[simp]
@@ -205,7 +203,7 @@ theorem coe_inf [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) :
   rfl
 #align is_Lprojection.coe_inf IsLprojection.coe_inf
 
-instance IsLprojection.Subtype.Sup [FaithfulSMul M X] : Sup { P : M // IsLprojection X P } :=
+instance Subtype.sup [FaithfulSMul M X] : Sup { P : M // IsLprojection X P } :=
   ⟨fun P Q => ⟨P + Q - P * Q, P.prop.join Q.prop⟩⟩
 
 @[simp]
@@ -214,7 +212,7 @@ theorem coe_sup [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) :
   rfl
 #align is_Lprojection.coe_sup IsLprojection.coe_sup
 
-instance IsLprojection.Subtype.SDiff [FaithfulSMul M X] : SDiff { P : M // IsLprojection X P } :=
+instance Subtype.sdiff [FaithfulSMul M X] : SDiff { P : M // IsLprojection X P } :=
   ⟨fun P Q => ⟨P * (1 - Q), P.prop.mul Q.prop.Lcomplement⟩⟩
 
 @[simp]
@@ -223,7 +221,7 @@ theorem coe_sdiff [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) :
   rfl
 #align is_Lprojection.coe_sdiff IsLprojection.coe_sdiff
 
-instance IsLprojection.Subtype.PartialOrder [FaithfulSMul M X] :
+instance Subtype.partialOrder [FaithfulSMul M X] :
     PartialOrder { P : M // IsLprojection X P } where
   le P Q := (↑P : M) = ↑(P ⊓ Q)
   le_refl P := by simpa only [coe_inf, ← sq] using P.prop.proj.eq.symm
@@ -237,7 +235,7 @@ theorem le_def [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) :
   Iff.rfl
 #align is_Lprojection.le_def IsLprojection.le_def
 
-instance IsLprojection.Subtype.Zero : Zero { P : M // IsLprojection X P } :=
+instance Subtype.zero : Zero { P : M // IsLprojection X P } :=
   ⟨⟨0, ⟨by rw [IsIdempotentElem, MulZeroClass.zero_mul], fun x => by
         simp only [zero_smul, norm_zero, sub_zero, one_smul, zero_add]⟩⟩⟩
 
@@ -246,15 +244,15 @@ theorem coe_zero : ↑(0 : { P : M // IsLprojection X P }) = (0 : M) :=
   rfl
 #align is_Lprojection.coe_zero IsLprojection.coe_zero
 
-instance IsLprojection.Subtype.One : One { P : M // IsLprojection X P } :=
+instance Subtype.one : One { P : M // IsLprojection X P } :=
   ⟨⟨1, sub_zero (1 : M) ▸ (0 : { P : M // IsLprojection X P }).prop.Lcomplement⟩⟩
 
 @[simp]
 theorem coe_one : ↑(1 : { P : M // IsLprojection X P }) = (1 : M) :=
   rfl
 #align is_Lprojection.coe_one IsLprojection.coe_one
 
-instance IsLprojection.Subtype.BoundedOrder [FaithfulSMul M X] :
+instance Subtype.boundedOrder [FaithfulSMul M X] :
     BoundedOrder { P : M // IsLprojection X P } where
   top := 1
   le_top P := (mul_one (P : M)).symm
@@ -299,32 +297,29 @@ theorem distrib_lattice_lemma [FaithfulSMul M X] {P Q R : { P : M // IsLprojecti
 -- (deterministic) timeout at 'whnf', maximum number of heartbeats (800000) has been reached"
 -- My workaround is to show instance Lattice first
 instance [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P } where
-  le_sup_left := fun P Q => by
+  le_sup_left P Q := by
     rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
       sub_self, add_zero]
-  le_sup_right := fun P Q => by
+  le_sup_right P Q := by
     rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, (P.prop.commute Q.prop).eq,
       ← mul_assoc, Q.prop.proj.eq, add_sub_cancel'_right]
-  sup_le := fun P Q R =>
-    by
+  sup_le P Q R := by
     rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_sup, coe_inf, coe_sup, ← add_sub, add_mul,
       sub_mul, mul_assoc]
     intro h₁ h₂
     rw [← h₂, ← h₁]
-  inf_le_left := fun P Q => by
+  inf_le_left P Q := by
     rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, (Q.prop.commute P.prop).eq, ← mul_assoc,
       P.prop.proj.eq]
-  inf_le_right := fun P Q => by rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
-  le_inf := fun P Q R =>
-    by
+  inf_le_right P Q := by rw [le_def, coe_inf, coe_inf, coe_inf, mul_assoc, Q.prop.proj.eq]
+  le_inf P Q R := by
     rw [le_def, le_def, le_def, coe_inf, coe_inf, coe_inf, coe_inf, ← mul_assoc]
     intro h₁ h₂
     rw [← h₁, ← h₂]
 
-instance IsLprojection.Subtype.DistribLattice [FaithfulSMul M X] :
+instance Subtype.distribLattice [FaithfulSMul M X] :
     DistribLattice { P : M // IsLprojection X P } where
-  le_sup_inf := fun P Q R =>
-    by
+  le_sup_inf P Q R := by
     have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑(Pᶜ) := by
       rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
         mul_add, ((Pᶜ).prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q: M),
@@ -337,19 +332,19 @@ instance IsLprojection.Subtype.DistribLattice [FaithfulSMul M X] :
         distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
     rw [le_def, e₁, coe_inf, e₂]
 
-instance IsLprojection.Subtype.BooleanAlgebra [FaithfulSMul M X] :
+instance Subtype.BooleanAlgebra [FaithfulSMul M X] :
     BooleanAlgebra { P : M // IsLprojection X P } :=
 --porting note: use explicitly specified instance names
-  { IsLprojection.Subtype.HasCompl,
-    IsLprojection.Subtype.SDiff,
-    IsLprojection.Subtype.BoundedOrder with
+  { IsLprojection.Subtype.hasCompl,
+    IsLprojection.Subtype.sdiff,
+    IsLprojection.Subtype.boundedOrder with
     inf_compl_le_bot := fun P =>
       (Subtype.ext (by rw [coe_inf, coe_compl, coe_bot, ← coe_compl, mul_compl_self])).le
     top_le_sup_compl := fun P =>
       (Subtype.ext
-          (by
-            rw [coe_top, coe_sup, coe_compl, add_sub_cancel'_right, ← coe_compl, mul_compl_self,
-              sub_zero])).le
+        (by
+          rw [coe_top, coe_sup, coe_compl, add_sub_cancel'_right, ← coe_compl, mul_compl_self,
+            sub_zero])).le
     sdiff_eq := fun P Q => Subtype.ext <| by rw [coe_sdiff, ← coe_compl, coe_inf] }
 
 end IsLprojection

Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

@@ -39,8 +39,6 @@ open MonoidalCategory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Type u₂} [Category.{v₂} D]
   [MonoidalCategory.{v₂} D]
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /-- A monoidal natural transformation is a natural transformation between (lax) monoidal functors
 additionally satisfying:
 `F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y`
@@ -82,8 +80,7 @@ def vcomp {F G H : LaxMonoidalFunctor C D} (α : MonoidalNatTrans F G) (β : Mon
   { NatTrans.vcomp α.toNatTrans β.toNatTrans with }
 #align category_theory.monoidal_nat_trans.vcomp CategoryTheory.MonoidalNatTrans.vcomp
 
-instance categoryLaxMonoidalFunctor : Category (LaxMonoidalFunctor C D)
-    where
+instance categoryLaxMonoidalFunctor : Category (LaxMonoidalFunctor C D) where
   Hom := MonoidalNatTrans
   id := id
   comp α β := vcomp α β
@@ -111,8 +108,7 @@ variable {E : Type u₃} [Category.{v₃} E] [MonoidalCategory.{v₃} E]
 @[simps]
 def hcomp {F G : LaxMonoidalFunctor C D} {H K : LaxMonoidalFunctor D E} (α : MonoidalNatTrans F G)
     (β : MonoidalNatTrans H K) : MonoidalNatTrans (F ⊗⋙ H) (G ⊗⋙ K) :=
-  { NatTrans.hcomp α.toNatTrans
-      β.toNatTrans with
+  { NatTrans.hcomp α.toNatTrans β.toNatTrans with
     unit := by
       dsimp; simp
       conv_lhs => rw [← K.toFunctor.map_comp, α.unit]
@@ -145,12 +141,11 @@ and the monoidal naturality in the forward direction. -/
 def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X)
     (naturality' : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f)
     (unit' : F.ε ≫ (app (𝟙_ C)).hom = G.ε)
-    (tensor' : ∀ X Y, F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) : F ≅ G
-    where
+    (tensor' : ∀ X Y, F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) :
+    F ≅ G where
   hom := { app := fun X => (app X).hom }
   inv := {
-    (NatIso.ofComponents app
-        @naturality').inv with
+    (NatIso.ofComponents app @naturality').inv with
     app := fun X => (app X).inv
     unit := by
       dsimp

Mathlib/Control/LawfulFix.lean

@@ -65,7 +65,7 @@ theorem approx_mono' {i : ℕ} : Fix.approx f i ≤ Fix.approx f (succ i) := by
 #align part.fix.approx_mono' Part.Fix.approx_mono'
 
 theorem approx_mono ⦃i j : ℕ⦄ (hij : i ≤ j) : approx f i ≤ approx f j := by
-  induction' j with j ih;
+  induction' j with j ih
   · cases hij
     exact le_rfl
   cases hij; · exact le_rfl
@@ -76,14 +76,14 @@ theorem mem_iff (a : α) (b : β a) : b ∈ Part.fix f a ↔ ∃ i, b ∈ approx
   by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
   · simp only [Part.fix_def f h₀]
     constructor <;> intro hh
-    exact ⟨_, hh⟩
+    · exact ⟨_, hh⟩
     have h₁ := Nat.find_spec h₀
     rw [dom_iff_mem] at h₁
     cases' h₁ with y h₁
     replace h₁ := approx_mono' f _ _ h₁
     suffices : y = b
-    subst this
-    exact h₁
+    · subst this
+      exact h₁
     cases' hh with i hh
     revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
     wlog case : i ≤ j
@@ -196,8 +196,7 @@ namespace Part
 
 /-- `toUnit` as a monotone function -/
 @[simps]
-def toUnitMono (f : Part α →o Part α) : (Unit → Part α) →o Unit → Part α
-    where
+def toUnitMono (f : Part α →o Part α) : (Unit → Part α) →o Unit → Part α where
   toFun x u := f (x u)
   monotone' x y (h : x ≤ y) u := f.monotone <| h u
 #align part.to_unit_mono Part.toUnitMono

Mathlib/Data/Finsupp/WellFounded.lean

@@ -21,7 +21,7 @@ lexicographic `(· < ·)` is well-founded on `α →₀ N`.
 `Finsupp.Lex.wellFoundedLT_of_finite` says that if `α` is finite and equipped with a linear order
 and `(· < ·)` is well-founded on `N`, then the lexicographic `(· < ·)` is well-founded on `α →₀ N`.
 
-`Finsupp.wellFoundedLT` and `well_founded_lt_of_finite` state the same results for the product
+`Finsupp.wellFoundedLT` and `wellFoundedLT_of_finite` state the same results for the product
 order `(· < ·)`, but without the ordering conditions on `α`.
 
 All results are transferred from `Dfinsupp` via `Finsupp.toDfinsupp`.
@@ -77,10 +77,10 @@ protected theorem wellFoundedLT [Zero N] [Preorder N] [WellFoundedLT N] (hbot :
   ⟨InvImage.wf toDfinsupp (Dfinsupp.wellFoundedLT fun _ a => hbot a).wf⟩
 #align finsupp.well_founded_lt Finsupp.wellFoundedLT
 
-instance well_founded_lt' {N} [CanonicallyOrderedAddMonoid N] [WellFoundedLT N] :
+instance wellFoundedLT' {N} [CanonicallyOrderedAddMonoid N] [WellFoundedLT N] :
     WellFoundedLT (α →₀ N) :=
   Finsupp.wellFoundedLT fun a => (zero_le a).not_lt
-#align finsupp.well_founded_lt' Finsupp.well_founded_lt'
+#align finsupp.well_founded_lt' Finsupp.wellFoundedLT'
 
 instance wellFoundedLT_of_finite [Finite α] [Zero N] [Preorder N] [WellFoundedLT N] :
     WellFoundedLT (α →₀ N) :=

Mathlib/Data/MvPolynomial/Rename.lean

@@ -207,12 +207,12 @@ theorem rename_eval₂ (g : τ → MvPolynomial σ R) :
       simp [*]
 #align mv_polynomial.rename_eval₂ MvPolynomial.rename_eval₂
 
-theorem rename_prodmk_eval₂ (j : τ) (g : σ → MvPolynomial σ R) :
+theorem rename_prod_mk_eval₂ (j : τ) (g : σ → MvPolynomial σ R) :
     rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C fun x => rename (Prod.mk j) (g x) := by
   apply MvPolynomial.induction_on p <;>
     · intros
       simp [*]
-#align mv_polynomial.rename_prodmk_eval₂ MvPolynomial.rename_prodmk_eval₂
+#align mv_polynomial.rename_prodmk_eval₂ MvPolynomial.rename_prod_mk_eval₂
 
 theorem eval₂_rename_prod_mk (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) :
     (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p := by

Mathlib/Data/Polynomial/DenomsClearable.lean

@@ -16,7 +16,7 @@ import Mathlib.Data.Polynomial.Eval
 
 Let `i : R → K` be a homomorphism of semirings.  Assume that `K` is commutative.  If `a` and
 `b` are elements of `R` such that `i b ∈ K` is invertible, then for any polynomial
-`f ∈ R[X]` the "mathematical" expression `b ^ f.nat_degree * f (a / b) ∈ K` is in
+`f ∈ R[X]` the "mathematical" expression `b ^ f.natDegree * f (a / b) ∈ K` is in
 the image of the homomorphism `i`.
 -/
 
@@ -31,7 +31,7 @@ variable {R K : Type _} [Semiring R] [CommSemiring K] {i : R →+* K}
 
 variable {a b : R} {bi : K}
 
--- TODO: use hypothesis (ub : is_unit (i b)) to work with localizations.
+-- TODO: use hypothesis (ub : IsUnit (i b)) to work with localizations.
 /-- `denomsClearable` formalizes the property that `b ^ N * f (a / b)`
 does not have denominators, if the inequality `f.natDegree ≤ N` holds.
 
@@ -87,7 +87,7 @@ end DenomsClearable
 
 open RingHom
 
---Porting note: `etaExmperiment` is required to synthesize the `RingHomClass (ℤ →+* K) ℤ K` instance
+--Porting note: `etaExperiment` is required to synthesize the `RingHomClass (ℤ →+* K) ℤ K` instance
 set_option synthInstance.etaExperiment true in
 /-- Evaluating a polynomial with integer coefficients at a rational number and clearing
 denominators, yields a number greater than or equal to one.  The target can be any
@@ -98,7 +98,7 @@ theorem one_le_pow_mul_abs_eval_div {K : Type _} [LinearOrderedField K] {f : ℤ
     (b0 : 0 < b) (fab : eval ((a : K) / b) (f.map (algebraMap ℤ K)) ≠ 0) :
     (1 : K) ≤ (b : K) ^ f.natDegree * |eval ((a : K) / b) (f.map (algebraMap ℤ K))| := by
   obtain ⟨ev, bi, bu, hF⟩ :=
-    @denomsClearable_natDegree _ _ _ _ b _ (algebraMap ℤ K) f a
+    denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
       (by
         rw [eq_intCast, one_div_mul_cancel]
         rw [Int.cast_ne_zero]