unsimp

Author: staroperator

Mathlib/Data/Finite/Defs.lean

@@ -215,9 +215,7 @@ theorem not_infinite {s : Set α} : ¬s.Infinite ↔ s.Finite :=
 
 alias ⟨_, Finite.not_infinite⟩ := not_infinite
 
-@[simp] lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
-
-attribute [simp] Finite.not_infinite
+lemma Infinite.not_finite {s : Set α} (hs : s.Infinite) : ¬ s.Finite := hs
 
 /-- See also `finite_or_infinite`, `fintypeOrInfinite`. -/
 protected theorem finite_or_infinite (s : Set α) : s.Finite ∨ s.Infinite :=

Mathlib/Data/Set/Countable.lean

@@ -339,9 +339,7 @@ theorem not_uncountable_iff_countable {s : Set α} : ¬s.Uncountable ↔ s.Count
 
 alias ⟨_, Countable.not_uncountable⟩ := not_uncountable_iff_countable
 
-@[simp] lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
-
-attribute [simp] Countable.not_uncountable
+lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
 
 theorem uncountable_coe_iff {s : Set α} : Uncountable s ↔ s.Uncountable :=
   not_countable_iff.symm.trans countable_coe_iff.not