chore: change Field.toEuclideanDomain (#5266)

Modifying the definition of `Field.toEuclideanDomain` makes some declaration faster.

Co-authored-by:  Sébastien Gouëzel

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -40,24 +40,16 @@ instance Int.euclideanDomain : EuclideanDomain ℤ :=
         rw [←Int.natAbs_pos] at b0
         exact Nat.mul_le_mul_of_nonneg_left b0  }
 
--- Porting note: this seems very slow.
 -- see Note [lower instance priority]
 instance (priority := 100) Field.toEuclideanDomain {K : Type _} [Field K] : EuclideanDomain K :=
-  { ‹Field K› with
-    add := (· + ·), mul := (· * ·), one := 1, zero := 0, neg := Neg.neg,
-    quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
-    quotient_mul_add_remainder_eq := fun a b => by
-      -- Porting note: was `by_cases h : b = 0 <;> simp [h, mul_div_cancel']`
-      by_cases h : b = 0 <;> dsimp only
-      · dsimp only
-        rw [h, zero_mul, mul_zero, zero_div, zero_add, sub_zero]
-      · dsimp only
-        rw [mul_div_cancel' _ h]
-        simp only [ne_eq, h, not_false_iff, mul_div_cancel, sub_self, add_zero]
-    r := fun a b => a = 0 ∧ b ≠ 0,
-    r_wellFounded :=
-      WellFounded.intro fun a =>
-        (Acc.intro _) fun b ⟨hb, _⟩ => (Acc.intro _) fun c ⟨_, hnb⟩ => False.elim <| hnb hb,
-    remainder_lt := fun a b hnb => by simp [hnb],
-    mul_left_not_lt := fun a b hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }
+{ toCommRing := Field.toCommRing
+  quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
+  quotient_mul_add_remainder_eq := fun a b => by
+    by_cases h : b = 0 <;> simp [h, mul_div_cancel']
+  r := fun a b => a = 0 ∧ b ≠ 0,
+  r_wellFounded :=
+    WellFounded.intro fun a =>
+      (Acc.intro _) fun b ⟨hb, _⟩ => (Acc.intro _) fun c ⟨_, hnb⟩ => False.elim <| hnb hb,
+  remainder_lt := fun a b hnb => by simp [hnb],
+  mul_left_not_lt := fun a b hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }
 #align field.to_euclidean_domain Field.toEuclideanDomain

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

@@ -257,7 +257,7 @@ theorem elementalStarAlgebra.bijective_characterSpaceToSpectrum :
 #align elemental_star_algebra.bijective_character_space_to_spectrum elementalStarAlgebra.bijective_characterSpaceToSpectrum
 
 -- porting note: it would be good to understand why and where Lean is having trouble here
-set_option synthInstance.maxHeartbeats 43000 in
+set_option synthInstance.maxHeartbeats 40000 in
 /-- The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
 single normal element `a : A` and `spectrum ℂ a`. -/
 noncomputable def elementalStarAlgebra.characterSpaceHomeo :

Mathlib/FieldTheory/Adjoin.lean

@@ -865,7 +865,6 @@ noncomputable def powerBasisAux {x : L} (hx : IsIntegral K x) :
   (AdjoinRoot.powerBasis (minpoly.ne_zero hx)).basis.map (adjoinRootEquivAdjoin K hx).toLinearEquiv
 #align intermediate_field.power_basis_aux IntermediateField.powerBasisAux
 
-set_option maxHeartbeats 300000 in
 /-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
 where `d` is the degree of the minimal polynomial of `x`. -/
 @[simps]
@@ -1098,7 +1097,7 @@ theorem Lifts.exists_upper_bound (c : Set (Lifts F E K)) (hc : IsChain (· ≤ 
       exact congr_arg z.2 (Subtype.ext hst)⟩
 #align intermediate_field.lifts.exists_upper_bound IntermediateField.Lifts.exists_upper_bound
 
-set_option maxHeartbeats 410000 in
+set_option maxHeartbeats 350000 in
 -- Porting note: instance `alg` added by hand. The proof is very slow.
 /-- Extend a lift `x : Lifts F E K` to an element `s : E` whose conjugates are all in `K` -/
 noncomputable def Lifts.liftOfSplits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s)

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -187,7 +187,6 @@ def toStepZero : k →+* Step k 0 :=
   RingHom.id k
 #align algebraic_closure.to_step_zero AlgebraicClosure.toStepZero
 
-set_option maxHeartbeats 210000 in
 /-- The canonical ring homomorphism to the next step. -/
 def toStepSucc (n : ℕ) : Step k n →+* (Step k (n + 1)) :=
   @toAdjoinMonic (Step k n) (Step.field k n)
@@ -272,9 +271,6 @@ private theorem toStepOfLE.succ (n : ℕ) (h : 0 ≤ n) :
     change _ = (_ ∘ _) x
     rw [toStepOfLE'.succ k 0 n h]
 
---Porting Note: Can probably still be optimized -
---Only the last `convert h` times out with 500000 Heartbeats
-set_option maxHeartbeats 700000 in
 theorem Step.isIntegral (n) : ∀ z : Step k n, IsIntegral k z := by
   induction' n with a h
   · intro z
@@ -349,9 +345,6 @@ theorem exists_ofStep (z : AlgebraicClosure k) : ∃ n x, ofStep k n x = z :=
   Ring.DirectLimit.exists_of z
 #align algebraic_closure.exists_of_step AlgebraicClosure.exists_ofStep
 
--- slow
---Porting Note: Timed out at 800000
-set_option maxHeartbeats 900000 in
 theorem exists_root {f : Polynomial (AlgebraicClosure k)} (hfm : f.Monic) (hfi : Irreducible f) :
     ∃ x : AlgebraicClosure k, f.eval x = 0 := by
   have : ∃ n p, Polynomial.map (ofStep k n) p = f := by

Mathlib/FieldTheory/Normal.lean

@@ -162,7 +162,6 @@ theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F
 -- salient in the future, or at least taking a closer look at the algebra instances it uses.
 attribute [-instance] AdjoinRoot.instSMulAdjoinRoot
 
-set_option maxHeartbeats 300000 in
 theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : Normal F E := by
   rcases eq_or_ne p 0 with (rfl | hp)
   · have := hFEp.adjoin_rootSet

Mathlib/RingTheory/Adjoin/Field.lean

@@ -59,8 +59,8 @@ def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly {R : Type _} [CommRing R] [Al
 
 open Finset
 
-set_option maxHeartbeats 950000 in
-set_option synthInstance.maxHeartbeats 140000 in
+set_option maxHeartbeats 500000 in
+set_option synthInstance.maxHeartbeats 120000 in
 /-- If `K` and `L` are field extensions of `F` and we have `s : Finset K` such that
 the minimal polynomial of each `x ∈ s` splits in `L` then `Algebra.adjoin F s` embeds in `L`. -/
 theorem lift_of_splits {F K L : Type _} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L]