chore(Data/Set/Card): adjust naming and simp set (#26791)

Renames:
- `Set.ncard_coe_Finset` -> `Set.ncard_coe_finset`
- `Set.Nat.card_coe_set_eq` -> `Nat.card_coe_set_eq`

Additionally, make the latter simp, so that `Nat.card` of a coerced set to type is no longer simp-normal, and make `ncard_univ` simp so that `Set.ncard univ` is no longer simp-normal.

The other simp changes in this PR are all for the simpNF linter, since a good chunk of simp lemmas are now provable.

Author: b-mehta

Mathlib/Algebra/Group/Pointwise/Set/Card.lean

@@ -44,17 +44,16 @@ variable [InvolutiveInv G]
 lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by
   rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]
 
-@[to_additive (attr := simp)]
-lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by
-  rw [← image_inv_eq_inv, Nat.card_image_of_injective inv_injective]
-
 @[to_additive (attr := simp)]
 lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by
   simp [← toENat_cardinalMk]
 
 @[to_additive (attr := simp)]
 lemma ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard := by simp [ncard]
 
+@[to_additive]
+lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by simp
+
 end InvolutiveInv
 
 section DivInvMonoid
@@ -79,16 +78,16 @@ variable [MulAction G α]
 lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s :=
   Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective a).injOn
 
-@[to_additive (attr := simp)]
-lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s :=
-  Nat.card_image_of_injective (MulAction.injective a) _
-
 @[to_additive (attr := simp)]
 lemma encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard := by
   simp [← toENat_cardinalMk]
 
 @[to_additive (attr := simp)]
 lemma ncard_smul_set (a : G) (s : Set α) : (a • s).ncard = s.ncard := by simp [ncard]
 
+@[to_additive]
+lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s := by
+  simp
+
 end Group
 end Set

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

@@ -240,15 +240,15 @@ abbrev oddComponents : Set G.ConnectedComponent := {c : G.ConnectedComponent | O
 lemma ConnectedComponent.odd_oddComponents_ncard_subset_supp [Finite V] {G'}
     (h : G ≤ G') (c' : ConnectedComponent G') :
     Odd {c ∈ G.oddComponents | c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard := by
-  simp_rw [← Set.Nat.card_coe_set_eq]
+  simp_rw [← Nat.card_coe_set_eq]
   classical
   cases nonempty_fintype V
   rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
   simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
   rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
   congr! 2
   ext c
-  simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_Finset, coe_filter,
+  simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
     mem_supp_iff, mem_univ, true_and, supp, and_comm]
 
 lemma odd_ncard_oddComponents [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Nat.card V) := by
@@ -259,8 +259,7 @@ lemma odd_ncard_oddComponents [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Na
     ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]
   rw [Finset.card_biUnion
     (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
-  simp_rw [Set.toFinset_card, ← Nat.card_eq_fintype_card, ← Finset.coe_filter_univ,
-    Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq]
+  simp_rw [← Set.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]
   exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm
 
 lemma ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -311,9 +311,8 @@ lemma odd_matches_node_outside [Finite V] {u : Set V}
   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, Set.toFinset_image, Nat.card_eq_fintype_card,
-    Set.toFinset_image,Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card,
-    ← Set.Nat.card_coe_set_eq] using hMmatch.even_card
+  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

Mathlib/Combinatorics/SimpleGraph/Tutte.lean

@@ -280,7 +280,7 @@ lemma exists_isTutteViolator (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching)
       Gmax.deleteUniversalVerts.coe.IsClique K.supp
   · -- Deleting universal vertices splits the graph into cliques
     rw [Fintype.card_eq_nat_card] at hc
-    simp_rw [Fintype.card_eq_nat_card, Set.Nat.card_coe_set_eq] at hc
+    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
     push_neg at hc
     obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
       (by simpa [IsTutteViolator] using hc) h'

Mathlib/Data/Set/Card.lean

@@ -503,22 +503,18 @@ theorem Finite.cast_ncard_eq (hs : s.Finite) : s.ncard = s.encard := by
 
 lemma ncard_le_encard (s : Set α) : s.ncard ≤ s.encard := ENat.coe_toNat_le_self _
 
-theorem Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard := by
-  obtain (h | h) := s.finite_or_infinite
-  · have := h.fintype
-    rw [ncard, h.encard_eq_coe_toFinset_card, Nat.card_eq_fintype_card,
-      toFinite_toFinset, toFinset_card, ENat.toNat_coe]
-  have := infinite_coe_iff.2 h
-  rw [ncard, h.encard_eq, Nat.card_eq_zero_of_infinite, ENat.toNat_top]
+@[simp] theorem _root_.Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard := rfl
+
+@[deprecated (since := "2025-07-05")] alias Nat.card_coe_set_eq := _root_.Nat.card_coe_set_eq
 
 theorem ncard_eq_toFinset_card (s : Set α) (hs : s.Finite := by toFinite_tac) :
     s.ncard = hs.toFinset.card := by
-  rw [← Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype,
+  rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype,
     @Finite.card_toFinset _ _ hs.fintype hs]
 
 theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] :
     s.ncard = s.toFinset.card := by
-  simp [← Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
+  simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
 
 lemma cast_ncard {s : Set α} (hs : s.Finite) :
     (s.ncard : Cardinal) = Cardinal.mk s := @Nat.cast_card _ hs
@@ -529,7 +525,7 @@ theorem encard_le_coe_iff_finite_ncard_le {k : ℕ} : s.encard ≤ k ↔ s.Finit
     fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩
 
 theorem Infinite.ncard (hs : s.Infinite) : s.ncard = 0 := by
-  rw [← Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]
+  rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]
 
 @[gcongr]
 theorem ncard_le_ncard (hst : s ⊆ t) (ht : t.Finite := by toFinite_tac) :
@@ -543,15 +539,12 @@ theorem ncard_mono [Finite α] : @Monotone (Set α) _ _ _ ncard := fun _ _ ↦ n
     s.ncard = 0 ↔ s = ∅ := by
   rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
 
-@[simp, norm_cast] theorem ncard_coe_Finset (s : Finset α) : (s : Set α).ncard = s.card := by
+@[simp, norm_cast] theorem ncard_coe_finset (s : Finset α) : (s : Set α).ncard = s.card := by
   rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]
 
-theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α := by
-  rcases finite_or_infinite α with h | h
-  · have hft := Fintype.ofFinite α
-    rw [ncard_eq_toFinset_card, Finite.toFinset_univ, Finset.card_univ, Nat.card_eq_fintype_card]
-  rw [Nat.card_eq_zero_of_infinite, Infinite.ncard]
-  exact infinite_univ
+@[deprecated (since := "2025-07-05")] alias ncard_coe_Finset := ncard_coe_finset
+
+@[simp] theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α := Nat.card_univ
 
 @[simp] theorem ncard_empty (α : Type*) : (∅ : Set α).ncard = 0 := by
   rw [ncard_eq_zero]
@@ -771,7 +764,7 @@ theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha
     obtain ⟨a, ha, rfl⟩ := h₃ y hy
     simp only [Subtype.exists]
     exact ⟨_, ha, rfl⟩
-  simp_rw [← Nat.card_coe_set_eq]
+  simp_rw [← _root_.Nat.card_coe_set_eq]
   exact Nat.card_congr (Equiv.ofBijective f' hbij)
 
 theorem ncard_le_ncard_of_injOn {t : Set β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : InjOn f s)
@@ -834,9 +827,8 @@ theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : 
       (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
       (by simpa) a₂ (by simpa) (by simpa)
 
-@[simp] theorem ncard_coe {α : Type*} (s : Set α) :
-    Set.ncard (Set.univ : Set (Set.Elem s)) = s.ncard :=
-  Set.ncard_congr (fun a ha ↦ ↑a) (fun a ha ↦ a.prop) (by simp) (by simp)
+theorem ncard_coe {α : Type*} (s : Set α) :
+    Set.ncard (Set.univ : Set (Set.Elem s)) = s.ncard := by simp
 
 @[simp] lemma ncard_graphOn (s : Set α) (f : α → β) : (s.graphOn f).ncard = s.ncard := by
   rw [← ncard_image_of_injOn fst_injOn_graph, image_fst_graphOn]
@@ -942,9 +934,7 @@ theorem eq_univ_iff_ncard [Finite α] (s : Set α) :
 
 lemma even_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) :
     Even sᶜ.ncard ↔ Even s.ncard := by
-  simp [compl_eq_univ_diff, ncard_diff (subset_univ _ : s ⊆ Set.univ),
-    Nat.even_sub (ncard_le_ncard (subset_univ _ : s ⊆ Set.univ)),
-    (ncard_univ _).symm ▸ heven]
+  rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]
 
 lemma odd_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) :
     Odd sᶜ.ncard ↔ Odd s.ncard := by

Mathlib/Data/Setoid/Partition/Card.lean

@@ -30,7 +30,7 @@ theorem Setoid.IsPartition.ncard_eq_finsum {α : Type*} {P : Set (Set α)}
     Nat.card_eq_card_finite_toFinset (hst t)
   suffices hs' : _ by
     rw [finsum_def, dif_pos hs']
-    simp only [← Set.Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]
+    simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]
     rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]
     rw [← Finset.card_sigma, eq_comm]
     apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)

Mathlib/FieldTheory/Finite/GaloisField.lean

@@ -250,7 +250,7 @@ theorem unitsMap_norm_surjective : Function.Surjective (Units.map <| Algebra.nor
     convert IsCyclic.card_pow_eq_one_le (α := K'ˣ) <| Nat.div_pos
       (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective) _) <|
       Nat.sub_pos_of_lt Finite.one_lt_card
-    rw [← Set.ncard_coe_Finset, ← SetLike.coe_sort_coe, Set.Nat.card_coe_set_eq]; congr; ext
+    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr; ext
     simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
 
 theorem norm_surjective : Function.Surjective (Algebra.norm K (S := K')) := fun k ↦ by

Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

@@ -511,7 +511,7 @@ theorem isMultiplyPretransitive {m n : ℕ} [Hn : IsMultiplyPretransitive G α n
   exists_smul_eq x y := by
     have : IsMultiplyPretransitive G α (s.ncard + m) := by rw [hmn]; infer_instance
     have Hs : Nonempty (Fin (s.ncard) ≃ s) :=
-      Finite.card_eq.mp (by simp [Set.Nat.card_coe_set_eq])
+      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
     set x' := ofFixingSubgroup.append x with hx
     set y' := ofFixingSubgroup.append y with hy
     obtain ⟨g, hg⟩ := exists_smul_eq G x' y'

Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean

@@ -444,7 +444,7 @@ noncomputable def ofFixingSubgroup.append
     {n : ℕ} [Finite s] (x : Fin n ↪ ofFixingSubgroup M s) :
     Fin (s.ncard + n) ↪ α := by
   have : Nonempty (Fin (s.ncard) ≃ s) :=
-    Finite.card_eq.mp (by simp [Set.Nat.card_coe_set_eq])
+    Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
   let y := (Classical.choice this).toEmbedding
   apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))
   rw [Set.disjoint_iff_forall_ne]
@@ -457,7 +457,7 @@ noncomputable def ofFixingSubgroup.append
 theorem ofFixingSubgroup.append_left {n : ℕ} [Finite s]
     (x : Fin n ↪ ofFixingSubgroup M s) (i : Fin s.ncard) :
     let Hs : Nonempty (Fin (s.ncard) ≃ s) :=
-      Finite.card_eq.mp (by simp [Set.Nat.card_coe_set_eq])
+      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
     ofFixingSubgroup.append x (Fin.castAdd n i) = (Classical.choice Hs) i := by
   simp [ofFixingSubgroup.append]
 

Mathlib/GroupTheory/Index.lean

@@ -699,7 +699,7 @@ variable (G : Type*) {X : Type*} [Group G] [MulAction G X] (x : X)
 @[to_additive] theorem index_stabilizer :
     (stabilizer G x).index = (orbit G x).ncard :=
   (Nat.card_congr (MulAction.orbitEquivQuotientStabilizer G x)).symm.trans
-    (Set.Nat.card_coe_set_eq (orbit G x))
+    (Nat.card_coe_set_eq (orbit G x))
 
 @[to_additive] theorem index_stabilizer_of_transitive [IsPretransitive G X] :
     (stabilizer G x).index = Nat.card X := by
@@ -713,7 +713,7 @@ namespace MonoidHom
 lemma surjective_of_card_ker_le_div {G M : Type*} [Group G] [Group M] [Finite G] [Finite M]
     (f : G →* M) (h : Nat.card f.ker ≤ Nat.card G / Nat.card M) : Function.Surjective f := by
   refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_
-  rw [Subgroup.coe_top, Set.ncard_univ, ← Set.Nat.card_coe_set_eq, SetLike.coe_sort_coe,
+  rw [Subgroup.coe_top, Set.ncard_univ, ← Nat.card_coe_set_eq, SetLike.coe_sort_coe,
     ← Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]
   exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos