fix: not_prime_zero and not_prime_one Aesop rules (#22394)

These rules, which derive a contradiction from `Prime 0` or `Prime 1`, were tagged incorrectly and would therefore add `¬ Prime 0` and `¬ Prime 1` to every goal.

Fixes the heartbeat bump introduced in #22334.

Author: JLimperg

Mathlib/Data/Nat/Prime/Defs.lean

@@ -43,12 +43,24 @@ def Prime (p : ℕ) :=
 theorem irreducible_iff_nat_prime (a : ℕ) : Irreducible a ↔ Nat.Prime a :=
   Iff.rfl
 
-@[aesop safe destruct] theorem not_prime_zero : ¬Prime 0
+theorem not_prime_zero : ¬ Prime 0
   | h => h.ne_zero rfl
 
-@[aesop safe destruct] theorem not_prime_one : ¬Prime 1
+/-- A copy of `not_prime_zero` stated in a way that works for `aesop`.
+
+See https://github.com/leanprover-community/aesop/issues/197 for an explanation. -/
+@[aesop safe destruct] theorem prime_zero_false : Prime 0 → False :=
+  not_prime_zero
+
+theorem not_prime_one : ¬ Prime 1
   | h => h.ne_one rfl
 
+/-- A copy of `not_prime_one` stated in a way that works for `aesop`.
+
+See https://github.com/leanprover-community/aesop/issues/197 for an explanation. -/
+@[aesop safe destruct] theorem prime_one_false : Prime 1 → False :=
+  not_prime_one
+
 theorem Prime.ne_zero {n : ℕ} (h : Prime n) : n ≠ 0 :=
   Irreducible.ne_zero h
 

Mathlib/Probability/Kernel/Proper.lean

@@ -89,13 +89,6 @@ private lemma IsProper.lintegral_indicator_mul_indicator (hπ : IsProper π) (h
     Pi.one_apply, one_mul]
   rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_comm]
 
-#adaptation_note
-/--
-The `by measurability` argument of `lintegral_iSup` became slower after
-https://github.com/leanprover-community/aesop/pull/199 was merged,
-resulting in this declaration now requiring a larger `maxHeartbeats` limit.
--/
-set_option maxHeartbeats 400000 in
 set_option linter.style.multiGoal false in -- false positive
 /-- Auxiliary lemma for `IsProper.lintegral_mul` and
 `IsProper.setLIntegral_eq_indicator_mul_lintegral`. -/