chore: removing unneeded maxHeartbeats (#7761)

Due to recent changes in core we can reduce or remove many `set_option maxHeartbeats` statements. I have tried to be careful to not leave anything too close to the line, so don't be surprised if some of these can still be reduced further. This reduces us from 96 `maxHeartbeats` statements to `44`. (There are 10 false positives in meta or testing code.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Oct 19, 2023 · ae7ec61 · ae7ec61
1 parent d478563
commit ae7ec61
Show file tree

Hide file tree

Showing 38 changed files with 8 additions and 73 deletions.
diff --git a/Archive/Imo/Imo1960Q1.lean b/Archive/Imo/Imo1960Q1.lean
@@ -90,7 +90,7 @@ theorem searchUpTo_end {c} (H : SearchUpTo c 1001) {n : ℕ} (ppn : ProblemPredi
   H.2 _ (by linarith [lt_1000 ppn]) ppn
 #align imo1960_q1.search_up_to_end Imo1960Q1.searchUpTo_end
 
-set_option maxHeartbeats 2000000 in
+set_option maxHeartbeats 800000 in
 theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n := by
   have := searchUpTo_start
   iterate 82

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -60,7 +60,6 @@ theorem forget₂_map_associator_hom (X Y Z : AlgebraCat.{u} R) :
         (forget₂ _ (ModuleCat R) |>.obj Z)).hom := by
   rfl
 
-set_option maxHeartbeats 400000 in
 theorem forget₂_map_associator_inv (X Y Z : AlgebraCat.{u} R) :
     (forget₂ (AlgebraCat R) (ModuleCat R)).map (associator X Y Z).inv =
       (α_

diff --git a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
@@ -264,17 +264,12 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
   contractLeft_apply f x
 #align fgModule.fgModule_evaluation_apply FGModuleCat.FGModuleCatEvaluation_apply
 
--- Porting note: extremely slow, was fast in mathlib3.
--- I tried many things using `dsimp` and `change`, but couldn't find anything faster than this.
-set_option maxHeartbeats 1500000 in
 private theorem coevaluation_evaluation :
     letI V' : FGModuleCat K := FGModuleCatDual K V
     (𝟙 V' ⊗ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 V') =
       (ρ_ V').hom ≫ (λ_ V').inv := by
   apply contractLeft_assoc_coevaluation K V
 
--- Porting note: extremely slow, was fast in mathlib3.
-set_option maxHeartbeats 400000 in
 private theorem evaluation_coevaluation :
     (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫
         (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -136,8 +136,6 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
   by convert associator_naturality_aux f₁ f₂ f₃ using 1
 #align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality
 
--- Porting note: very slow!
-set_option maxHeartbeats 1200000 in
 theorem pentagon (W X Y Z : ModuleCat R) :
     tensorHom (associator W X Y).hom (𝟙 Z) ≫
         (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =

diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean
@@ -122,7 +122,6 @@ variable {R : Type max u v v'} [CommRing R] {D : Type v} [SmallCategory D]
 
 variable {E : Type v'} [SmallCategory E] (I' : E ⥤ D) (I : D ⥤ Ideal R)
 
-set_option maxHeartbeats 250000 in
 /-- Local cohomology along a composition of diagrams. -/
 def diagramComp (i : ℕ) : diagram (I' ⋙ I) i ≅ I'.op ⋙ diagram I i :=
   Iso.refl _

diff --git a/Mathlib/Algebra/Jordan/Basic.lean b/Mathlib/Algebra/Jordan/Basic.lean
@@ -194,7 +194,6 @@ private theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c
   simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
   abel
 
-set_option maxHeartbeats 250000 in
 private theorem aux1 {a b c : A} :
     ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) +
     2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean
@@ -164,7 +164,7 @@ theorem exists_smul_eq_zero_and_mk_eq {z : M} (hz : Module.IsTorsionBy R M (p ^
 
 open Finset Multiset
 
-set_option maxHeartbeats 800000 in
+set_option maxHeartbeats 400000 in
 /-- A finitely generated `p ^ ∞`-torsion module over a PID is isomorphic to a direct sum of some
   `R ⧸ R ∙ (p ^ e i)` for some `e i`.-/
 theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoid.powers p))

diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -501,7 +501,6 @@ instance basicOpenSectionsToAffine_isIso {X : Scheme} {U : Opens X} (hU : IsAffi
     rw [hU.fromSpec_range]
     exact RingedSpace.basicOpen_le _ _
 
-set_option maxHeartbeats 300000 in
 theorem isLocalization_basicOpen {X : Scheme} {U : Opens X} (hU : IsAffineOpen U)
     (f : X.presheaf.obj (op U)) : IsLocalization.Away f (X.presheaf.obj (op <| X.basicOpen f)) := by
   apply
@@ -607,7 +606,7 @@ theorem IsAffineOpen.fromSpec_primeIdealOf {X : Scheme} {U : Opens X} (hU : IsAf
 
 -- Porting note : the original proof does not compile under 0 `heartbeat`, so partially rewritten
 -- but after the rewrite, I still can't get it compile under `200000`
-set_option maxHeartbeats 640000 in
+set_option maxHeartbeats 400000 in
 theorem IsAffineOpen.isLocalization_stalk_aux {X : Scheme} (U : Opens X)
     [IsAffine (X.restrict U.openEmbedding)] :
     (inv (ΓSpec.adjunction.unit.app (X.restrict U.openEmbedding))).1.c.app
@@ -630,7 +629,7 @@ theorem IsAffineOpen.isLocalization_stalk_aux {X : Scheme} (U : Opens X)
   rw [eqToHom_trans]
 #align algebraic_geometry.is_affine_open.is_localization_stalk_aux AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux
 
-set_option maxHeartbeats 1600000 in
+set_option maxHeartbeats 800000 in
 theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U)
     (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) :
     hU.fromSpec.val.c.app (op U) ≫ (Scheme.Spec.obj <| op (X.presheaf.obj <| op U)).presheaf.germ
@@ -661,7 +660,6 @@ theorem IsAffineOpen.isLocalization_stalk_aux' {X : Scheme} {U : Opens X} (hU :
   rw [Category.id_comp]
   rfl
 
-set_option maxHeartbeats 500000 in
 theorem IsAffineOpen.isLocalization_stalk' {X : Scheme} {U : Opens X} (hU : IsAffineOpen U)
     (y : PrimeSpectrum (X.presheaf.obj <| op U)) (hy : hU.fromSpec.1.base y ∈ U) :
   haveI : IsAffine _ := hU

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Point.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Point.lean
@@ -511,8 +511,6 @@ lemma Y_eq_of_Y_ne (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) : y₁ =
 set_option linter.uppercaseLean3 false in
 #align weierstrass_curve.Y_eq_of_Y_ne WeierstrassCurve.Y_eq_of_Y_ne
 
--- porting note: increased `maxHeartbeats` for `ring1`
-set_option synthInstance.maxHeartbeats 30000 in
 lemma XYIdeal_eq₂ (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) :
     XYIdeal W x₂ (C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) := by
   -- porting note: removed assumption `h₂` explicitly
@@ -717,8 +715,6 @@ variable {F : Type u} [Field F] {W : WeierstrassCurve F} {x₁ x₂ y₁ y₂ :
   (h₁ : W.nonsingular x₁ y₁) (h₂ : W.nonsingular x₂ y₂) (h₁' : W.equation x₁ y₁)
   (h₂' : W.equation x₂ y₂)
 
--- porting note: increased `maxHeartbeats` for `ring1`
-set_option maxHeartbeats 800000 in
 lemma XYIdeal_neg_mul : XYIdeal W x₁ (C <| W.negY x₁ y₁) * XYIdeal W x₁ (C y₁) = XIdeal W x₁ := by
   have Y_rw :
     (Y - C (C y₁)) * (Y - C (C (W.negY x₁ y₁))) -
@@ -760,9 +756,6 @@ private lemma XYIdeal'_mul_inv :
   rw [← mul_assoc, ← FractionalIdeal.coeIdeal_mul, mul_comm <| XYIdeal W _ _, XYIdeal_neg_mul h₁,
     XIdeal, FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero W x₁]
 
--- porting note: increased `maxHeartbeats` for `ring1`
-set_option synthInstance.maxHeartbeats 60000 in
-set_option maxHeartbeats 600000 in
 lemma XYIdeal_mul_XYIdeal (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) :
     XIdeal W (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) =
       YIdeal W (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) *

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
@@ -579,7 +579,6 @@ theorem affineLocally_of_isOpenImmersion (hP : RingHom.PropertyIsLocal @P) {X Y
   · intro; exact H
 #align ring_hom.property_is_local.affine_locally_of_is_open_immersion RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion
 
-set_option maxHeartbeats 3000000 in
 theorem affineLocally_of_comp
     (H : ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T],
       ∀ (f : R →+* S) (g : S →+* T), P (g.comp f) → P g)

diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean
@@ -89,7 +89,6 @@ theorem isReducedOfOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersi
       Y.presheaf.obj _ ≅ _).symm.commRingCatIsoToRingEquiv.injective
 #align algebraic_geometry.is_reduced_of_open_immersion AlgebraicGeometry.isReducedOfOpenImmersion
 
-set_option maxHeartbeats 250000 in
 instance {R : CommRingCat} [H : _root_.IsReduced R] : IsReduced (Scheme.Spec.obj <| op R) := by
   apply (config := { allowSynthFailures := true }) isReducedOfStalkIsReduced
   intro x; dsimp

diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean
@@ -113,7 +113,6 @@ theorem HasIntegral.of_aeEq_zero {l : IntegrationParams} {I : Box ι} {f : (ι
   set N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊
   have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp
   have : ∀ n, ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦ by
-    set_option synthInstance.maxHeartbeats 21000 in
     refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
     cases' n with n
     · simpa [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne'] using measure_lt_top (μ.restrict I) _

diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
@@ -1196,8 +1196,6 @@ variable [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace
   [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G}
   (L : E →L[𝕜] E' →L[𝕜] F)
 
--- porting note: the lemma is slow, added `set_option maxHeartbeats 250000 in`
-set_option maxHeartbeats 250000 in
 /-- The derivative of the convolution `f * g` is given by `f * Dg`, when `f` is locally integrable
 and `g` is `C^1` and compactly supported. Version where `g` depends on an additional parameter in an
 open subset `s` of a parameter space `P` (and the compact support `k` is independent of the

diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -1822,7 +1822,6 @@ namespace ContinuousLinearMap
 variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
 
 -- Note: odd and expensive build behavior is explicitly turned off using `noncomputable`
-set_option synthInstance.maxHeartbeats 40000 in
 /-- Given `f : E →L[𝕜] E'`, construct the continuous sesquilinear form `fun x y ↦ ⟪x, A y⟫`, given
 as a continuous linear map. -/
 noncomputable def toSesqForm : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜 :=

diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
@@ -1014,7 +1014,7 @@ variable (M₁ : Type u₁) [SeminormedAddCommGroup M₁] [NormedSpace 𝕜 M₁
 
 variable {Eₗ} (𝕜)
 
-set_option maxHeartbeats 500000 in
+set_option maxHeartbeats 400000 in
 /-- `ContinuousLinearMap.prodMap` as a continuous linear map. -/
 def prodMapL : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
   ContinuousLinearMap.copy

diff --git a/Mathlib/CategoryTheory/Monoidal/Bimod.lean b/Mathlib/CategoryTheory/Monoidal/Bimod.lean
@@ -972,7 +972,6 @@ theorem whisker_exchange_bimod {X Y Z : Mon_ C} {M N : Bimod X Y} {P Q : Bimod Y
 set_option linter.uppercaseLean3 false in
 #align Bimod.whisker_exchange_Bimod Bimod.whisker_exchange_bimod
 
-set_option maxHeartbeats 400000 in
 theorem pentagon_bimod {V W X Y Z : Mon_ C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y)
     (Q : Bimod Y Z) :
     tensorHom (associatorBimod M N P).hom (𝟙 Q) ≫

diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean
@@ -117,7 +117,6 @@ theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).G
 set_option linter.uppercaseLean3 false in
 #align gal_X_pow_sub_one_is_solvable gal_X_pow_sub_one_isSolvable
 
-set_option maxHeartbeats 250000 in
 theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
     (h : (X ^ n - 1 : F[X]).Splits (RingHom.id F)) : IsSolvable (X ^ n - C a).Gal := by
   by_cases ha : a = 0
@@ -157,7 +156,6 @@ theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
 set_option linter.uppercaseLean3 false in
 #align gal_X_pow_sub_C_is_solvable_aux gal_X_pow_sub_C_isSolvable_aux
 
-set_option maxHeartbeats 250000 in
 theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [Field E]
     (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : (X ^ n - C a).Splits i) :
     (X ^ n - 1 : F[X]).Splits i := by
@@ -309,7 +307,6 @@ def P (α : solvableByRad F E) : Prop :=
 set_option linter.uppercaseLean3 false in
 #align solvable_by_rad.P solvableByRad.P
 
-set_option maxHeartbeats 400000 in
 /-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
 theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (α ^ n)) : P α := by
   let p := minpoly F (α ^ n)

diff --git a/Mathlib/FieldTheory/Cardinality.lean b/Mathlib/FieldTheory/Cardinality.lean
@@ -62,7 +62,6 @@ theorem Fintype.not_isField_of_card_not_prime_pow {α} [Fintype α] [Ring α] :
   mt fun h => Fintype.nonempty_field_iff.mp ⟨h.toField⟩
 #align fintype.not_is_field_of_card_not_prime_pow Fintype.not_isField_of_card_not_prime_pow
 
-set_option synthInstance.maxHeartbeats 50000 in
 /-- Any infinite type can be endowed a field structure. -/
 theorem Infinite.nonempty_field {α : Type u} [Infinite α] : Nonempty (Field α) := by
   letI K := FractionRing (MvPolynomial α <| ULift.{u} ℚ)

diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
@@ -318,7 +318,6 @@ AlgHom.comp
   (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly R x).toAlgHom
 
 -- porting note: this was much faster in lean 3
-set_option maxHeartbeats 300000 in
 set_option synthInstance.maxHeartbeats 200000 in
 theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom K L M).carrier = ⊤ := by
   rw [eq_top_iff]

diff --git a/Mathlib/FieldTheory/Normal.lean b/Mathlib/FieldTheory/Normal.lean
@@ -227,8 +227,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] :
     rw [AdjoinRoot.adjoinRoot_eq_top, Subalgebra.restrictScalars_top, ←
       @Subalgebra.restrictScalars_top F C] at this
     exact top_le_iff.mpr (Subalgebra.restrictScalars_injective F this)
-/- Porting note: the `change` was `dsimp only [S]`. This is the step that requires increasing
-`maxHeartbeats`. Using `set S ... with hS` doesn't work. -/
+/- Porting note: the `change` was `dsimp only [S]`. Using `set S ... with hS` doesn't work. -/
   change Subalgebra.restrictScalars F (Algebra.adjoin C
     (((p.aroots E).map (algebraMap E D)).toFinset : Set D)) = _
   rw [← Finset.image_toFinset, Finset.coe_image]

diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean
@@ -330,7 +330,6 @@ theorem mul_splits_in_splittingField_of_mul {p₁ q₁ p₂ q₂ : F[X]} (hq₁
     exact splits_comp_of_splits _ _ h₂
 #align polynomial.gal.mul_splits_in_splitting_field_of_mul Polynomial.Gal.mul_splits_in_splittingField_of_mul
 
-set_option maxHeartbeats 300000 in
 /-- `p` splits in the splitting field of `p ∘ q`, for `q` non-constant. -/
 theorem splits_in_splittingField_of_comp (hq : q.natDegree ≠ 0) :
     p.Splits (algebraMap F (p.comp q).SplittingField) := by

diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
@@ -1065,7 +1065,6 @@ theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ :
       mul_comm r₃]
 #align orientation.oangle_sign_smul_add_smul_smul_add_smul Orientation.oangle_sign_smul_add_smul_smul_add_smul
 
-set_option maxHeartbeats 350000 in
 /-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/
 theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) :
     |(o.oangle (y - x) y).toReal| < π / 2 := by

diff --git a/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean b/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
@@ -146,7 +146,6 @@ instance : Neg (LeftInvariantDerivation I G) where
     rw [map_neg (Derivation.evalAt (𝕜 := 𝕜) (1 : G)), map_neg (𝒅ₕ (smoothLeftMul_one I g)),
       left_invariant', map_neg (Derivation.evalAt (𝕜 := 𝕜) g)]⟩
 
-set_option maxHeartbeats 300000 in
 instance : Sub (LeftInvariantDerivation I G) where
   sub X Y := ⟨X - Y, fun g => by
     -- porting note: was simp [left_invariant']

diff --git a/Mathlib/GroupTheory/Perm/List.lean b/Mathlib/GroupTheory/Perm/List.lean
@@ -99,7 +99,6 @@ theorem formPerm_apply_mem_of_mem (x : α) (l : List α) (h : x ∈ l) : formPer
       simp [formPerm_apply_of_not_mem _ _ hx, ← h]
 #align list.form_perm_apply_mem_of_mem List.formPerm_apply_mem_of_mem
 
-set_option maxHeartbeats 220000 in
 theorem mem_of_formPerm_apply_mem (x : α) (l : List α) (h : l.formPerm x ∈ l) : x ∈ l := by
   cases' l with y l
   · simp at h

diff --git a/Mathlib/LinearAlgebra/AdicCompletion.lean b/Mathlib/LinearAlgebra/AdicCompletion.lean
@@ -212,7 +212,6 @@ def of : M →ₗ[R] adicCompletion I M where
   map_smul' _ _ := rfl
 #align adic_completion.of adicCompletion.of
 
-set_option maxHeartbeats 300000 in
 @[simp]
 theorem of_apply (x : M) (n : ℕ) : (of I M x).1 n = mkQ _ x :=
   rfl
@@ -235,7 +234,6 @@ theorem eval_apply (n : ℕ) (f : adicCompletion I M) : eval I M n f = f.1 n :=
   rfl
 #align adic_completion.eval_apply adicCompletion.eval_apply
 
-set_option maxHeartbeats 300000 in
 theorem eval_of (n : ℕ) (x : M) : eval I M n (of I M x) = mkQ _ x :=
   rfl
 #align adic_completion.eval_of adicCompletion.eval_of

diff --git a/Mathlib/LinearAlgebra/FreeModule/Norm.lean b/Mathlib/LinearAlgebra/FreeModule/Norm.lean
@@ -69,9 +69,6 @@ instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) :
   refine AdjoinRoot.powerBasis ?_
   refine I.smithCoeffs_ne_zero b hI i
 
--- Porting note: this proof was already slow in mathlib3 and it is even slower now
--- See: https://github.com/leanprover-community/mathlib4/issues/5028
-set_option maxHeartbeats 1000000 in
 /-- For a nonzero element `f` in a `F[X]`-module `S`, the dimension of $S/\langle f \rangle$ as an
 `F`-vector space is the degree of the norm of `f` relative to `F[X]`. -/
 theorem finrank_quotient_span_eq_natDegree_norm [Algebra F S] [IsScalarTower F F[X] S]

diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
@@ -70,7 +70,6 @@ end instMonoidalCategory
 
 open instMonoidalCategory
 
-set_option maxHeartbeats 400000 in
 noncomputable instance instMonoidalCategory : MonoidalCategory (QuadraticModuleCat.{u} R) :=
   Monoidal.induced
     (forget₂ (QuadraticModuleCat R) (ModuleCat R))

diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -539,12 +539,6 @@ theorem integral_add (f g : α →₁ₛ[μ] E) : integral (f + g) = integral f
   setToL1S_add _ (fun _ _ => weightedSMul_null) weightedSMul_union _ _
 #align measure_theory.L1.simple_func.integral_add MeasureTheory.L1.SimpleFunc.integral_add
 
--- Porting note: finding `SMul 𝕜 (Lp.simpleFunc E 1 μ)` takes about twice the default
--- `synthInstance.maxHeartbeats 20000`, so we provide some shortcut instances to speed it up.
-instance : Module 𝕜 (Lp.simpleFunc E 1 μ) := inferInstance in
-instance : MulActionWithZero 𝕜 (Lp.simpleFunc E 1 μ) := inferInstance in
-instance : SMul 𝕜 (Lp.simpleFunc E 1 μ) := inferInstance
-
 theorem integral_smul (c : 𝕜) (f : α →₁ₛ[μ] E) : integral (c • f) = c • integral f :=
   setToL1S_smul _ (fun _ _ => weightedSMul_null) weightedSMul_union weightedSMul_smul c f
 #align measure_theory.L1.simple_func.integral_smul MeasureTheory.L1.SimpleFunc.integral_smul

diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean
@@ -259,9 +259,6 @@ in this way, the result is reduced to `card_pow_char_pow`.
 
 open ZMod
 
--- Porting note: This proof is _really_ slow, maybe it should be broken into several lemmas
--- See https://github.com/leanprover-community/mathlib4/issues/5028
-set_option maxHeartbeats 500000 in
 /-- For every finite field `F` of odd characteristic, we have `2^(#F/2) = χ₈#F` in `F`. -/
 theorem FiniteField.two_pow_card {F : Type*} [Fintype F] [Field F] (hF : ringChar F ≠ 2) :
     (2 : F) ^ (Fintype.card F / 2) = χ₈ (Fintype.card F) := by

diff --git a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
@@ -128,7 +128,6 @@ theorem neg_one_pow_div_two_of_three_mod_four {n : ℕ} (hn : n % 4 = 3) :
   rfl
 #align zmod.neg_one_pow_div_two_of_three_mod_four ZMod.neg_one_pow_div_two_of_three_mod_four
 
-set_option maxHeartbeats 250000 in -- Porting note: otherwise `map_nonunit'` times out
 /-- Define the first primitive quadratic character on `ZMod 8`, `χ₈`.
 It corresponds to the extension `ℚ(√2)/ℚ`. -/
 @[simps]
@@ -172,7 +171,6 @@ theorem χ₈_nat_eq_if_mod_eight (n : ℕ) :
   exact_mod_cast χ₈_int_eq_if_mod_eight n
 #align zmod.χ₈_nat_eq_if_mod_eight ZMod.χ₈_nat_eq_if_mod_eight
 
-set_option maxHeartbeats 250000 in -- Porting note: otherwise `map_nonunit'` times out
 /-- Define the second primitive quadratic character on `ZMod 8`, `χ₈'`.
 It corresponds to the extension `ℚ(√-2)/ℚ`. -/
 @[simps]

diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
@@ -369,7 +369,6 @@ theorem g_eq_of_c_eq_one (hc : (↑ₘg) 1 0 = 1) : g = T ^ (↑ₘg) 0 0 * S *
   congrm !![?_, ?_; ?_, ?_] <;> ring
 #align modular_group.g_eq_of_c_eq_one ModularGroup.g_eq_of_c_eq_one
 
-set_option maxHeartbeats 250000 in
 /-- If `1 < |z|`, then `|S • z| < 1`. -/
 theorem normSq_S_smul_lt_one (h : 1 < normSq z) : normSq ↑(S • z) < 1 := by
   simpa [coe_S, num, denom] using (inv_lt_inv z.normSq_pos zero_lt_one).mpr h
@@ -415,7 +414,6 @@ theorem three_lt_four_mul_im_sq_of_mem_fdo (h : z ∈ 𝒟ᵒ) : 3 < 4 * z.im ^
   cases abs_cases z.re <;> nlinarith
 #align modular_group.three_lt_four_mul_im_sq_of_mem_fdo ModularGroup.three_lt_four_mul_im_sq_of_mem_fdo
 
-set_option maxHeartbeats 260000 in
 /-- If `z ∈ 𝒟ᵒ`, and `n : ℤ`, then `|z + n| > 1`. -/
 theorem one_lt_normSq_T_zpow_smul (hz : z ∈ 𝒟ᵒ) (n : ℤ) : 1 < normSq (T ^ n • z : ℍ) := by
   have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1

diff --git a/Mathlib/NumberTheory/ModularForms/SlashActions.lean b/Mathlib/NumberTheory/ModularForms/SlashActions.lean
@@ -221,7 +221,6 @@ theorem mul_slash (k1 k2 : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
   ring
 #align modular_form.mul_slash ModularForm.mul_slash
 
-set_option maxHeartbeats 600000 in
 -- @[simp] -- Porting note: simpNF says LHS simplifies to something more complex
 theorem mul_slash_SL2 (k1 k2 : ℤ) (A : SL(2, ℤ)) (f g : ℍ → ℂ) :
     (f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A :=