feat(Pointwise): cardinality of product set in GroupWithZero (#24578)

This PR:
* generalises the assumptions to `card_le_card_image₂_left` and `card_le_card_image₂_right` and golf these: they previously required injectivity everywhere despite using it in only one place. (These lemmas were also used in exactly one place each in mathlib)
* adds `card_le_card_mul_left_of_injective` and `card_le_card_mul_right_of_injective` which generalise the typeclass assumptions on the existing `card_le_card_mul_left` and `card_le_card_mul_right`
* uses the above to add versions of `card_le_card_mul_left` and `card_le_card_mul_right` in groups with zero. This is useful for applying the pointwise constructions to fields

In fact, the first versions of all the above lemmas were written in this generality, but that was seemingly lost during an upstream.

Author: b-mehta

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -489,6 +489,28 @@ lemma inf_mul_right {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f
     inf (s * t) f = inf t fun y ↦ inf s (f <| · * y) :=
   inf_image₂_right ..
 
+/--
+See `card_le_card_mul_left` for a more convenient but less general version for types with a
+left-cancellative multiplication.
+-/
+@[to_additive
+"See `card_le_card_add_left` for a more convenient but less general version for types with a
+left-cancellative addition."]
+lemma card_le_card_mul_left_of_injective (has : a ∈ s) (ha : Function.Injective (a * ·)) :
+    #t ≤ #(s * t) :=
+  card_le_card_image₂_left _ has ha
+
+/--
+See `card_le_card_mul_right` for a more convenient but less general version for types with a
+right-cancellative multiplication.
+-/
+@[to_additive
+"See `card_le_card_add_right` for a more convenient but less general version for types with a
+right-cancellative addition."]
+lemma card_le_card_mul_right_of_injective (hat : a ∈ t) (ha : Function.Injective (· * a)) :
+    #s ≤ #(s * t) :=
+  card_le_card_image₂_right _ hat ha
+
 end Mul
 
 /-! ### Finset subtraction/division -/
@@ -1154,7 +1176,7 @@ theorem singleton_mul_inter (a : α) (s t : Finset α) : {a} * (s ∩ t) = {a} *
 
 @[to_additive]
 theorem card_le_card_mul_left {s : Finset α} (hs : s.Nonempty) : #t ≤ #(s * t) :=
-  card_le_card_image₂_left _ hs mul_right_injective
+  have ⟨_, ha⟩ := hs; card_le_card_mul_left_of_injective ha (mul_right_injective _)
 
 /--
 The size of `s * s` is at least the size of `s`, version with left-cancellative multiplication.
@@ -1187,7 +1209,7 @@ theorem inter_mul_singleton (s t : Finset α) (a : α) : s ∩ t * {a} = s * {a}
 
 @[to_additive]
 theorem card_le_card_mul_right (ht : t.Nonempty) : #s ≤ #(s * t) :=
-  card_le_card_image₂_right _ ht mul_left_injective
+  have ⟨_, ha⟩ := ht; card_le_card_mul_right_of_injective ha (mul_left_injective _)
 
 /--
 The size of `s * s` is at least the size of `s`, version with right-cancellative multiplication.
@@ -1231,10 +1253,10 @@ section Group
 variable [Group α] [DecidableEq α] {s t : Finset α}
 
 @[to_additive] lemma card_le_card_div_left (hs : s.Nonempty) : #t ≤ #(s / t) :=
-  card_le_card_image₂_left _ hs fun _ ↦ div_right_injective
+  have ⟨_, ha⟩ := hs; card_le_card_image₂_left _ ha div_right_injective
 
 @[to_additive] lemma card_le_card_div_right (ht : t.Nonempty) : #s ≤ #(s / t) :=
-  card_le_card_image₂_right _ ht fun _ ↦ div_left_injective
+  have ⟨_, ha⟩ := ht; card_le_card_image₂_right _ ha div_left_injective
 
 @[to_additive] lemma card_le_card_div_self : #s ≤ #(s / s) := by
   cases s.eq_empty_or_nonempty <;> simp [card_le_card_div_left, *]

Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean

@@ -17,7 +17,27 @@ assert_not_exists MulAction Ring
 open scoped Pointwise
 
 namespace Finset
-variable {α β : Type*} [DecidableEq β]
+variable {α : Type*}
+
+section Mul
+
+variable [Mul α] [Zero α] [DecidableEq α] {s t : Finset α} {a : α}
+
+lemma card_le_card_mul_left₀ [IsLeftCancelMulZero α] (has : a ∈ s) (ha : a ≠ 0) : #t ≤ #(s * t) :=
+  card_le_card_mul_left_of_injective has (mul_right_injective₀ ha)
+
+lemma card_le_card_mul_right₀ [IsRightCancelMulZero α] (hat : a ∈ t) (ha : a ≠ 0) : #s ≤ #(s * t) :=
+  card_le_card_mul_right_of_injective hat (mul_left_injective₀ ha)
+
+lemma card_le_card_mul_self₀ [IsLeftCancelMulZero α] : #s ≤ #(s * s) := by
+  obtain hs | hs := (s.erase 0).eq_empty_or_nonempty
+  · rw [erase_eq_empty_iff] at hs
+    obtain rfl | rfl := hs <;> simp
+  obtain ⟨a, ha⟩ := hs
+  simp only [mem_erase, ne_eq] at ha
+  exact card_le_card_mul_left₀ ha.2 ha.1
+
+end Mul
 
 section MulZeroClass
 variable [DecidableEq α] [MulZeroClass α] {s : Finset α}

Mathlib/Data/Finset/NAry.lean

@@ -217,17 +217,13 @@ theorem image₂_inter_singleton [DecidableEq α] (s₁ s₂ : Finset α) (hf :
     image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b} := by
   simp_rw [image₂_singleton_right, image_inter _ _ hf]
 
-theorem card_le_card_image₂_left {s : Finset α} (hs : s.Nonempty) (hf : ∀ a, Injective (f a)) :
-    #t ≤ #(image₂ f s t) := by
-  obtain ⟨a, ha⟩ := hs
-  rw [← card_image₂_singleton_left _ (hf a)]
-  exact card_le_card (image₂_subset_right <| singleton_subset_iff.2 ha)
-
-theorem card_le_card_image₂_right {t : Finset β} (ht : t.Nonempty)
-    (hf : ∀ b, Injective fun a => f a b) : #s ≤ #(image₂ f s t) := by
-  obtain ⟨b, hb⟩ := ht
-  rw [← card_image₂_singleton_right _ (hf b)]
-  exact card_le_card (image₂_subset_left <| singleton_subset_iff.2 hb)
+theorem card_le_card_image₂_left {s : Finset α} (ha : a ∈ s) (hf : Injective (f a)) :
+    #t ≤ #(image₂ f s t) :=
+  card_le_card_of_injOn (f a) (fun _ hb ↦ mem_image₂_of_mem ha hb) hf.injOn
+
+theorem card_le_card_image₂_right {t : Finset β} (hb : b ∈ t) (hf : Injective (f · b)) :
+    #s ≤ #(image₂ f s t) :=
+  card_le_card_of_injOn (f · b) (fun _ ha ↦ mem_image₂_of_mem ha hb) hf.injOn
 
 variable {s t}