From d9c6cd913475dc489e05717148d162e14bf9748b Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 23 Apr 2026 20:58:06 +0300
Subject: [PATCH 1/8] feat(Data/Set/Card): `Fintype.card s = s.ncard`

---
 Mathlib/Data/Set/Card.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 1ca79eb8302a1a..3deca6914a5bf6 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -599,6 +599,10 @@ theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] :
     s.ncard = s.toFinset.card := by
   simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
 
+variable (s) in
+theorem fintypeCard_eq_ncard [Fintype s] : Fintype.card s = s.ncard := by
+  rw [ncard_eq_toFinset_card', toFinset_card]
+
 lemma cast_ncard {s : Set α} (hs : s.Finite) :
     (s.ncard : Cardinal) = Cardinal.mk s := @Nat.cast_card _ hs
 

From 658c92ea05acd359d22b8a3a2d41c59ba9933c1e Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 28 Apr 2026 08:24:43 +0300
Subject: [PATCH 2/8] add `coe_ncard_eq_encard` and change `simp` tags

---
 Mathlib/Data/Set/Card.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 77e686dfe1345d..86eb9fb3207d09 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 α) :
@@ -603,9 +604,15 @@ 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]
 
+variable (s) in
+@[simp]
+theorem coe_ncard_eq_encard [Finite s] : s.ncard = s.encard :=
+  s.toFinite.cast_ncard_eq
+
 lemma cast_ncard {s : Set α} (hs : s.Finite) :
     (s.ncard : Cardinal) = Cardinal.mk s := @Nat.cast_card _ hs
 

From 2f75d2ea99a4ea2961d3752345daa032299d644f Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 28 Apr 2026 09:09:28 +0300
Subject: [PATCH 3/8] fix

---
 .../SimpleGraph/Connectivity/EdgeConnectivity.lean           | 4 ++--
 Mathlib/Combinatorics/SimpleGraph/Matching.lean              | 5 ++---
 Mathlib/GroupTheory/ClassEquation.lean                       | 3 +--
 Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean    | 2 +-
 4 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
index 90b571f8cb242b..f60cf2162d5902 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 <| by grind [Walk.nil_iff_length_eq, Walk.eq_of_length_eq_zero]
 
 lemma IsEdgeConnected.le_degree [Fintype (G.neighborSet u)] [Nontrivial V]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
index fe6bd569de4901..ea02b58bd1db7a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -311,9 +311,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/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
 

From d37ab42f7fde62e7e2844e955dea13d30735136c Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 04:20:33 +0300
Subject: [PATCH 4/8] untag some `simp`s to see what the damage is

---
 Mathlib/Combinatorics/SimpleGraph/Finite.lean   | 10 ++++------
 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |  3 +--
 Mathlib/Data/Fintype/Card.lean                  |  1 -
 Mathlib/Data/Set/Finite/Basic.lean              |  1 -
 Mathlib/Order/Interval/Finset/Defs.lean         | 11 +++++------
 5 files changed, 10 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index 0bd2fc936d8797..4c30da23e4b2e0 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
@@ -267,8 +266,7 @@ def incidenceFinset [DecidableEq V] : Finset (Sym2 V) :=
 @[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/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index 4ad99886d99d06..f0edb922df04bf 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/Finite/Basic.lean b/Mathlib/Data/Set/Finite/Basic.lean
index 9ab9a13a96d5d8..a7c92fdc666255 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/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]

From 9de8f533fc85bc227bf0b3b2e18d23892d24f9dc Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 05:58:59 +0300
Subject: [PATCH 5/8] fix `SimpleGraph/Copy.lean`

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 80ff36db037e4a..2a753b17ae4b88 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

From df37db9e62de41b1cfb587faedc14c3626912330 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 06:13:56 +0300
Subject: [PATCH 6/8] untag another simp lemma in `SimpleGraph/Finite`

---
 Mathlib/Combinatorics/SimpleGraph/Finite.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index 4c30da23e4b2e0..163ef903de60df 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -263,7 +263,6 @@ 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), card_neighborSet_eq_degree]

From 5f0ed72899144212dcec47cdd73677dfb8febb11 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 06:18:00 +0300
Subject: [PATCH 7/8] fix `SimpleGraph/IncMatrix`

---
 Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

From b27ad15f00a21c317c8c0237664a96e5c76d6788 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 30 Apr 2026 00:50:46 +0300
Subject: [PATCH 8/8] revert

---
 .../SimpleGraph/Connectivity/EdgeConnectivity.lean  |  4 ++--
 Mathlib/Combinatorics/SimpleGraph/Copy.lean         |  3 +--
 Mathlib/Combinatorics/SimpleGraph/Finite.lean       | 11 +++++++----
 Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean    |  2 +-
 Mathlib/Combinatorics/SimpleGraph/Matching.lean     |  5 +++--
 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean     |  3 ++-
 Mathlib/Data/Fintype/Card.lean                      |  1 +
 Mathlib/Data/Set/Card.lean                          | 13 +++++--------
 Mathlib/Data/Set/Finite/Basic.lean                  |  1 +
 Mathlib/GroupTheory/ClassEquation.lean              |  3 ++-
 .../Matrix/GeneralLinearGroup/Card.lean             |  2 +-
 Mathlib/Order/Interval/Finset/Defs.lean             | 11 ++++++-----
 12 files changed, 32 insertions(+), 27 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
index f60cf2162d5902..90b571f8cb242b 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
-  rw [← card_incidenceSet_eq_degree, ← ENat.coe_lt_coe, Set.coe_fintypeCard] at hh
-  obtain ⟨w, _⟩ := h hh |>.exists_isPath
+  obtain ⟨w, _⟩ :=
+    @h (G.incidenceSet u) (by simpa [← Set.coe_fintypeCard, ENat.coe_lt_coe]) |>.exists_isPath
   simpa using w.adj_snd <| by grind [Walk.nil_iff_length_eq, Walk.eq_of_length_eq_zero]
 
 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 2a753b17ae4b88..80ff36db037e4a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -313,8 +313,7 @@ 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 [card_neighborSet_eq_degree] using
-    Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective
+  simpa 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 163ef903de60df..0bd2fc936d8797 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -121,11 +121,12 @@ 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 [card_edgeSet]
+  simp
 
 variable [Fintype V]
 
@@ -202,6 +203,7 @@ 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
 
@@ -253,8 +255,7 @@ 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)),
-      card_neighborSet_eq_degree]
+    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
 
 instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
   Fintype.ofEquiv (G.neighborSet v) (G.incidenceSetEquivNeighborSet v).symm
@@ -263,9 +264,11 @@ 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), card_neighborSet_eq_degree]
+  rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v)]
+  simp
 
 @[simp, norm_cast]
 theorem coe_incidenceFinset [DecidableEq V] :
diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
index 46293d4e0079c5..7dce7be3752083 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, card_incidenceSet_eq_degree]
+  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]
 
 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 ea02b58bd1db7a..fe6bd569de4901 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -311,8 +311,9 @@ 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.ofFinite c.val.supp
-  simpa [Finset.card_image_of_injective] using hMmatch.even_card
+  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
 
 end Finite
 end ConnectedComponent
diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index f0edb922df04bf..4ad99886d99d06 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@@ -868,6 +868,7 @@ 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
@@ -879,7 +880,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, card_neighborSet_toSubgraph]
+  simp [Subgraph.degree]
 
 section MkProperties
 
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index 92b0c19123219c..acca9b0f9856a7 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -198,6 +198,7 @@ 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 86eb9fb3207d09..710db7d396e6bb 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -86,8 +86,7 @@ theorem toENat_cardinalMk_subtype (P : α → Prop) :
     (Cardinal.mk {x // P x}).toENat = {x | P x}.encard :=
   rfl
 
-variable (s) in
-theorem coe_fintypeCard [Fintype s] : Fintype.card s = s.encard := by
+@[simp] theorem coe_fintypeCard (s : Set α) [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 +589,10 @@ theorem ncard_def (s : Set α) : s.ncard = ENat.toNat s.encard := rfl
 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
+theorem coe_ncard_eq_encard [Finite s] : s.ncard = s.encard :=
+  s.toFinite.cast_ncard_eq
+
 lemma ncard_le_encard (s : Set α) : s.ncard ≤ s.encard := ENat.coe_toNat_le_self _
 
 @[simp] theorem _root_.Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard := rfl
@@ -604,15 +607,9 @@ 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]
 
-variable (s) in
-@[simp]
-theorem coe_ncard_eq_encard [Finite s] : s.ncard = s.encard :=
-  s.toFinite.cast_ncard_eq
-
 lemma cast_ncard {s : Set α} (hs : s.Finite) :
     (s.ncard : Cardinal) = Cardinal.mk s := @Nat.cast_card _ hs
 
diff --git a/Mathlib/Data/Set/Finite/Basic.lean b/Mathlib/Data/Set/Finite/Basic.lean
index a7c92fdc666255..9ab9a13a96d5d8 100644
--- a/Mathlib/Data/Set/Finite/Basic.lean
+++ b/Mathlib/Data/Set/Finite/Basic.lean
@@ -759,6 +759,7 @@ 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 7fc2f802ba769a..cde16a2e95a5de 100644
--- a/Mathlib/GroupTheory/ClassEquation.lean
+++ b/Mathlib/GroupTheory/ClassEquation.lean
@@ -42,7 +42,8 @@ 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
-  simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
+  rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
+  simp [Set.ncard_eq_toFinset_card']
 
 /-- 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 cb2b6a3bc39145..64ef4382b6bf6c 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), -Set.fintypeCard_eq_ncard]
+        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k)]
 
 end LinearIndependent
 
diff --git a/Mathlib/Order/Interval/Finset/Defs.lean b/Mathlib/Order/Interval/Finset/Defs.lean
index 6a0024141b5cd5..911b7a147d1a6b 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
 
-@[to_dual self]
+@[simp, 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)]
+@[to_dual (reorder := a b) (attr := simp)]
 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
 
-@[to_dual self]
+@[simp, 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]
+@[to_dual (attr := simp)]
 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]
+@[to_dual (attr := simp)]
 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,6 +437,7 @@ 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]