feat: StarOrderedRing (α × β) (#18209)

The `Pi` version (for `Finite` indices) would be more work due to missing API around `Submonoid.pi`.

Mathlib.lean

@@ -710,6 +710,7 @@ import Mathlib.Algebra.Order.Ring.Unbundled.Rat
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.Algebra.Order.Star.Conjneg
+import Mathlib.Algebra.Order.Star.Prod
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1401,6 +1401,15 @@ theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
 theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥ := by
   simpa only [← Subgroup.toSubmonoid_eq] using Submonoid.prod_eq_bot_iff
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 /-- Product of subgroups is isomorphic to their product as groups. -/
 @[to_additive prodEquiv
       "Product of additive subgroups is isomorphic to their product

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -715,6 +715,15 @@ theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)}
       simpa using h2
     simpa using Submonoid.mul_mem _ h1' h2'
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 end Submonoid
 
 namespace MonoidHom

Mathlib/Algebra/Order/Star/Prod.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.Order.Star.Basic
+import Mathlib.Algebra.Star.Prod
+import Mathlib.Algebra.Ring.Prod
+
+/-!
+# Products of star-ordered rings
+-/
+
+variable {α β : Type*}
+
+open AddSubmonoid in
+instance Prod.instStarOrderedRing
+    [NonUnitalSemiring α] [NonUnitalSemiring β] [PartialOrder α] [PartialOrder β]
+    [StarRing α] [StarRing β] [StarOrderedRing α] [StarOrderedRing β] :
+    StarOrderedRing (α × β) where
+  le_iff := Prod.forall.2 fun xa xy => Prod.forall.2 fun ya yb => by
+    have :
+        closure (Set.range fun s : α × β ↦ star s * s) =
+          (closure <| Set.range fun s : α ↦ star s * s).prod
+          (closure <| Set.range fun s : β ↦ star s * s) := by
+      rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
+        Set.prod_range_range_eq]
+      simp_rw [Prod.mul_def, Prod.star_def]
+    simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this,
+      AddSubmonoid.mem_prod, exists_and_exists_comm, and_and_and_comm]

Mathlib/Logic/Basic.lean

@@ -485,6 +485,10 @@ theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x,
 theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
   ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩
 
+theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
+    (∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b :=
+  ⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩
+
 export Classical (not_forall)
 
 theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not