From 7077b721478060ae8c7dd73bb332fe296456c524 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Thu, 29 Dec 2022 11:25:42 +0000
Subject: [PATCH] feat: port `Order/ConditionallyCompleteLattice/Group` (#1253)

---
 Mathlib.lean                                  |  1 +
 .../ConditionallyCompleteLattice/Group.lean   | 64 +++++++++++++++++++
 2 files changed, 65 insertions(+)
 create mode 100644 Mathlib/Order/ConditionallyCompleteLattice/Group.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 53a2932bdb963..cc1f0482dff2a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -409,6 +409,7 @@ import Mathlib.Order.Compare
 import Mathlib.Order.CompleteBooleanAlgebra
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Order.Copy
 import Mathlib.Order.Cover
 import Mathlib.Order.Directed
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Group.lean b/Mathlib/Order/ConditionallyCompleteLattice/Group.lean
new file mode 100644
index 0000000000000..8642d01a7cbdc
--- /dev/null
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Group.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+Ported by: Anatole Dedecker
+
+! This file was ported from Lean 3 source module order.conditionally_complete_lattice.group
+! leanprover-community/mathlib commit 46a64b5b4268c594af770c44d9e502afc6a515cb
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Algebra.Order.Group.TypeTags
+
+/-!
+# Conditionally complete lattices and groups.
+
+-/
+
+
+section Group
+
+variable {α : Type _} {ι : Sort _} {ι' : Sort _} [Nonempty ι] [Nonempty ι']
+  [ConditionallyCompleteLattice α] [Group α]
+
+@[to_additive]
+theorem le_mul_cinfᵢ [CovariantClass α α (· * ·) (· ≤ ·)] {a : α} {g : α} {h : ι → α}
+    (H : ∀ j, a ≤ g * h j) : a ≤ g * infᵢ h :=
+  inv_mul_le_iff_le_mul.mp <| le_cinfᵢ fun _ => inv_mul_le_iff_le_mul.mpr <| H _
+#align le_mul_cinfi le_mul_cinfᵢ
+
+@[to_additive]
+theorem mul_csupᵢ_le [CovariantClass α α (· * ·) (· ≤ ·)] {a : α} {g : α} {h : ι → α}
+    (H : ∀ j, g * h j ≤ a) : g * supᵢ h ≤ a :=
+  @le_mul_cinfᵢ αᵒᵈ _ _ _ _ _ _ _ _ H
+#align mul_csupr_le mul_csupᵢ_le
+
+@[to_additive]
+theorem le_cinfᵢ_mul [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a : α} {g : ι → α}
+    {h : α} (H : ∀ i, a ≤ g i * h) : a ≤ infᵢ g * h :=
+  mul_inv_le_iff_le_mul.mp <| le_cinfᵢ fun _ => mul_inv_le_iff_le_mul.mpr <| H _
+#align le_cinfi_mul le_cinfᵢ_mul
+
+@[to_additive]
+theorem csupᵢ_mul_le [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a : α} {g : ι → α}
+    {h : α} (H : ∀ i, g i * h ≤ a) : supᵢ g * h ≤ a :=
+  @le_cinfᵢ_mul αᵒᵈ _ _ _ _ _ _ _ _ H
+#align csupr_mul_le csupᵢ_mul_le
+
+@[to_additive]
+theorem le_cinfᵢ_mul_cinfᵢ [CovariantClass α α (· * ·) (· ≤ ·)]
+    [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a : α} {g : ι → α} {h : ι' → α}
+    (H : ∀ i j, a ≤ g i * h j) : a ≤ infᵢ g * infᵢ h :=
+  le_cinfᵢ_mul fun _ => le_mul_cinfᵢ <| H _
+#align le_cinfi_mul_cinfi le_cinfᵢ_mul_cinfᵢ
+
+@[to_additive]
+theorem csupᵢ_mul_csupᵢ_le [CovariantClass α α (· * ·) (· ≤ ·)]
+    [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a : α} {g : ι → α} {h : ι' → α}
+    (H : ∀ i j, g i * h j ≤ a) : supᵢ g * supᵢ h ≤ a :=
+  csupᵢ_mul_le fun _ => mul_csupᵢ_le <| H _
+#align csupr_mul_csupr_le csupᵢ_mul_csupᵢ_le
+
+end Group