From ae7ec61a7b0e120ac9bdbeda6f0047c8059f754f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 19 Oct 2023 09:00:56 +0000 Subject: [PATCH] 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 --- Archive/Imo/Imo1960Q1.lean | 2 +- Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean | 1 - Mathlib/Algebra/Category/FGModuleCat/Basic.lean | 5 ----- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean | 2 -- Mathlib/Algebra/Homology/LocalCohomology.lean | 1 - Mathlib/Algebra/Jordan/Basic.lean | 1 - Mathlib/Algebra/Module/PID.lean | 2 +- Mathlib/AlgebraicGeometry/AffineScheme.lean | 6 ++---- Mathlib/AlgebraicGeometry/EllipticCurve/Point.lean | 7 ------- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean | 1 - Mathlib/AlgebraicGeometry/Properties.lean | 1 - Mathlib/Analysis/BoxIntegral/Integrability.lean | 1 - Mathlib/Analysis/Convolution.lean | 2 -- Mathlib/Analysis/InnerProductSpace/Basic.lean | 1 - Mathlib/Analysis/NormedSpace/OperatorNorm.lean | 2 +- Mathlib/CategoryTheory/Monoidal/Bimod.lean | 1 - Mathlib/FieldTheory/AbelRuffini.lean | 3 --- Mathlib/FieldTheory/Cardinality.lean | 1 - Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 1 - Mathlib/FieldTheory/Normal.lean | 3 +-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean | 1 - Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean | 1 - .../Geometry/Manifold/Algebra/LeftInvariantDerivation.lean | 1 - Mathlib/GroupTheory/Perm/List.lean | 1 - Mathlib/LinearAlgebra/AdicCompletion.lean | 2 -- Mathlib/LinearAlgebra/FreeModule/Norm.lean | 3 --- .../QuadraticForm/QuadraticModuleCat/Monoidal.lean | 1 - Mathlib/MeasureTheory/Integral/Bochner.lean | 6 ------ Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean | 3 --- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean | 2 -- Mathlib/NumberTheory/Modular.lean | 2 -- Mathlib/NumberTheory/ModularForms/SlashActions.lean | 1 - Mathlib/RepresentationTheory/Action.lean | 2 -- .../RepresentationTheory/GroupCohomology/Resolution.lean | 3 +-- Mathlib/RepresentationTheory/Rep.lean | 2 -- Mathlib/RingTheory/Adjoin/Field.lean | 3 +-- Mathlib/RingTheory/AdjoinRoot.lean | 1 - Mathlib/RingTheory/Jacobson.lean | 2 -- 38 files changed, 8 insertions(+), 73 deletions(-) diff --git a/Archive/Imo/Imo1960Q1.lean b/Archive/Imo/Imo1960Q1.lean index df450b7c95bf4..5b6a4a08aea0e 100644 --- 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 index 5476d2c43c375..80a3874a9e6c4 100644 --- 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 index bf49b898dd920..e4bc23931c6ca 100644 --- 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 index 2e493440e12ca..9f275ea4bcd83 100644 --- 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 index 77812c4e0adec..48486eaa8f1de 100644 --- 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 index 9e49383b71a59..745fedf19a000 100644 --- 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 index b405853b85741..86fd2d17ad637 100644 --- 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 index 70b6a3ea4db66..8a84450d0fa41 100644 --- 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 index 5967019787f65..6ea93841b6a6c 100644 --- 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 index 1bf7e5c231b67..3bb20c128b91a 100644 --- 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 index 95eaca9ac4bf8..ddaaa15ca1518 100644 --- 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 index a278e514591dc..ccd01bfef3f9f 100644 --- 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 index 5200bd761a8b2..5ae1efbc6f25e 100644 --- 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 index 53bf6878f6e26..e95ce1099b420 100644 --- 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 index ca18178ceae73..c806e9a558524 100644 --- 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 index 62685dcafaa40..deb4b6049ec25 100644 --- 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 index 06e87f0bf8535..266de2b7c4a16 100644 --- 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 index 71cea5ebf8cf5..f1a4ed13e397f 100644 --- 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 index 64b2aeeb58ec8..9a89a9ed7c7ac 100644 --- 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 index e4a49d8256095..188bce0341ebd 100644 --- 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 index 1f65031e230b9..a4af395878bc8 100644 --- 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 index 4a7c60b47d67c..e56f6c784262a 100644 --- 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 index 4aef737c883f1..7da09659c4592 100644 --- 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 index 4d52f2ec62e73..bd0431bdb9e91 100644 --- 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 index d80c9ec3f0135..03809a972c51d 100644 --- 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 index 1cb4e970068f2..4533553bd1613 100644 --- 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 index 175cfe6801ee2..881fc36537788 100644 --- 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 index eac69691e79de..d91f3f72e3ece 100644 --- 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 index d09feb3d41eca..88581fa7e69e3 100644 --- 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 index 2d40e042617cf..7b7731b54bbf6 100644 --- 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 index 1998c88553087..b9bced6e19a27 100644 --- 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 index e14f838c77714..2a417e3e8ab96 100644 --- 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 := diff --git a/Mathlib/RepresentationTheory/Action.lean b/Mathlib/RepresentationTheory/Action.lean index 58279e05a4fd3..8f95e79e1385e 100644 --- a/Mathlib/RepresentationTheory/Action.lean +++ b/Mathlib/RepresentationTheory/Action.lean @@ -564,7 +564,6 @@ set_option linter.uppercaseLean3 false in variable (V G) -set_option maxHeartbeats 400000 in /-- When `V` is monoidal the forgetful functor `Action V G` to `V` is monoidal. -/ @[simps] def forgetMonoidal : MonoidalFunctor (Action V G) V := @@ -583,7 +582,6 @@ section variable [BraidedCategory V] -set_option maxHeartbeats 400000 in instance : BraidedCategory (Action V G) := braidedCategoryOfFaithful (forgetMonoidal V G) (fun X Y => mkIso (β_ _ _) (fun g => by simp [FunctorCategoryEquivalence.inverse])) (by aesop_cat) diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean index 8df4bc2679aa2..a60d54aeba129 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean @@ -266,7 +266,7 @@ end Rep open scoped TensorProduct open Representation -set_option maxHeartbeats 500000 in + /-- The `k[G]`-linear isomorphism `k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹]`, where the `k[G]`-module structure on the lefthand side is `TensorProduct.leftModule`, whilst that of the righthand side comes from `Representation.asModule`. Allows us to use `Algebra.TensorProduct.basis` to get a `k[G]`-basis @@ -704,7 +704,6 @@ instance : EnoughProjectives (Rep k G) := Rep.equivalenceModuleMonoidAlgebra.enoughProjectives_iff.2 ModuleCat.moduleCat_enoughProjectives.{u} -set_option maxHeartbeats 1200000 in /-- Given a `k`-linear `G`-representation `V`, `Extⁿ(k, V)` (where `k` is a trivial `k`-linear `G`-representation) is isomorphic to the `n`th cohomology group of `Hom(P, V)`, where `P` is the standard resolution of `k` called `GroupCohomology.resolution k G`. -/ diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean index aa7180b06b714..5f051c9d60885 100644 --- a/Mathlib/RepresentationTheory/Rep.lean +++ b/Mathlib/RepresentationTheory/Rep.lean @@ -459,8 +459,6 @@ theorem ihom_ev_app_hom (A B : Rep k G) : set_option linter.uppercaseLean3 false in #align Rep.ihom_ev_app_hom Rep.ihom_ev_app_hom -/- Porting note: needs extra heartbeats. -/ -set_option maxHeartbeats 240000 in @[simp] theorem ihom_coev_app_hom (A B : Rep k G) : Action.Hom.hom ((ihom.coev A).app B) = (TensorProduct.mk k _ _).flip := LinearMap.ext fun _ => LinearMap.ext fun _ => rfl diff --git a/Mathlib/RingTheory/Adjoin/Field.lean b/Mathlib/RingTheory/Adjoin/Field.lean index 7a455d2eb6b98..f69f10c6e67d1 100644 --- a/Mathlib/RingTheory/Adjoin/Field.lean +++ b/Mathlib/RingTheory/Adjoin/Field.lean @@ -43,8 +43,7 @@ def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly {R : Type*} [CommRing R] [Alg open Finset -set_option maxHeartbeats 400000 in -set_option synthInstance.maxHeartbeats 160000 in +set_option synthInstance.maxHeartbeats 40000 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] diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index fac4a748d3433..f0d55bef228e3 100644 --- a/Mathlib/RingTheory/AdjoinRoot.lean +++ b/Mathlib/RingTheory/AdjoinRoot.lean @@ -818,7 +818,6 @@ theorem quotAdjoinRootEquivQuotPolynomialQuot_mk_of (p : R[X]) : (p.map (Ideal.Quotient.mk I)) := rfl #align adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_mk_of AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of -set_option maxHeartbeats 300000 in @[simp] theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) : (quotAdjoinRootEquivQuotPolynomialQuot I f).symm diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index d6d6e6d392216..09efecea4f371 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -303,7 +303,6 @@ variable {R S : Type*} [CommRing R] [CommRing S] [IsDomain S] variable {Rₘ Sₘ : Type*} [CommRing Rₘ] [CommRing Sₘ] -set_option maxHeartbeats 300000 in /-- If `I` is a prime ideal of `R[X]` and `pX ∈ I` is a non-constant polynomial, then the map `R →+* R[x]/I` descends to an integral map when localizing at `pX.leadingCoeff`. In particular `X` is integral because it satisfies `pX`, and constants are trivially integral, @@ -433,7 +432,6 @@ private theorem isJacobson_polynomial_of_domain (R : Type*) [CommRing R] [IsDoma haveI islocSₘ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ := by infer_instance exact @isIntegral_isLocalization_polynomial_quotient R _ Rₘ Sₘ _ _ P p pP _ _ _ islocSₘ -set_option maxHeartbeats 300000 in theorem isJacobson_polynomial_of_isJacobson (hR : IsJacobson R) : IsJacobson R[X] := by rw [isJacobson_iff_prime_eq] intro I hI