increase max heartbeats

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -662,6 +662,8 @@ theorem app_eq_inv_app_app_of_comp_eq_aux {X Y U : Scheme} (f : Y ⟶ U) (g : U
   exact (Set.preimage_image_eq _ h.base_open.inj).symm
 #align algebraic_geometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux AlgebraicGeometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 /-- The `fg` argument is to avoid nasty stuff about dependent types. -/
 theorem app_eq_invApp_app_of_comp_eq {X Y U : Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X)
     (H : fg = f ≫ g) [h : IsOpenImmersion g] (V : Opens U) :
@@ -678,6 +680,8 @@ theorem app_eq_invApp_app_of_comp_eq {X Y U : Scheme} (f : Y ⟶ U) (g : U ⟶ X
   convert Y.presheaf.map_id _
 #align algebraic_geometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 theorem lift_app {X Y U : Scheme} (f : U ⟶ Y) (g : X ⟶ Y) [IsOpenImmersion f] (H)
     (V : Opens U) :
     (IsOpenImmersion.lift f g H).1.c.app (op V) =

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -49,6 +49,9 @@ abbrev Scheme.ιOpens {X : Scheme} (U : Opens X.carrier) : X ∣_ᵤ U ⟶ X :=
 lemma Scheme.ofRestrict_val_c_app_self {X : Scheme} (U : Opens X) :
     (X.ofRestrict U.openEmbedding).1.c.app (op U) = X.presheaf.map (eqToHom (by simp)).op := rfl
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 320000 in
+set_option maxHeartbeats 800000 in
 lemma Scheme.eq_restrict_presheaf_map_eqToHom {X : Scheme} (U : Opens X) {V W : Opens U}
     (e : U.openEmbedding.isOpenMap.functor.obj V = U.openEmbedding.isOpenMap.functor.obj W) :
   X.presheaf.map (eqToHom e).op =
@@ -142,6 +145,9 @@ theorem Scheme.restrictFunctor_map_app_aux {U V : Opens X} (i : U ⟶ V) (W : Op
   exact ⟨_, h, rfl⟩
 #align algebraic_geometry.Scheme.restrict_functor_map_app_aux AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 640000 in
+set_option maxHeartbeats 800000 in
 theorem Scheme.restrictFunctor_map_app {U V : Opens X} (i : U ⟶ V) (W : Opens V) :
     (X.restrictFunctor.map i).1.1.c.app (op W) =
       X.presheaf.map (homOfLE <| X.restrictFunctor_map_app_aux i W).op := by
@@ -334,6 +340,9 @@ theorem image_morphismRestrict_preimage {X Y : Scheme} (f : X ⟶ Y) (U : Opens
     exact morphismRestrict_base_coe f U ⟨x, hx⟩
 #align algebraic_geometry.image_morphism_restrict_preimage AlgebraicGeometry.image_morphismRestrict_preimage
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 1280000 in
+set_option maxHeartbeats 1600000 in
 theorem morphismRestrict_c_app {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) (V : Opens U) :
     (f ∣_ U).1.c.app (op V) =
       f.1.c.app (op (U.openEmbedding.isOpenMap.functor.obj V)) ≫
@@ -354,6 +363,9 @@ theorem morphismRestrict_c_app {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) (V : O
     congr 1
 #align algebraic_geometry.morphism_restrict_c_app AlgebraicGeometry.morphismRestrict_c_app
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 640000 in
+set_option maxHeartbeats 800000 in
 theorem Γ_map_morphismRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) :
     Scheme.Γ.map (f ∣_ U).op =
       Y.presheaf.map (eqToHom <| U.openEmbedding_obj_top.symm).op ≫

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -140,6 +140,8 @@ theorem comp_val_base_apply {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X)
   simp
 #align algebraic_geometry.Scheme.comp_val_base_apply AlgebraicGeometry.Scheme.comp_val_base_apply
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 @[simp, reassoc] -- reassoc lemma does not need `simp`
 theorem comp_val_c_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
     (f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app _ :=
@@ -151,6 +153,8 @@ theorem congr_app {X Y : Scheme} {f g : X ⟶ Y} (e : f = g) (U) :
   subst e; dsimp; simp
 #align algebraic_geometry.Scheme.congr_app AlgebraicGeometry.Scheme.congr_app
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 theorem app_eq {X Y : Scheme} (f : X ⟶ Y) {U V : Opens Y.carrier} (e : U = V) :
     f.val.c.app (op U) =
       Y.presheaf.map (eqToHom e.symm).op ≫
@@ -177,6 +181,8 @@ instance {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U) : IsIso (f.val.c.app U) :=
   haveI := PresheafedSpace.c_isIso_of_iso f.val
   NatIso.isIso_app_of_isIso _ _
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 @[simp]
 theorem inv_val_c_app {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U : Opens X.carrier) :
     (inv f).val.c.app (op U) =
@@ -190,6 +196,8 @@ theorem inv_val_c_app {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U : Opens X.carrie
     eqToHom_op]
 #align algebraic_geometry.Scheme.inv_val_c_app AlgebraicGeometry.Scheme.inv_val_c_app
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 theorem inv_val_c_app_top {X Y : Scheme} (f : X ⟶ Y) [IsIso f] :
     (inv f).val.c.app (op ⊤) = inv (f.val.c.app (op ⊤)) := by simp
 
@@ -278,11 +286,15 @@ theorem Γ_obj_op (X : Scheme) : Γ.obj (op X) = X.presheaf.obj (op ⊤) :=
   rfl
 #align algebraic_geometry.Scheme.Γ_obj_op AlgebraicGeometry.Scheme.Γ_obj_op
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 @[simp]
 theorem Γ_map {X Y : Schemeᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.1.c.app (op ⊤) :=
   rfl
 #align algebraic_geometry.Scheme.Γ_map AlgebraicGeometry.Scheme.Γ_map
 
+#adaptation_note /-- These maxHeartbeats increases are due to leanprover/lean4#4085. -/
+set_option synthInstance.maxHeartbeats 40000 in
 theorem Γ_map_op {X Y : Scheme} (f : X ⟶ Y) : Γ.map f.op = f.1.c.app (op ⊤) :=
   rfl
 #align algebraic_geometry.Scheme.Γ_map_op AlgebraicGeometry.Scheme.Γ_map_op

Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

@@ -180,6 +180,7 @@ theorem comp_val_c {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.comp_val_c AlgebraicGeometry.LocallyRingedSpace.comp_val_c
 
+set_option synthInstance.maxHeartbeats 30000 in
 theorem comp_val_c_app {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (Opens Z)ᵒᵖ) :
     (f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app (op <| (Opens.map g.val.base).obj U.unop) :=
   rfl
@@ -281,12 +282,14 @@ theorem Γ_obj_op (X : LocallyRingedSpace) : Γ.obj (op X) = X.presheaf.obj (op
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.Γ_obj_op AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op
 
+set_option synthInstance.maxHeartbeats 30000 in
 @[simp]
 theorem Γ_map {X Y : LocallyRingedSpaceᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.1.c.app (op ⊤) :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.Γ_map AlgebraicGeometry.LocallyRingedSpace.Γ_map
 
+set_option synthInstance.maxHeartbeats 30000 in
 theorem Γ_map_op {X Y : LocallyRingedSpace} (f : X ⟶ Y) : Γ.map f.op = f.1.c.app (op ⊤) :=
   rfl
 set_option linter.uppercaseLean3 false in