feat(UniqueProds + NoZeroDivisors): AddMonoidAlgebra instances (#6723)

Add `UniqueProds/Sums` and `NoZeroDivisors` instances.

This has recently been prompted by the port of the [Lindemann-Weierstrass Theorem](https://leanprover.zulipchat.com/#narrow/stream/116395-maths), but the results are self-contained.  Instances such as the ones in this PR are the reasons why `UniqueProds/Sums` were introduced.

Affected files:
```
Algebra/
	Group/UniqueProds.lean
	MonoidAlgebra/NoZeroDivisors.lean
```




Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Group/UniqueProds.lean

@@ -3,7 +3,10 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
+import Mathlib.Data.DFinsupp.Basic
+import Mathlib.Data.Finset.Pointwise
 import Mathlib.Data.Finset.Preimage
+import Mathlib.Data.Finsupp.Defs
 
 #align_import algebra.group.unique_prods from "leanprover-community/mathlib"@"d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce"
 
@@ -45,7 +48,6 @@ about the grading type and then a generic statement of the form "look at the coe
 The file `Algebra/MonoidAlgebra/NoZeroDivisors` contains several examples of this use.
 -/
 
-
 /-- Let `G` be a Type with multiplication, let `A B : Finset G` be finite subsets and
 let `a0 b0 : G` be two elements.  `UniqueMul A B a0 b0` asserts `a0 * b0` can be written in at
 most one way as a product of an element of `A` and an element of `B`. -/
@@ -203,7 +205,7 @@ end Opposites
 end UniqueMul
 
 /-- Let `G` be a Type with addition.  `UniqueSums G` asserts that any two non-empty
-finite subsets of `A` have the `UniqueAdd` property, with respect to some element of their
+finite subsets of `G` have the `UniqueAdd` property, with respect to some element of their
 sum `A + B`. -/
 class UniqueSums (G) [Add G] : Prop where
 /-- For `A B` two nonempty finite sets, there always exist `a0 ∈ A, b0 ∈ B` such that
@@ -238,52 +240,138 @@ instance {M} [Mul M] [UniqueProds M] : UniqueSums (Additive M) where
 
 end Additive
 
--- see Note [lower instance priority]
-/-- This instance asserts that if `A` has a multiplication, a linear order, and multiplication
-is 'very monotone', then `A` also has `UniqueProds`. -/
-@[to_additive
-      "This instance asserts that if `A` has an addition, a linear order, and addition
-is 'very monotone', then `A` also has `UniqueSums`."]
-instance (priority := 100) Covariants.to_uniqueProds {A} [Mul A] [LinearOrder A]
-    [CovariantClass A A (· * ·) (· ≤ ·)] [CovariantClass A A (Function.swap (· * ·)) (· < ·)]
-    [ContravariantClass A A (· * ·) (· ≤ ·)] : UniqueProds A where
-  uniqueMul_of_nonempty {A B} hA hB :=
-    ⟨_, A.max'_mem ‹_›, _, B.max'_mem ‹_›, fun a b ha hb ↦
-      (mul_eq_mul_iff_eq_and_eq (Finset.le_max' _ _ ‹_›) (Finset.le_max' _ _ ‹_›)).mp⟩
-#align covariants.to_unique_prods Covariants.to_uniqueProds
-#align covariants.to_unique_sums Covariants.to_uniqueSums
+#noalign covariants.to_unique_prods
+#noalign covariants.to_unique_sums
 
 namespace UniqueProds
 
-@[to_additive (attr := nontriviality, simp)]
-theorem of_subsingleton {G : Type*} [Mul G] [Subsingleton G] : UniqueProds G where
-  uniqueMul_of_nonempty {A B} | ⟨a, hA⟩, ⟨b, hB⟩ => ⟨a, hA, b, hB, by simp⟩
+variable {G H : Type*} [Mul G] [Mul H]
 
 open Finset MulOpposite in
 @[to_additive]
-theorem of_mulOpposite (G : Type*) [Mul G] (h : UniqueProds Gᵐᵒᵖ) :
+theorem of_mulOpposite (h : @UniqueProds Gᵐᵒᵖ (MulOpposite.mul G)) :
     UniqueProds G :=
-  ⟨fun hA hB =>
-    let f : G ↪ Gᵐᵒᵖ := ⟨op, op_injective⟩
-    let ⟨y, yB, x, xA, hxy⟩ := h.uniqueMul_of_nonempty (hB.map (f := f)) (hA.map (f := f))
-    ⟨unop x, (mem_map' _).mp xA, unop y, (mem_map' _).mp yB, hxy.of_mulOpposite⟩⟩
+⟨fun hA hB =>
+  let f : G ↪ Gᵐᵒᵖ := ⟨op, op_injective⟩
+  let ⟨y, yB, x, xA, hxy⟩ := h.uniqueMul_of_nonempty (hB.map (f := f)) (hA.map (f := f))
+  ⟨unop x, (mem_map' _).mp xA, unop y, (mem_map' _).mp yB, hxy.of_mulOpposite⟩⟩
+
+-- see Note [lower instance priority]
+/-- This instance asserts that if `G` has a right-cancellative multiplication, a linear order,
+  and multiplication is strictly monotone w.r.t. the second argument, then `G` has `UniqueProds`. -/
+@[to_additive
+  "This instance asserts that if `G` has a right-cancellative addition, a linear order,
+  and addition is strictly monotone w.r.t. the second argument, then `G` has `UniqueSums`." ]
+instance (priority := 100) of_Covariant_right [IsRightCancelMul G]
+    [LinearOrder G] [CovariantClass G G (· * ·) (· < ·)] :
+    UniqueProds G where
+  uniqueMul_of_nonempty {A B} hA hB := by
+    obtain ⟨a0, b0, ha0, hb0, he⟩ := Finset.mem_mul.mp (Finset.max'_mem _ <| hA.mul hB)
+    refine ⟨a0, ha0, b0, hb0, fun a b ha hb he' => ?_⟩
+    obtain hl | rfl | hl := lt_trichotomy b b0
+    · refine ((he'.trans he ▸ mul_lt_mul_left' hl a).not_le <| Finset.le_max' _ (a * b0) ?_).elim
+      exact Finset.mem_mul.mpr ⟨a, b0, ha, hb0, rfl⟩
+    · exact ⟨mul_right_cancel he', rfl⟩
+    · refine ((he ▸ mul_lt_mul_left' hl a0).not_le <| Finset.le_max' _ (a0 * b) ?_).elim
+      exact Finset.mem_mul.mpr ⟨a0, b, ha0, hb, rfl⟩
 
 open MulOpposite in
-@[to_additive (attr := simp)]
-theorem iff_mulOpposite (G : Type*) [Mul G] :
-    UniqueProds Gᵐᵒᵖ ↔ UniqueProds G := by
-  refine ⟨of_mulOpposite G, fun h ↦ of_mulOpposite (Gᵐᵒᵖ) ⟨fun {A B} hA hB ↦ ?_⟩⟩
+-- see Note [lower instance priority]
+/-- This instance asserts that if `G` has a left-cancellative multiplication, a linear order,
+  and multiplication is strictly monotone w.r.t. the first argument, then `G` has `UniqueProds`. -/
+@[to_additive
+  "This instance asserts that if `G` has a left-cancellative addition, a linear order,
+  and addition is strictly monotone w.r.t. the first argument, then `G` has `UniqueSums`." ]
+instance (priority := 100) of_Covariant_left [IsLeftCancelMul G]
+    [LinearOrder G] [CovariantClass G G (Function.swap (· * ·)) (· < ·)] :
+    UniqueProds G :=
+let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective
+let _ : CovariantClass Gᵐᵒᵖ Gᵐᵒᵖ (· * ·) (· < ·) :=
+{ elim := fun _ _ _ bc =>
+          have : StrictMono (unop (α := G)) := fun _ _ => id
+          mul_lt_mul_right' (α := G) bc (unop _) }
+of_mulOpposite of_Covariant_right
+
+open Finset
+@[to_additive]
+theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f) (uG : UniqueProds G) :
+    UniqueProds H := by
+  refine ⟨fun {A B} A0 B0 => ?_⟩
   classical
-  let f : Gᵐᵒᵖᵐᵒᵖ ↪ G := ⟨_, unop_injective.comp unop_injective⟩
-  obtain ⟨a0, ha0, b0, hb0, d⟩ :=
-    h.uniqueMul_of_nonempty (Finset.Nonempty.map (f := f) hA) (Finset.Nonempty.map (f := f) hB)
-  simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Function.comp_apply] at ha0 hb0
-  rcases ha0 with ⟨a0, ha0, rfl⟩
-  rcases hb0 with ⟨b0, hb0, rfl⟩
-  refine ⟨a0, ha0, b0, hb0, ?_⟩
-  apply (UniqueMul.mulHom_map_iff (H := G) (⟨_, unop_injective.comp unop_injective⟩) ?_).mp
-  · simp only [Function.Embedding.coeFn_mk, Function.comp_apply]
-    convert d
-  · simp only [Function.Embedding.coeFn_mk, Function.comp_apply, unop_mul, implies_true]
+  obtain ⟨a0, ha0, b0, hb0, h⟩ := uG.uniqueMul_of_nonempty (A0.image f) (B0.image f)
+  rcases mem_image.mp ha0 with ⟨a', ha', rfl⟩
+  rcases mem_image.mp hb0 with ⟨b', hb', rfl⟩
+  exact ⟨a', ha', b', hb', (UniqueMul.mulHom_image_iff f hf).mp h⟩
+
+/-- `UniqueProd` is preserved under multiplicative equivalences. -/
+@[to_additive "`UniqueSums` is preserved under additive equivalences."]
+theorem mulHom_image_iff (f : G ≃* H) :
+    UniqueProds G ↔ UniqueProds H :=
+⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩
+
+@[to_additive] instance [UniqueProds G] [UniqueProds H] : UniqueProds (G × H) where
+  uniqueMul_of_nonempty {A B} hA hB := by
+    classical
+    obtain ⟨aG, hA, bG, hB, hG⟩ := uniqueMul_of_nonempty (hA.image Prod.fst) (hB.image Prod.fst)
+    rw [mem_image, ← filter_nonempty_iff] at hA hB
+    obtain ⟨aH, hA, bH, hB, hH⟩ := uniqueMul_of_nonempty (hA.image Prod.snd) (hB.image Prod.snd)
+    simp_rw [mem_image, mem_filter] at hA hB
+    refine ⟨(aG, aH), ?_, (bG, bH), ?_, fun a b ha hb he => ?_⟩
+    · obtain ⟨a, ⟨ha, rfl⟩, rfl⟩ := hA; exact ha
+    · obtain ⟨b, ⟨hb, rfl⟩, rfl⟩ := hB; exact hb
+    rw [Prod.ext_iff] at he
+    specialize hG (mem_image.mpr ⟨a, ha, rfl⟩) (mem_image.mpr ⟨b, hb, rfl⟩) he.1
+    specialize hH _ _ he.2
+    all_goals try simp_rw [mem_image, mem_filter]
+    exacts [⟨a, ⟨ha, hG.1⟩, rfl⟩, ⟨b, ⟨hb, hG.2⟩, rfl⟩, ⟨Prod.ext hG.1 hH.1, Prod.ext hG.2 hH.2⟩]
+
+@[to_additive] instance {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, UniqueProds (G i)] :
+    UniqueProds (∀ i, G i) where
+  uniqueMul_of_nonempty {A} := by
+    classical
+    let _ := Finset.isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
+    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
+    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
+    obtain hc | ⟨i, hc⟩ : (A.card ≤ 1 ∧ B.card ≤ 1) ∨
+      ∃ i, (∃ a1 ∈ A, ∃ a2 ∈ A, a1 i ≠ a2 i) ∨ (∃ b1 ∈ B, ∃ b2 ∈ B, b1 i ≠ b2 i)
+    · obtain hA1 | h1A := le_or_lt A.card 1
+      · obtain hB1 | h1B := le_or_lt B.card 1
+        · exact Or.inl ⟨hA1, hB1⟩
+        obtain ⟨b1, h1, b2, h2, hne⟩ := Finset.one_lt_card.mp h1B
+        obtain ⟨i, hne⟩ := Function.ne_iff.mp hne
+        exact Or.inr ⟨i, Or.inr ⟨b1, h1, b2, h2, hne⟩⟩
+      obtain ⟨a1, h1, a2, h2, hne⟩ := Finset.one_lt_card.mp h1A
+      obtain ⟨i, hne⟩ := Function.ne_iff.mp hne
+      exact Or.inr ⟨i, Or.inl ⟨a1, h1, a2, h2, hne⟩⟩
+    · obtain ⟨a0, ha0⟩ := hA; obtain ⟨b0, hb0⟩ := hB
+      simp_rw [Finset.card_le_one_iff] at hc
+      exact ⟨a0, ha0, b0, hb0, fun a b ha hb _ => ⟨hc.1 ha ha0, hc.2 hb hb0⟩⟩
+    obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))
+    rw [mem_image, ← filter_nonempty_iff] at hA hB
+    let A' := A.filter (· i = ai); let B' := B.filter (· i = bi)
+    obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0
+    · rcases hc with ⟨a1, h1, a2, h2, hne⟩ | ⟨b1, h1, b2, h2, hne⟩
+      · refine ihA _ ⟨A.filter_subset _, fun h => ?_⟩ hA hB
+        obtain rfl | hai := eq_or_ne (a1 i) ai
+        exacts [hne (mem_filter.mp <| h h2).2.symm, hai (mem_filter.mp <| h h1).2]
+      by_cases hA' : A' = A
+      · rw [hA']; refine ihB _ ⟨B.filter_subset _, fun h => ?_⟩ hB
+        obtain rfl | hbi := eq_or_ne (b1 i) bi
+        exacts [hne (mem_filter.mp <| h h2).2.symm, hbi (mem_filter.mp <| h h1).2]
+      exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
+    rw [mem_filter] at ha0 hb0
+    refine ⟨a0, ha0.1, b0, hb0.1, fun a b ha hb he => ?_⟩
+    specialize hi (mem_image_of_mem _ ha) (mem_image_of_mem _ hb) ?_
+    · refine (congr_arg (· i) he).trans ?_; rw [← ha0.2, ← hb0.2]; rfl
+    exact hu (mem_filter.mpr ⟨ha, hi.1⟩) (mem_filter.mpr ⟨hb, hi.2⟩) he
 
 end UniqueProds
+
+instance {ι} (G : ι → Type*) [∀ i, AddZeroClass (G i)] [∀ i, UniqueSums (G i)] :
+    UniqueSums (Π₀ i, G i) :=
+  UniqueSums.addHom_image_of_injective
+    DFinsupp.coeFnAddMonoidHom.toAddHom FunLike.coe_injective inferInstance
+
+instance {ι G} [AddZeroClass G] [UniqueSums G] : UniqueSums (ι →₀ G) :=
+  UniqueSums.addHom_image_of_injective
+    Finsupp.coeFnAddHom.toAddHom FunLike.coe_injective inferInstance