[Merged by Bors] - feat: When s ×ˢ t is finite

Mathlib/Data/Set/Finite.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 
 ! This file was ported from Lean 3 source module data.set.finite
-! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
+! leanprover-community/mathlib commit c941bb9426d62e266612b6d99e6c9fc93e7a1d07
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -138,11 +138,20 @@ theorem not_infinite {s : Set α} : ¬s.Infinite ↔ s.Finite :=
   not_not
 #align set.not_infinite Set.not_infinite
 
+alias not_infinite ↔ _ Finite.not_infinite
+#align set.finite.not_infinite Set.Finite.not_infinite
+
+attribute [simp] Finite.not_infinite
+
 /-- See also `finite_or_infinite`, `fintype_or_infinite`. -/
 protected theorem finite_or_infinite (s : Set α) : s.Finite ∨ s.Infinite :=
   em _
 #align set.finite_or_infinite Set.finite_or_infinite
 
+protected theorem infinite_or_finite (s : Set α) : s.Infinite ∨ s.Finite :=
+  em' _
+#align set.infinite_or_finite Set.infinite_or_finite
+
 /-! ### Basic properties of `Set.Finite.toFinset` -/
 
 
@@ -803,6 +812,12 @@ theorem finite_empty : (∅ : Set α).Finite :=
   toFinite _
 #align set.finite_empty Set.finite_empty
 
+protected theorem Infinite.nonempty {s : Set α} (h : s.Infinite) : s.Nonempty :=
+  nonempty_iff_ne_empty.2 $ by
+    rintro rfl
+    exact h finite_empty
+#align set.infinite.nonempty Set.Infinite.nonempty
+
 @[simp]
 theorem finite_singleton (a : α) : ({a} : Set α).Finite :=
   toFinite _
@@ -874,26 +889,62 @@ theorem finite_le_nat (n : ℕ) : Set.Finite { i | i ≤ n } :=
   toFinite _
 #align set.finite_le_nat Set.finite_le_nat
 
-theorem Finite.prod {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
-    (s ×ˢ t : Set (α × β)).Finite := by
+section Prod
+
+variable {s : Set α} {t : Set β}
+
+protected theorem Finite.prod (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t : Set (α × β)).Finite := by
   cases hs
   cases ht
   apply toFinite
 #align set.finite.prod Set.Finite.prod
 
-theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite := by
+theorem Finite.of_prod_left (h : (s ×ˢ t : Set (α × β)).Finite) : t.Nonempty → s.Finite :=
+  fun ⟨b, hb⟩ => (h.image Prod.fst).subset fun a ha => ⟨(a, b), ⟨ha, hb⟩, rfl⟩
+#align set.finite.of_prod_left Set.Finite.of_prod_left
+
+theorem Finite.of_prod_right (h : (s ×ˢ t : Set (α × β)).Finite) : s.Nonempty → t.Finite :=
+  fun ⟨a, ha⟩ => (h.image Prod.snd).subset fun b hb => ⟨(a, b), ⟨ha, hb⟩, rfl⟩
+#align set.finite.of_prod_right Set.Finite.of_prod_right
+
+protected theorem Infinite.prod_left (hs : s.Infinite) (ht : t.Nonempty) : (s ×ˢ t).Infinite :=
+  fun h => hs <| h.of_prod_left ht
+#align set.infinite.prod_left Set.Infinite.prod_left
+
+protected theorem Infinite.prod_right (ht : t.Infinite) (hs : s.Nonempty) : (s ×ˢ t).Infinite :=
+  fun h => ht <| h.of_prod_right hs
+#align set.infinite.prod_right Set.Infinite.prod_right
+
+protected theorem infinite_prod :
+    (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty := by
+  refine' ⟨fun h => _, _⟩
+  · simp_rw [Set.Infinite, @and_comm ¬_, ← not_imp]
+    by_contra'
+    exact h ((this.1 h.nonempty.snd).prod $ this.2 h.nonempty.fst)
+  · rintro (h | h)
+    · exact h.1.prod_left h.2
+    · exact h.1.prod_right h.2
+#align set.infinite_prod Set.infinite_prod
+
+theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) := by
+  simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]
+#align set.finite_prod Set.finite_prod
+
+protected theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite := by
   classical
     cases hs
     apply Set.toFinite
 #align set.finite.off_diag Set.Finite.offDiag
 
-theorem Finite.image2 (f : α → β → γ) {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
+protected theorem Finite.image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) :
     (image2 f s t).Finite := by
   cases hs
   cases ht
   apply toFinite
 #align set.finite.image2 Set.Finite.image2
 
+end Prod
+
 theorem Finite.seq {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
     (f.seq s).Finite := by
   classical
@@ -1231,11 +1282,6 @@ theorem Infinite.exists_subset_card_eq {s : Set α} (hs : s.Infinite) (n : ℕ)
   ⟨((Finset.range n).map (hs.natEmbedding _)).map (Embedding.subtype _), by simp⟩
 #align set.infinite.exists_subset_card_eq Set.Infinite.exists_subset_card_eq
 
-theorem Infinite.nonempty {s : Set α} (h : s.Infinite) : s.Nonempty :=
-  let a := Infinite.natEmbedding s h 37
-  ⟨a.1, a.2⟩
-#align set.infinite.nonempty Set.Infinite.nonempty
-
 theorem infinite_of_finite_compl [Infinite α] {s : Set α} (hs : sᶜ.Finite) : s.Infinite := fun h =>
   Set.infinite_univ (by simpa using hs.union h)
 #align set.infinite_of_finite_compl Set.infinite_of_finite_compl
@@ -1257,15 +1303,47 @@ theorem infinite_union {s t : Set α} : (s ∪ t).Infinite ↔ s.Infinite ∨ t.
   simp only [Set.Infinite, finite_union, not_and_or]
 #align set.infinite_union Set.infinite_union
 
-theorem infinite_of_infinite_image (f : α → β) {s : Set α} (hs : (f '' s).Infinite) : s.Infinite :=
+theorem Infinite.of_image (f : α → β) {s : Set α} (hs : (f '' s).Infinite) : s.Infinite :=
   mt (Finite.image f) hs
-#align set.infinite_of_infinite_image Set.infinite_of_infinite_image
+#align set.infinite.of_image Set.Infinite.of_image
 
 theorem infinite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) :
     (f '' s).Infinite ↔ s.Infinite :=
   not_congr <| finite_image_iff hi
 #align set.infinite_image_iff Set.infinite_image_iff
 
+alias infinite_image_iff ↔ _ Infinite.image
+#align set.infinite.image Set.Infinite.image
+
+-- Porting note: attribute [protected] doesn't work
+-- attribute [protected] infinite.image
+
+section Image2
+
+variable {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}
+
+protected theorem Infinite.image2_left (hs : s.Infinite) (hb : b ∈ t)
+    (hf : InjOn (fun a => f a b) s) : (image2 f s t).Infinite :=
+  (hs.image hf).mono <| image_subset_image2_left hb
+#align set.infinite.image2_left Set.Infinite.image2_left
+
+protected theorem Infinite.image2_right (ht : t.Infinite) (ha : a ∈ s) (hf : InjOn (f a) t) :
+    (image2 f s t).Infinite :=
+  (ht.image hf).mono <| image_subset_image2_right ha
+#align set.infinite.image2_right Set.Infinite.image2_right
+
+theorem infinite_image2 (hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
+    (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty := by
+  refine' ⟨fun h => Set.infinite_prod.1 _, _⟩
+  · rw [← image_uncurry_prod] at h
+    exact h.of_image _
+  · rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
+    · exact hs.image2_left hb (hfs _ hb)
+    · exact ht.image2_right ha (hft _ ha)
+#align set.infinite_image2 Set.infinite_image2
+
+end Image2
+
 theorem infinite_of_injOn_mapsTo {s : Set α} {t : Set β} {f : α → β} (hi : InjOn f s)
     (hm : MapsTo f s t) (hs : s.Infinite) : t.Infinite :=
   ((infinite_image_iff hi).2 hs).mono (mapsTo'.mp hm)

Mathlib/Data/Set/Pointwise/Finite.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Floris van Doorn
 
 ! This file was ported from Lean 3 source module data.set.pointwise.finite
-! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
+! leanprover-community/mathlib commit c941bb9426d62e266612b6d99e6c9fc93e7a1d07
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -109,6 +109,12 @@ theorem Finite.smul_set : s.Finite → (a • s).Finite :=
 #align set.finite.smul_set Set.Finite.smul_set
 #align set.finite.vadd_set Set.Finite.vadd_set
 
+@[to_additive]
+theorem Infinite.of_smul_set : (a • s).Infinite → s.Infinite :=
+  Infinite.of_image _
+#align set.infinite.of_smul_set Set.Infinite.of_smul_set
+#align set.infinite.of_vadd_set Set.Infinite.of_vadd_set
+
 end HasSmulSet
 
 section Vsub
@@ -121,6 +127,45 @@ theorem Finite.vsub (hs : s.Finite) (ht : t.Finite) : Set.Finite (s -ᵥ t) :=
 
 end Vsub
 
+section Cancel
+
+variable [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α}
+
+@[to_additive]
+theorem infinite_mul : (s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty :=
+  infinite_image2 (fun _ _ => (mul_left_injective _).injOn _) fun _ _ =>
+    (mul_right_injective _).injOn _
+#align set.infinite_mul Set.infinite_mul
+#align set.infinite_add Set.infinite_add
+
+end Cancel
+
+section Group
+
+variable [Group α] [MulAction α β] {a : α} {s : Set β}
+
+@[to_additive (attr := simp)]
+theorem finite_smul_set : (a • s).Finite ↔ s.Finite :=
+  finite_image_iff <| (MulAction.injective _).injOn _
+#align set.finite_smul_set Set.finite_smul_set
+#align set.finite_vadd_set Set.finite_vadd_set
+
+@[to_additive (attr := simp)]
+theorem infinite_smul_set : (a • s).Infinite ↔ s.Infinite :=
+  infinite_image_iff <| (MulAction.injective _).injOn _
+#align set.infinite_smul_set Set.infinite_smul_set
+#align set.infinite_vadd_set Set.infinite_vadd_set
+
+alias finite_smul_set ↔ Finite.of_smul_set _
+#align set.finite.of_smul_set Set.Finite.of_smul_set
+
+alias infinite_smul_set ↔ _ Infinite.smul_set
+#align set.infinite.smul_set Set.Infinite.smul_set
+
+attribute [to_additive] Finite.of_smul_set Infinite.smul_set
+
+end Group
+
 end Set
 
 open Set