diff --git a/Mathlib/Algebra/BigOperators/Expect.lean b/Mathlib/Algebra/BigOperators/Expect.lean
index ed859ddca94e4..b64a24d549e6c 100644
--- a/Mathlib/Algebra/BigOperators/Expect.lean
+++ b/Mathlib/Algebra/BigOperators/Expect.lean
@@ -416,7 +416,7 @@ end AddCommMonoid
 section Semiring
 variable [Semiring M] [Module ℚ≥0 M]
 
-@[simp] lemma expect_one [Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1 := expect_const _
+lemma expect_one [Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1 := expect_const _
 
 end Semiring
 end Fintype
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index 1852e40e4fd39..0ff3b973f0141 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -93,7 +93,7 @@ theorem Nonempty.eq_univ [Subsingleton α] : s.Nonempty → s = univ := by
 theorem univ_nonempty_iff : (univ : Finset α).Nonempty ↔ Nonempty α := by
   rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]
 
-@[aesop unsafe apply (rule_sets := [finsetNonempty])]
+@[simp, aesop unsafe apply (rule_sets := [finsetNonempty])]
 theorem univ_nonempty [Nonempty α] : (univ : Finset α).Nonempty :=
   univ_nonempty_iff.2 ‹_›