diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index c1cfd9ca699ef..c9ece6f547994 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -107,6 +107,9 @@ lemma norm_fourierSMulRight_le (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (
   _ ≤ (2 * π) * (‖L‖ * ‖v‖) * ‖f v‖ := by gcongr; exact L.le_opNorm _
   _ = 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ := by ring
 
+-- Adaptation note: nightly-2024-04-01
+-- This maxHeartbeats was not needed previously.
+set_option maxHeartbeats 400000 in
 lemma _root_.MeasureTheory.AEStronglyMeasurable.fourierSMulRight
     [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] [MeasurableSpace V] [BorelSpace V]
     {L : V →L[ℝ] W →L[ℝ] ℝ} {f : V → E} {μ : Measure V}
diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean
index 9ef775fe51976..93b5d29d462c5 100644
--- a/Mathlib/Probability/Kernel/MeasureCompProd.lean
+++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean
@@ -69,6 +69,9 @@ lemma ae_compProd_of_ae_ae [SFinite μ] [IsSFiniteKernel κ] {p : α × β → P
     ∀ᵐ x ∂(μ ⊗ₘ κ), p x :=
   kernel.ae_compProd_of_ae_ae hp h
 
+-- Adaptation note: nightly-2024-04-01
+-- This maxHeartbeats was not needed previously.
+set_option maxHeartbeats 400000 in
 lemma ae_ae_of_ae_compProd [SFinite μ] [IsSFiniteKernel κ] {p : α × β → Prop}
     (h : ∀ᵐ x ∂(μ ⊗ₘ κ), p x) :
     ∀ᵐ a ∂μ, ∀ᵐ b ∂(κ a), p (a, b) :=