diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
index e97f55dc75df1f..ea0f0f703ce16c 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
@@ -96,8 +96,8 @@ lemma IsEdgeReachable.le_degree [Fintype (G.neighborSet u)] (h : G.IsEdgeReachab
     (huv : u ≠ v) : k ≤ G.degree u := by
   classical
   by_contra! hh
-  obtain ⟨w, _⟩ :=
-    @h (G.incidenceSet u) (by simpa [← Set.coe_fintypeCard, ENat.coe_lt_coe]) |>.exists_isPath
+  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
+  obtain ⟨w, _⟩ := h hh |>.exists_isPath
   simpa using w.adj_snd <| mt Walk.Nil.eq huv
 
 lemma IsEdgeConnected.le_degree [Fintype (G.neighborSet u)] [Nontrivial V]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index f3662614ba254e..740e6bf42fcc09 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -313,7 +313,8 @@ alias ⟨IsContained.exists_iso_subgraph, IsContained.of_exists_iso_subgraph⟩
 
 theorem Copy.degree_le (f : Copy G H) (v : V) [Fintype <| G.neighborSet v]
     [Fintype <| H.neighborSet (f v)] : G.degree v ≤ H.degree (f v) := by
-  simpa using Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective
+  simpa [card_neighborSet_eq_degree] using
+    Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective
 
 theorem Copy.max_degree_le [Fintype V] [Fintype W] [DecidableRel G.Adj] [DecidableRel H.Adj]
     (f : Copy G H) : G.maxDegree ≤ H.maxDegree := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index e67cc079450575..995f4e087a421e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -121,12 +121,11 @@ lemma edgeFinset_nonempty : G.edgeFinset.Nonempty ↔ G ≠ ⊥ := by
 theorem edgeFinset_card : #G.edgeFinset = Fintype.card G.edgeSet :=
   Set.toFinset_card _
 
-@[simp]
 theorem card_edgeSet : Fintype.card G.edgeSet = #G.edgeFinset :=
   .symm <| Set.toFinset_card _
 
 theorem edgeSet_univ_card : #(univ : Finset G.edgeSet) = #G.edgeFinset := by
-  simp
+  simp [card_edgeSet]
 
 variable [Fintype V]
 
@@ -203,7 +202,6 @@ def degree : ℕ := #(G.neighborFinset v)
 @[simp]
 theorem card_neighborFinset_eq_degree : #(G.neighborFinset v) = G.degree v := rfl
 
-@[simp]
 theorem card_neighborSet_eq_degree : Fintype.card (G.neighborSet v) = G.degree v :=
   (Set.toFinset_card _).symm
 
@@ -255,7 +253,8 @@ theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] :
     Gᶜ.degree v = Fintype.card V - 1 - G.degree v := by
   classical
     rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
-    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
+    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
+      card_neighborSet_eq_degree]
 
 instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
   Fintype.ofEquiv (G.neighborSet v) (G.incidenceSetEquivNeighborSet v).symm
@@ -264,11 +263,9 @@ instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
 def incidenceFinset [DecidableEq V] : Finset (Sym2 V) :=
   (G.incidenceSet v).toFinset
 
-@[simp]
 theorem card_incidenceSet_eq_degree [DecidableEq V] :
     Fintype.card (G.incidenceSet v) = G.degree v := by
-  rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v)]
-  simp
+  rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v), card_neighborSet_eq_degree]
 
 @[simp, norm_cast]
 theorem coe_incidenceFinset [DecidableEq V] :
diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
index 7dce7be3752083..46293d4e0079c5 100644
--- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
@@ -106,7 +106,7 @@ variable [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e
 
 theorem sum_incMatrix_apply [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     ∑ e, G.incMatrix R a e = G.degree a := by
-  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]
+  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree]
 
 theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     (G.incMatrix R * (G.incMatrix R)ᵀ) a a = G.degree a := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
index 155e81cb76250d..c46984c916903b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -334,9 +334,8 @@ lemma odd_matches_node_outside [Finite V] {u : Set V}
   apply Nat.not_even_iff_odd.2 c.prop
   haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
   classical
-  haveI : Fintype (c.val.supp) := Fintype.ofFinite _
-  simpa [Subgraph.induce_verts, Subgraph.verts_top, Nat.card_eq_fintype_card, Set.toFinset_card,
-    Finset.card_image_of_injective, ← Nat.card_coe_set_eq] using hMmatch.even_card
+  haveI := Fintype.ofFinite c.val.supp
+  simpa [Finset.card_image_of_injective] using hMmatch.even_card
 
 end Finite
 end ConnectedComponent
diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index 0b71a3f1559e06..d40653ef36eb63 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@@ -868,7 +868,6 @@ lemma adj_iff_of_neighborSet_equiv {v : V} {H : Subgraph G}
 
 end Subgraph
 
-@[simp]
 theorem card_neighborSet_toSubgraph (G H : SimpleGraph V) (h : H ≤ G)
     (v : V) [Fintype ↑((toSubgraph H h).neighborSet v)] [Fintype ↑(H.neighborSet v)] :
     Fintype.card ↑((toSubgraph H h).neighborSet v) = H.degree v := by
@@ -880,7 +879,7 @@ theorem card_neighborSet_toSubgraph (G H : SimpleGraph V) (h : H ≤ G)
 lemma degree_toSubgraph (G H : SimpleGraph V) (h : H ≤ G) {v : V}
     [Fintype ↑((toSubgraph H h).neighborSet v)] [Fintype ↑(H.neighborSet v)] :
     (toSubgraph H h).degree v = H.degree v := by
-  simp [Subgraph.degree]
+  simp [Subgraph.degree, card_neighborSet_toSubgraph]
 
 section MkProperties
 
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index acca9b0f9856a7..92b0c19123219c 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -198,7 +198,6 @@ theorem Fintype.card_lex (α : Type*) [Fintype α] : Fintype.card (Lex α) = Fin
 
 -- Note: The extra hypothesis `h` is there so that the rewrite lemma applies,
 -- no matter what instance of `Fintype (Set.univ : Set α)` is used.
-@[simp]
 theorem Fintype.card_setUniv [Fintype α] {h : Fintype (Set.univ : Set α)} :
     Fintype.card (Set.univ : Set α) = Fintype.card α := by
   apply Fintype.card_of_finset'
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 59cc2f2713652b..b43cbc00827755 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -86,7 +86,8 @@ theorem toENat_cardinalMk_subtype (P : α → Prop) :
     (Cardinal.mk {x // P x}).toENat = {x | P x}.encard :=
   rfl
 
-@[simp] theorem coe_fintypeCard (s : Set α) [Fintype s] : Fintype.card s = s.encard := by
+variable (s) in
+theorem coe_fintypeCard [Fintype s] : Fintype.card s = s.encard := by
   simp [encard_eq_coe_toFinset_card]
 
 @[simp, norm_cast] theorem encard_coe_eq_coe_finsetCard (s : Finset α) :
@@ -590,6 +591,7 @@ theorem Finite.cast_ncard_eq (hs : s.Finite) : s.ncard = s.encard := by
   rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
 
 variable (s) in
+@[simp]
 theorem coe_ncard_eq_encard [Finite s] : s.ncard = s.encard :=
   s.toFinite.cast_ncard_eq
 
@@ -607,6 +609,7 @@ theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] :
   simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
 
 variable (s) in
+@[simp]
 theorem fintypeCard_eq_ncard [Fintype s] : Fintype.card s = s.ncard := by
   rw [ncard_eq_toFinset_card', toFinset_card]
 
diff --git a/Mathlib/Data/Set/Finite/Basic.lean b/Mathlib/Data/Set/Finite/Basic.lean
index f21ac811686ff5..22f7fe48edbf21 100644
--- a/Mathlib/Data/Set/Finite/Basic.lean
+++ b/Mathlib/Data/Set/Finite/Basic.lean
@@ -759,7 +759,6 @@ theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉
     @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by
   simp [Fintype.card_ofFinset]
 
-@[simp]
 theorem card_insert {a : α} (s : Set α) [Fintype s] (h : a ∉ s)
     {d : Fintype (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1 := by
   rw [← card_fintypeInsertOfNotMem s h]; congr!
diff --git a/Mathlib/GroupTheory/ClassEquation.lean b/Mathlib/GroupTheory/ClassEquation.lean
index cde16a2e95a5de..7fc2f802ba769a 100644
--- a/Mathlib/GroupTheory/ClassEquation.lean
+++ b/Mathlib/GroupTheory/ClassEquation.lean
@@ -42,8 +42,7 @@ theorem Group.sum_card_conj_classes_eq_card [Finite G] :
     ∑ᶠ x : ConjClasses G, x.carrier.ncard = Nat.card G := by
   classical
   cases nonempty_fintype G
-  rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
-  simp [Set.ncard_eq_toFinset_card']
+  simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
 
 /-- The **class equation** for finite groups. The cardinality of a group is equal to the size
 of its center plus the sum of the size of all its nontrivial conjugacy classes. -/
diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
index 64ef4382b6bf6c..cb2b6a3bc39145 100644
--- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
+++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
@@ -55,7 +55,7 @@ theorem card_linearIndependent {k : ℕ} (hk : k ≤ n) :
             simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
             rw [Module.card_eq_pow_finrank (K := K)]
       simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
-        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k)]
+        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k), -Set.fintypeCard_eq_ncard]
 
 end LinearIndependent
 
diff --git a/Mathlib/Order/Interval/Finset/Defs.lean b/Mathlib/Order/Interval/Finset/Defs.lean
index 911b7a147d1a6b..6a0024141b5cd5 100644
--- a/Mathlib/Order/Interval/Finset/Defs.lean
+++ b/Mathlib/Order/Interval/Finset/Defs.lean
@@ -330,17 +330,17 @@ theorem coe_Ico (a b : α) : (Ico a b : Set α) = Set.Ico a b :=
 theorem coe_Ioo (a b : α) : (Ioo a b : Set α) = Set.Ioo a b :=
   Set.ext fun _ => mem_Ioo
 
-@[simp, to_dual self]
+@[to_dual self]
 theorem _root_.Fintype.card_Icc (a b : α) [Fintype (Set.Icc a b)] :
     Fintype.card (Set.Icc a b) = #(Icc a b) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp
 
-@[to_dual (reorder := a b) (attr := simp)]
+@[to_dual (reorder := a b)]
 theorem _root_.Fintype.card_Ico (a b : α) [Fintype (Set.Ico a b)] :
     Fintype.card (Set.Ico a b) = #(Ico a b) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp
 
-@[simp, to_dual self]
+@[to_dual self]
 theorem _root_.Fintype.card_Ioo (a b : α) [Fintype (Set.Ioo a b)] :
     Fintype.card (Set.Ioo a b) = #(Ioo a b) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp
@@ -379,12 +379,12 @@ theorem coe_Ici (a : α) : (Ici a : Set α) = Set.Ici a :=
 theorem coe_Ioi (a : α) : (Ioi a : Set α) = Set.Ioi a :=
   Set.ext fun _ => mem_Ioi
 
-@[to_dual (attr := simp)]
+@[to_dual]
 theorem _root_.Fintype.card_Ici (a : α) [Fintype (Set.Ici a)] :
     Fintype.card (Set.Ici a) = #(Ici a) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp
 
-@[to_dual (attr := simp)]
+@[to_dual]
 theorem _root_.Fintype.card_Ioi (a : α) [Fintype (Set.Ioi a)] :
     Fintype.card (Set.Ioi a) = #(Ioi a) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp
@@ -437,7 +437,6 @@ theorem mem_uIcc : x ∈ uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b :=
 theorem coe_uIcc (a b : α) : (Finset.uIcc a b : Set α) = Set.uIcc a b :=
   coe_Icc _ _
 
-@[simp]
 theorem _root_.Fintype.card_uIcc (a b : α) [Fintype (Set.uIcc a b)] :
     Fintype.card (Set.uIcc a b) = #(uIcc a b) :=
   Fintype.card_of_finset' _ fun _ ↦ by simp [Set.uIcc]