chore: testing leanprover/lean4#4085 against nightly-testing

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/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

@@ -229,11 +229,6 @@ noncomputable def elementalStarAlgebra.characterSpaceToSpectrum (x : A)
       AlgHom.apply_mem_spectrum φ ⟨x, self_mem ℂ x⟩
 #align elemental_star_algebra.character_space_to_spectrum elementalStarAlgebra.characterSpaceToSpectrum
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12227
-attribute [nolint simpNF] elementalStarAlgebra.characterSpaceToSpectrum_coe
-
 theorem elementalStarAlgebra.continuous_characterSpaceToSpectrum (x : A) :
     Continuous (elementalStarAlgebra.characterSpaceToSpectrum x) :=
   continuous_induced_rng.2

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -94,10 +94,7 @@ theorem periodic_expMapCircle : Periodic expMapCircle (2 * π) := fun z =>
   expMapCircle_eq_expMapCircle.2 ⟨1, by rw [Int.cast_one, one_mul]⟩
 #align periodic_exp_map_circle periodic_expMapCircle
 
--- Adaptation note: nightly-2024-04-14
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12229
-@[simp, nolint simpNF]
+@[simp]
 theorem expMapCircle_two_pi : expMapCircle (2 * π) = 1 :=
   periodic_expMapCircle.eq.trans expMapCircle_zero
 #align exp_map_circle_two_pi expMapCircle_two_pi

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

@@ -228,10 +228,7 @@ theorem map_exp_comap_re_atBot : map exp (comap re atBot) = 𝓝[≠] 0 := by
   rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
 #align complex.map_exp_comap_re_at_bot Complex.map_exp_comap_re_atBot
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12226
-@[simp, nolint simpNF]
+@[simp]
 theorem map_exp_comap_re_atTop : map exp (comap re atTop) = cobounded ℂ := by
   rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]
   exact eventually_ne_cobounded _

Mathlib/Data/Complex/Basic.lean

@@ -691,10 +691,7 @@ theorem normSq_pos {z : ℂ} : 0 < normSq z ↔ z ≠ 0 :=
   (normSq_nonneg z).lt_iff_ne.trans <| not_congr (eq_comm.trans normSq_eq_zero)
 #align complex.norm_sq_pos Complex.normSq_pos
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12228
-@[simp, nolint simpNF]
+@[simp]
 theorem normSq_neg (z : ℂ) : normSq (-z) = normSq z := by simp [normSq]
 #align complex.norm_sq_neg Complex.normSq_neg
 

Mathlib/Data/Complex/Exponential.lean

@@ -1714,10 +1714,7 @@ end Mathlib.Meta.Positivity
 
 namespace Complex
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12230
-@[simp, nolint simpNF]
+@[simp]
 theorem abs_cos_add_sin_mul_I (x : ℝ) : abs (cos x + sin x * I) = 1 := by
   have := Real.sin_sq_add_cos_sq x
   simp_all [add_comm, abs, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]

Mathlib/Data/Matrix/Basic.lean

@@ -2332,10 +2332,7 @@ theorem conjTranspose_ratCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMo
   Matrix.ext <| by simp
 #align matrix.conj_transpose_rat_cast_smul Matrix.conjTranspose_ratCast_smul
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12231
-@[simp, nolint simpNF]
+@[simp]
 theorem conjTranspose_rat_smul [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
     (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
   Matrix.ext <| by simp

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

Mathlib/GroupTheory/Perm/Fin.lean

@@ -37,10 +37,7 @@ theorem Equiv.Perm.decomposeFin_symm_of_one {n : ℕ} (p : Fin (n + 1)) :
   Equiv.Perm.decomposeFin_symm_of_refl p
 #align equiv.perm.decompose_fin_symm_of_one Equiv.Perm.decomposeFin_symm_of_one
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12232
-@[simp, nolint simpNF]
+@[simp]
 theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
     Equiv.Perm.decomposeFin.symm (p, e) 0 = p := by simp [Equiv.Perm.decomposeFin]
 #align equiv.perm.decompose_fin_symm_apply_zero Equiv.Perm.decomposeFin_symm_apply_zero
@@ -57,10 +54,7 @@ theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : ℕ} (e : Perm (Fin n)) (p
         swap_apply_def, Ne.symm h]
 #align equiv.perm.decompose_fin_symm_apply_succ Equiv.Perm.decomposeFin_symm_apply_succ
 
--- Adaptation note: nightly-2024-04-01
--- The simpNF linter now times out on this lemma.
--- See https://github.com/leanprover-community/mathlib4/issues/12232
-@[simp, nolint simpNF]
+@[simp]
 theorem Equiv.Perm.decomposeFin_symm_apply_one {n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) :
     Equiv.Perm.decomposeFin.symm (p, e) 1 = swap 0 p (e 0).succ := by
   rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

lakefile.lean

@@ -21,7 +21,7 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing-2024-05-06"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.35"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-05-06
+leanprover/lean4-pr-releases:pr-release-4085