Skip to content

Commit 6fbf296

Browse files
mattrobballmattrobball
committed
comment out bumps again
1 parent b5ec8c8 commit 6fbf296

52 files changed

Lines changed: 86 additions & 86 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Mathlib/Algebra/Category/FGModuleCat/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -265,15 +265,15 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
265265

266266
-- Porting note: extremely slow, was fast in mathlib3.
267267
-- I tried many things using `dsimp` and `change`, but couldn't find anything faster than this.
268-
set_option maxHeartbeats 1600000 in
268+
-- set_option maxHeartbeats 1600000 in
269269
private theorem coevaluation_evaluation :
270270
letI V' : FGModuleCat K := FGModuleCatDual K V
271271
(𝟙 V' ⊗ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 V') =
272272
(ρ_ V').hom ≫ (λ_ V').inv := by
273273
apply contractLeft_assoc_coevaluation K V
274274

275275
-- Porting note: extremely slow, was fast in mathlib3.
276-
set_option maxHeartbeats 400000 in
276+
-- set_option maxHeartbeats 400000 in
277277
private theorem evaluation_coevaluation :
278278
(FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫
279279
(α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =

‎Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -333,7 +333,7 @@ namespace RestrictionCoextensionAdj
333333
variable {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S)
334334

335335
-- Porting note: too much time
336-
set_option maxHeartbeats 500000 in
336+
-- set_option maxHeartbeats 500000 in
337337
/-- Given `R`-module X and `S`-module Y, any `g : (restrictScalars f).obj Y ⟶ X`
338338
corresponds to `Y ⟶ (coextendScalars f).obj X` by sending `y ↦ (s ↦ g (s • y))`
339339
-/

‎Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
125125
#align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality
126126

127127
-- Porting note: very slow!
128-
set_option maxHeartbeats 1200000 in
128+
-- set_option maxHeartbeats 1200000 in
129129
theorem pentagon (W X Y Z : ModuleCat R) :
130130
tensorHom (associator W X Y).hom (𝟙 Z) ≫
131131
(associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =

‎Mathlib/Algebra/DirectLimit.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -733,7 +733,7 @@ protected theorem inv_mul_cancel {p : Ring.DirectLimit G f} (hp : p ≠ 0) : inv
733733
#align field.direct_limit.inv_mul_cancel Field.DirectLimit.inv_mul_cancel
734734

735735
-- porting note: this takes some time, had to increase heartbeats
736-
set_option maxHeartbeats 500000 in
736+
-- set_option maxHeartbeats 500000 in
737737
/-- Noncomputable field structure on the direct limit of fields.
738738
See note [reducible non-instances]. -/
739739
@[reducible]

‎Mathlib/Algebra/Homology/DifferentialObject.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ theorem d_eqToHom (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (
8080
X.d x y ≫ eqToHom (congr_arg X.X h) = X.d x z := by cases h; simp
8181
#align homological_complex.d_eq_to_hom HomologicalComplex.d_eqToHom
8282

83-
set_option maxHeartbeats 400000 in
83+
-- set_option maxHeartbeats 400000 in
8484
/-- The functor from differential graded objects to homological complexes.
8585
-/
8686
@[simps]

‎Mathlib/Algebra/Homology/LocalCohomology.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ variable {R : Type max u v v'} [CommRing R] {D : Type v} [SmallCategory D]
116116

117117
variable {E : Type v'} [SmallCategory E] (I' : E ⥤ D) (I : D ⥤ Ideal R)
118118

119-
set_option maxHeartbeats 250000 in
119+
-- set_option maxHeartbeats 250000 in
120120
/-- Local cohomology along a composition of diagrams. -/
121121
def diagramComp (i : ℕ) : diagram (I' ⋙ I) i ≅ I'.op ⋙ diagram I i :=
122122
Iso.refl _

‎Mathlib/Algebra/Jordan/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ private theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c
194194
simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
195195
abel
196196

197-
set_option maxHeartbeats 250000 in
197+
-- set_option maxHeartbeats 250000 in
198198
private theorem aux1 {a b c : A} :
199199
⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) +
200200
2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
@@ -208,7 +208,7 @@ private theorem aux1 {a b c : A} :
208208
rw [add_lie, add_lie]
209209
iterate 15 rw [lie_add]
210210

211-
set_option maxHeartbeats 300000 in
211+
-- set_option maxHeartbeats 300000 in
212212
private theorem aux2 {a b c : A} :
213213
⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ +
214214
⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ +

‎Mathlib/Algebra/Module/GradedModule.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ namespace GradedModule
208208
variable [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A]
209209
[AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜]
210210

211-
set_option maxHeartbeats 300000 in -- Porting note: needs more Heartbeats to elaborate
211+
-- set_option maxHeartbeats 300000 in -- Porting note: needs more Heartbeats to elaborate
212212
/-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
213213
turns `⨁ i, 𝓜 i` into an `A`-module
214214
-/

‎Mathlib/Algebra/Module/LocalizedModule.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ theorem mk_neg {M : Type*} [AddCommGroup M] [Module R M] {m : M} {s : S} : mk (-
237237
rfl
238238
#align localized_module.mk_neg LocalizedModule.mk_neg
239239

240-
set_option maxHeartbeats 400000 in
240+
-- set_option maxHeartbeats 400000 in
241241
instance {A : Type _} [Semiring A] [Algebra R A] {S : Submonoid R} :
242242
Semiring (LocalizedModule S A) :=
243243
{ show (AddCommMonoid (LocalizedModule S A)) by infer_instance with

‎Mathlib/Algebra/Module/PID.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@ theorem exists_smul_eq_zero_and_mk_eq {z : M} (hz : Module.IsTorsionBy R M (p ^
164164

165165
open Finset Multiset
166166

167-
set_option maxHeartbeats 800000 in
167+
-- set_option maxHeartbeats 800000 in
168168
/-- A finitely generated `p ^ ∞`-torsion module over a PID is isomorphic to a direct sum of some
169169
`R ⧸ R ∙ (p ^ e i)` for some `e i`.-/
170170
theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoid.powers p))

0 commit comments

Comments
 (0)