[Merged by Bors] - feat: port Algebra.Order.Pointwise

Mathlib/Algebra/Order/Pointwise.lean

@@ -9,7 +9,8 @@ Authors: Alex J. Best, Yaël Dillies
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Bounds
-import Mathlib.Data.Set.Pointwise.Smul
+import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Data.Set.Pointwise.SMul
 
 /-!
 # Pointwise operations on ordered algebraic objects
@@ -19,7 +20,7 @@ This file contains lemmas about the effect of pointwise operations on sets with
 ## TODO
 
 `Sup (s • t) = Sup s • Sup t` and `Inf (s • t) = Inf s • Inf t` hold as well but
-`covariant_class` is currently not polymorphic enough to state it.
+`CovariantClass` is currently not polymorphic enough to state it.
 -/
 
 
@@ -29,148 +30,161 @@ open Pointwise
 
 variable {α : Type _}
 
-section ConditionallyCompleteLattice
+-- Porting note : Swapped the place of `CompleteLattice` and `ConditionallyCompleteLattice`
+-- due to simpNF problem between `supₛ_xx` `csupₛ_xx`.
 
-variable [ConditionallyCompleteLattice α]
+section CompleteLattice
+
+variable [CompleteLattice α]
 
 section One
 
 variable [One α]
+@[to_additive (attr := simp)]
+theorem supₛ_one : supₛ (1 : Set α) = 1 :=
+  supₛ_singleton
+#align Sup_zero supₛ_zero
+#align Sup_one supₛ_one
 
-@[simp, to_additive]
-theorem cSup_one : supₛ (1 : Set α) = 1 :=
-  csupₛ_singleton _
-#align cSup_one cSup_one
-
-@[simp, to_additive]
-theorem cInf_one : infₛ (1 : Set α) = 1 :=
-  cinfₛ_singleton _
-#align cInf_one cInf_one
+@[to_additive (attr := simp)]
+theorem infₛ_one : infₛ (1 : Set α) = 1 :=
+  infₛ_singleton
+#align Inf_zero infₛ_zero
+#align Inf_one infₛ_one
 
 end One
 
 section Group
 
 variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
-  {s t : Set α}
+  (s t : Set α)
 
 @[to_additive]
-theorem cSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : supₛ s⁻¹ = (infₛ s)⁻¹ :=
-  by
-  rw [← image_inv]
-  exact ((OrderIso.inv α).map_cInf' hs₀ hs₁).symm
-#align cSup_inv cSup_inv
+theorem supₛ_inv (s : Set α) : supₛ s⁻¹ = (infₛ s)⁻¹ := by
+  rw [← image_inv, supₛ_image]
+  exact ((OrderIso.inv α).map_infₛ _).symm
+#align Sup_inv supₛ_inv
+#align Sup_neg supₛ_neg
 
 @[to_additive]
-theorem cInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : infₛ s⁻¹ = (supₛ s)⁻¹ :=
-  by
-  rw [← image_inv]
-  exact ((OrderIso.inv α).map_cSup' hs₀ hs₁).symm
-#align cInf_inv cInf_inv
+theorem infₛ_inv (s : Set α) : infₛ s⁻¹ = (supₛ s)⁻¹ := by
+  rw [← image_inv, infₛ_image]
+  exact ((OrderIso.inv α).map_supₛ _).symm
+#align Inf_inv infₛ_inv
+#align Inf_neg infₛ_neg
 
 @[to_additive]
-theorem cSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
-    supₛ (s * t) = supₛ s * supₛ t :=
-  csupₛ_image2_eq_csupₛ_csupₛ (fun _ => (OrderIso.mulRight _).to_galois_connection)
-    (fun _ => (OrderIso.mulLeft _).to_galois_connection) hs₀ hs₁ ht₀ ht₁
-#align cSup_mul cSup_mul
+theorem supₛ_mul : supₛ (s * t) = supₛ s * supₛ t :=
+  (supₛ_image2_eq_supₛ_supₛ fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).to_galoisConnection
+#align Sup_mul supₛ_mul
+#align Sup_add supₛ_add
 
 @[to_additive]
-theorem cInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
-    infₛ (s * t) = infₛ s * infₛ t :=
-  cinfₛ_image2_eq_cinfₛ_cinfₛ (fun _ => (OrderIso.mulRight _).symm.to_galois_connection)
-    (fun _ => (OrderIso.mulLeft _).symm.to_galois_connection) hs₀ hs₁ ht₀ ht₁
-#align cInf_mul cInf_mul
+theorem infₛ_mul : infₛ (s * t) = infₛ s * infₛ t :=
+  (infₛ_image2_eq_infₛ_infₛ fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).symm.to_galoisConnection
+#align Inf_mul infₛ_mul
+#align Inf_add infₛ_add
 
 @[to_additive]
-theorem cSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
-    supₛ (s / t) = supₛ s / infₛ t := by
-  rw [div_eq_mul_inv, cSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, cSup_inv ht₀ ht₁, div_eq_mul_inv]
-#align cSup_div cSup_div
+theorem supₛ_div : supₛ (s / t) = supₛ s / infₛ t := by simp_rw [div_eq_mul_inv, supₛ_mul, supₛ_inv]
+#align Sup_div supₛ_div
+#align Sup_sub supₛ_sub
 
 @[to_additive]
-theorem cInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
-    infₛ (s / t) = infₛ s / supₛ t := by
-  rw [div_eq_mul_inv, cInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, cInf_inv ht₀ ht₁, div_eq_mul_inv]
-#align cInf_div cInf_div
+theorem infₛ_div : infₛ (s / t) = infₛ s / supₛ t := by simp_rw [div_eq_mul_inv, infₛ_mul, infₛ_inv]
+#align Inf_div infₛ_div
+#align Inf_sub infₛ_sub
 
 end Group
 
-end ConditionallyCompleteLattice
+end CompleteLattice
 
-section CompleteLattice
+section ConditionallyCompleteLattice
 
-variable [CompleteLattice α]
+variable [ConditionallyCompleteLattice α]
 
 section One
 
 variable [One α]
 
-@[simp, to_additive]
-theorem Sup_one : supₛ (1 : Set α) = 1 :=
-  supₛ_singleton
-#align Sup_one Sup_one
+@[to_additive (attr := simp)]
+theorem csupₛ_one : supₛ (1 : Set α) = 1 :=
+  csupₛ_singleton _
+#align cSup_zero csupₛ_zero
+#align cSup_one csupₛ_one
 
-@[simp, to_additive]
-theorem Inf_one : infₛ (1 : Set α) = 1 :=
-  infₛ_singleton
-#align Inf_one Inf_one
+@[to_additive (attr := simp)]
+theorem cinfₛ_one : infₛ (1 : Set α) = 1 :=
+  cinfₛ_singleton _
+#align cInf_zero cinfₛ_zero
+#align cInf_one cinfₛ_one
 
 end One
 
 section Group
 
 variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
-  (s t : Set α)
+  {s t : Set α}
 
 @[to_additive]
-theorem Sup_inv (s : Set α) : supₛ s⁻¹ = (infₛ s)⁻¹ :=
-  by
-  rw [← image_inv, supₛ_image]
-  exact ((OrderIso.inv α).map_Inf _).symm
-#align Sup_inv Sup_inv
+theorem csupₛ_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : supₛ s⁻¹ = (infₛ s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv α).map_cinfₛ' hs₀ hs₁).symm
+#align cSup_inv csupₛ_inv
+#align cSup_neg csupₛ_neg
 
 @[to_additive]
-theorem Inf_inv (s : Set α) : infₛ s⁻¹ = (supₛ s)⁻¹ :=
-  by
-  rw [← image_inv, infₛ_image]
-  exact ((OrderIso.inv α).map_Sup _).symm
-#align Inf_inv Inf_inv
+theorem cinfₛ_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : infₛ s⁻¹ = (supₛ s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv α).map_csupₛ' hs₀ hs₁).symm
+#align cInf_inv cinfₛ_inv
+#align cInf_neg cinfₛ_neg
 
 @[to_additive]
-theorem Sup_mul : supₛ (s * t) = supₛ s * supₛ t :=
-  (supₛ_image2_eq_supₛ_supₛ fun _ => (OrderIso.mulRight _).to_galois_connection) fun _ =>
-    (OrderIso.mulLeft _).to_galois_connection
-#align Sup_mul Sup_mul
+theorem csupₛ_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    supₛ (s * t) = supₛ s * supₛ t :=
+  csupₛ_image2_eq_csupₛ_csupₛ (fun _ => (OrderIso.mulRight _).to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+#align cSup_mul csupₛ_mul
+#align cSup_add csupₛ_add
 
 @[to_additive]
-theorem Inf_mul : infₛ (s * t) = infₛ s * infₛ t :=
-  (infₛ_image2_eq_infₛ_infₛ fun _ => (OrderIso.mulRight _).symm.to_galois_connection) fun _ =>
-    (OrderIso.mulLeft _).symm.to_galois_connection
-#align Inf_mul Inf_mul
+theorem cinfₛ_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    infₛ (s * t) = infₛ s * infₛ t :=
+  cinfₛ_image2_eq_cinfₛ_cinfₛ (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+#align cInf_mul cinfₛ_mul
+#align cInf_add cinfₛ_add
 
 @[to_additive]
-theorem Sup_div : supₛ (s / t) = supₛ s / infₛ t := by simp_rw [div_eq_mul_inv, Sup_mul, Sup_inv]
-#align Sup_div Sup_div
+theorem csupₛ_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    supₛ (s / t) = supₛ s / infₛ t := by
+  rw [div_eq_mul_inv, csupₛ_mul hs₀ hs₁ ht₀.inv ht₁.inv, csupₛ_inv ht₀ ht₁, div_eq_mul_inv]
+#align cSup_div csupₛ_div
+#align cSup_sub csupₛ_sub
 
 @[to_additive]
-theorem Inf_div : infₛ (s / t) = infₛ s / supₛ t := by simp_rw [div_eq_mul_inv, Inf_mul, Inf_inv]
-#align Inf_div Inf_div
+theorem cinfₛ_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    infₛ (s / t) = infₛ s / supₛ t := by
+  rw [div_eq_mul_inv, cinfₛ_mul hs₀ hs₁ ht₀.inv ht₁.inv, cinfₛ_inv ht₀ ht₁, div_eq_mul_inv]
+#align cInf_div cinfₛ_div
+#align cInf_sub cinfₛ_sub
 
 end Group
 
-end CompleteLattice
+end ConditionallyCompleteLattice
 
 namespace LinearOrderedField
 
 variable {K : Type _} [LinearOrderedField K] {a b r : K} (hr : 0 < r)
 
 open Set
 
-include hr
+-- Porting note: Removing `include hr`
 
-theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) :=
-  by
+theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
   ext x
   simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
   constructor
@@ -184,8 +198,7 @@ theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) :=
     rw [mul_div_cancel' _ (ne_of_gt hr)]
 #align linear_ordered_field.smul_Ioo LinearOrderedField.smul_Ioo
 
-theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) :=
-  by
+theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
   ext x
   simp only [mem_smul_set, smul_eq_mul, mem_Icc]
   constructor
@@ -199,8 +212,7 @@ theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) :=
     rw [mul_div_cancel' _ (ne_of_gt hr)]
 #align linear_ordered_field.smul_Icc LinearOrderedField.smul_Icc
 
-theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) :=
-  by
+theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
   ext x
   simp only [mem_smul_set, smul_eq_mul, mem_Ico]
   constructor
@@ -214,8 +226,7 @@ theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) :=
     rw [mul_div_cancel' _ (ne_of_gt hr)]
 #align linear_ordered_field.smul_Ico LinearOrderedField.smul_Ico
 
-theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) :=
-  by
+theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
   ext x
   simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
   constructor
@@ -282,4 +293,3 @@ theorem smul_Iic : r • Iic a = Iic (r • a) := by
 #align linear_ordered_field.smul_Iic LinearOrderedField.smul_Iic
 
 end LinearOrderedField
-