From 97eac6059001f9f0d759e77b758b9dfe459cb633 Mon Sep 17 00:00:00 2001
From: Reid Barton <rwbarton@gmail.com>
Date: Fri, 13 Jan 2023 13:10:21 +0100
Subject: [PATCH] fix: add missing to_additive aligns in Mathlib.Algebra.Bounds

Also fix 1 name.
---
 Mathlib/Algebra/Bounds.lean | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Bounds.lean b/Mathlib/Algebra/Bounds.lean
index 126c2a0602b10..32abd12953d5d 100644
--- a/Mathlib/Algebra/Bounds.lean
+++ b/Mathlib/Algebra/Bounds.lean
@@ -35,51 +35,61 @@ variable {G : Type _} [Group G] [Preorder G] [CovariantClass G G (· * ·) (· 
 theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s :=
   (OrderIso.inv G).bddAbove_preimage
 #align bdd_above_inv bddAbove_inv
+#align bdd_above_neg bddAbove_neg
 
 @[to_additive (attr := simp)]
 theorem bddBelow_inv : BddBelow s⁻¹ ↔ BddAbove s :=
   (OrderIso.inv G).bddBelow_preimage
 #align bdd_below_inv bddBelow_inv
+#align bdd_below_neg bddBelow_neg
 
 @[to_additive]
 theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ :=
   bddBelow_inv.2 h
 #align bdd_above.inv BddAbove.inv
+#align bdd_above.neg BddAbove.neg
 
 @[to_additive]
 theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ :=
   bddAbove_inv.2 h
 #align bdd_below.inv BddBelow.inv
+#align bdd_below.neg BddBelow.neg
 
 @[to_additive (attr := simp)]
 theorem isLUB_inv : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹ :=
   (OrderIso.inv G).isLUB_preimage
 #align is_lub_inv isLUB_inv
+#align is_lub_neg isLUB_neg
 
 @[to_additive]
 theorem isLUB_inv' : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a :=
   (OrderIso.inv G).isLUB_preimage'
 #align is_lub_inv' isLUB_inv'
+#align is_lub_neg' isLUB_neg'
 
 @[to_additive]
 theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ :=
   isLUB_inv'.2 h
 #align is_glb.inv IsGLB.inv
+#align is_glb.neg IsGLB.neg
 
 @[to_additive (attr := simp)]
 theorem isGLB_inv : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹ :=
   (OrderIso.inv G).isGLB_preimage
 #align is_glb_inv isGLB_inv
+#align is_glb_neg isGLB_neg
 
 @[to_additive]
 theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a :=
   (OrderIso.inv G).isGLB_preimage'
 #align is_glb_inv' isGLB_inv'
+#align is_glb_neg' isGLB_neg'
 
 @[to_additive]
 theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
   isGLB_inv'.2 h
 #align is_lub.inv IsLUB.inv
+#align is_lub.neg IsLUB.neg
 
 end InvNeg
 
@@ -93,34 +103,40 @@ theorem mul_mem_upperBounds_mul {s t : Set M} {a b : M} (ha : a ∈ upperBounds
     (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t) :=
   forall_image2_iff.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)
 #align mul_mem_upper_bounds_mul mul_mem_upperBounds_mul
+#align add_mem_upper_bounds_add add_mem_upperBounds_add
 
 @[to_additive]
 theorem subset_upperBounds_mul (s t : Set M) :
     upperBounds s * upperBounds t ⊆ upperBounds (s * t) :=
   image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy
 #align subset_upper_bounds_mul subset_upperBounds_mul
+#align subset_upper_bounds_add subset_upperBounds_add
 
 @[to_additive]
 theorem mul_mem_lowerBounds_mul {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s)
     (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t) :=
   @mul_mem_upperBounds_mul Mᵒᵈ _ _ _ _ _ _ _ _ ha hb
 #align mul_mem_lower_bounds_mul mul_mem_lowerBounds_mul
+#align add_mem_lower_bounds_add add_mem_lowerBounds_add
 
 @[to_additive]
 theorem subset_lowerBounds_mul (s t : Set M) :
     lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) :=
   @subset_upperBounds_mul Mᵒᵈ _ _ _ _ _ _
 #align subset_lower_bounds_mul subset_lowerBounds_mul
+#align subset_lower_bounds_add subset_lowerBounds_add
 
 @[to_additive]
 theorem BddAbove.mul {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
   (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t)
 #align bdd_above.mul BddAbove.mul
+#align bdd_above.add BddAbove.add
 
 @[to_additive]
 theorem BddBelow.mul {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
   (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
 #align bdd_below.mul BddBelow.mul
+#align bdd_below.add BddBelow.add
 
 end mul_add
 
@@ -135,11 +151,13 @@ variable {ι G : Type _} [Group G] [ConditionallyCompleteLattice G]
 theorem csupᵢ_mul (hf : BddAbove (Set.range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
   (OrderIso.mulRight a).map_csupᵢ hf
 #align csupr_mul csupᵢ_mul
+#align csupr_add csupᵢ_add
 
 @[to_additive]
-theorem csupr_div (hf : BddAbove (Set.range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
+theorem csupᵢ_div (hf : BddAbove (Set.range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
   simp only [div_eq_mul_inv, csupᵢ_mul hf]
-#align csupr_div csupr_div
+#align csupr_div csupᵢ_div
+#align csupr_sub csupᵢ_sub
 
 end Right
 
@@ -152,6 +170,7 @@ variable {ι G : Type _} [Group G] [ConditionallyCompleteLattice G]
 theorem mul_csupᵢ (hf : BddAbove (Set.range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
   (OrderIso.mulLeft a).map_csupᵢ hf
 #align mul_csupr mul_csupᵢ
+#align add_csupr add_csupᵢ
 
 end Left