Revert "unsimp"

This reverts commit b995b1f.

Author: staroperator

Mathlib/Data/Finite/Defs.lean

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

Mathlib/Data/Set/Countable.lean

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