fix: fill in "in" in maxHeartbeats (#6206)

```bash git ls-files '*.lean' | xargs sed -i "s=maxHeartbeats [0-9]*$=& in=" ``` Affected files: ``` Mathlib/CategoryTheory/Monoidal/Braided.lean:479:set_option maxHeartbeats 400000 Mathlib/FieldTheory/Adjoin.lean:1212:set_option synthInstance.maxHeartbeats 30000 Mathlib/FieldTheory/IsAlgClosed/Basic.lean:302:set_option maxHeartbeats 800000 Mathlib/FieldTheory/IsAlgClosed/Basic.lean:303:set_option synthInstance.maxHeartbeats 400000 Mathlib/RepresentationTheory/GroupCohomology/Basic.lean:202:set_option maxHeartbeats 6400000 Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean:345:set_option maxHeartbeats 800000 Mathlib/Topology/MetricSpace/GromovHausdorff.lean:415:set_option maxHeartbeats 300000 ``` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/set_option.20maxHeartbeats.20with.20no.20.22in.22)
leanprover-community · Jul 28, 2023 · 86ac6bf · 86ac6bf
1 parent c841722
commit 86ac6bf
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 7 deletions.
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean
@@ -476,7 +476,7 @@ theorem tensor_associativity_aux (W X Y Z : C) :
   slice_rhs 3 5 => rw [← tensor_comp, ← tensor_comp, ← hexagon_reverse, tensor_comp, tensor_comp]
 #align category_theory.tensor_associativity_aux CategoryTheory.tensor_associativity_aux
 
-set_option maxHeartbeats 400000
+set_option maxHeartbeats 400000 in
 theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
     (tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫
         tensor_μ C (X₁ ⊗ Y₁, X₂ ⊗ Y₂) (Z₁, Z₂) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) =
@@ -625,6 +625,7 @@ theorem associator_monoidal_aux (W X Y Z : C) :
   simp
 #align category_theory.associator_monoidal_aux CategoryTheory.associator_monoidal_aux
 
+set_option maxHeartbeats 400000 in
 theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
     tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫
         (tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =

diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
@@ -1209,7 +1209,7 @@ theorem sup_toSubalgebra [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K
       (Field.toIsField K)
 #align intermediate_field.sup_to_subalgebra IntermediateField.sup_toSubalgebra
 
-set_option synthInstance.maxHeartbeats 30000
+set_option synthInstance.maxHeartbeats 30000 in
 instance finiteDimensional_sup [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K E2] :
     FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) := by
   let g := Algebra.TensorProduct.productMap E1.val E2.val

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

diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
@@ -199,7 +199,7 @@ noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ :=
     exact map_zero _
 #align group_cohomology.inhomogeneous_cochains GroupCohomology.inhomogeneousCochains
 
-set_option maxHeartbeats 6400000
+set_option maxHeartbeats 6400000 in
 /-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic
 to `Hom(P, A)`, where `P` is the standard resolution of `k` as a trivial `G`-representation. -/
 def inhomogeneousCochainsIso : inhomogeneousCochains A ≅ linearYonedaObjResolution A := by

diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
@@ -342,7 +342,7 @@ theorem diagonalHomEquiv_apply (f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶
 set_option linter.uppercaseLean3 false in
 #align Rep.diagonal_hom_equiv_apply Rep.diagonalHomEquiv_apply
 
-set_option maxHeartbeats 800000
+set_option maxHeartbeats 800000 in
 /-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of
 the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that the
 inverse map sends a function `f : Gⁿ → A` to the representation morphism sending

diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorff.lean b/Mathlib/Topology/MetricSpace/GromovHausdorff.lean
@@ -412,7 +412,7 @@ theorem ghDist_eq_hausdorffDist (X : Type u) [MetricSpace X] [CompactSpace X] [N
     exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm
 #align Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist GromovHausdorff.ghDist_eq_hausdorffDist
 
-set_option maxHeartbeats 300000
+set_option maxHeartbeats 300000 in
 /-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
 instance : MetricSpace GHSpace where
   dist := dist