[Merged by Bors] - feat: Ruzsa covering for sets

Mathlib/Combinatorics/Additive/RuzsaCovering.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Data.Finset.Pointwise
+import Mathlib.SetTheory.Cardinal.Finite
 
 #align_import combinatorics.additive.ruzsa_covering from "leanprover-community/mathlib"@"b363547b3113d350d053abdf2884e9850a56b205"
 
@@ -54,3 +55,23 @@ theorem exists_subset_mul_div (ht : t.Nonempty) :
 #align finset.exists_subset_add_sub Finset.exists_subset_add_sub
 
 end Finset
+
+namespace Set
+variable {α : Type*} [CommGroup α] {s t : Set α}
+
+/-- **Ruzsa's covering lemma** for sets. See also `Finset.exists_subset_mul_div`. -/
+@[to_additive "**Ruzsa's covering lemma**. Version for sets. For finsets,
+see `Finset.exists_subset_add_sub`."]
+lemma exists_subset_mul_div (hs : s.Finite) (ht' : t.Finite) (ht : t.Nonempty) :
+    ∃ u : Set α, Nat.card u * Nat.card t ≤ Nat.card (s * t) ∧ s ⊆ u * t / t ∧ u.Finite := by
+  lift s to Finset α using hs
+  lift t to Finset α using ht'
+  classical
+  obtain ⟨u, hu, hsut⟩ := Finset.exists_subset_mul_div s ht
+  refine ⟨u, ?_⟩
+  -- `norm_cast` would find these automatically, but breaks `to_additive` when it does so
+  rw [← Finset.coe_mul, ← Finset.coe_mul, ← Finset.coe_div]
+  norm_cast
+  simp [*]
+
+end Set

Mathlib/Data/Set/Card.lean

@@ -476,7 +476,7 @@ 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]
 
-@[simp] theorem Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard := by
+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,