refactor(order/conditionally_complete_lattice): csupr_le_csupr → csupr_mono (#13320)

For consistency with `supr_mono` and `infi_mono`

Author: vihdzp

src/dynamics/circle/rotation_number/translation_number.lean

@@ -839,7 +839,7 @@ begin
   -- Now we apply `cSup_div_semiconj` and go back to `f₁` and `f₂`.
   refine ⟨⟨_, λ x y hxy, _, λ x, _⟩, cSup_div_semiconj F₂ F₁ (λ x, _)⟩;
     simp only [hF₁, hF₂, ← monoid_hom.map_inv, coe_mk],
-  { refine csupr_le_csupr (this y) (λ g, _),
+  { refine csupr_mono (this y) (λ g, _),
     exact mono _ (mono _ hxy) },
   { simp only [map_add_one],
     exact (map_csupr_of_continuous_at_of_monotone (continuous_at_id.add continuous_at_const)

src/order/conditionally_complete_lattice.lean

@@ -455,7 +455,7 @@ lemma le_csupr_of_le {f : ι → α} (H : bdd_above (range f)) (c : ι) (h : a 
 le_trans h (le_csupr H c)
 
 /--The indexed supremum of two functions are comparable if the functions are pointwise comparable-/
-lemma csupr_le_csupr {f g : ι → α} (B : bdd_above (range g)) (H : ∀x, f x ≤ g x) :
+lemma csupr_mono {f g : ι → α} (B : bdd_above (range g)) (H : ∀ x, f x ≤ g x) :
   supr f ≤ supr g :=
 begin
   casesI is_empty_or_nonempty ι,
@@ -468,9 +468,9 @@ lemma le_csupr_set {f : β → α} {s : set β}
 (le_cSup H $ mem_image_of_mem f hc).trans_eq Sup_image'
 
 /--The indexed infimum of two functions are comparable if the functions are pointwise comparable-/
-lemma cinfi_le_cinfi {f g : ι → α} (B : bdd_below (range f)) (H : ∀x, f x ≤ g x) :
+lemma cinfi_mono {f g : ι → α} (B : bdd_below (range f)) (H : ∀ x, f x ≤ g x) :
   infi f ≤ infi g :=
-@csupr_le_csupr (order_dual α) _ _ _ _ B H
+@csupr_mono (order_dual α) _ _ _ _ B H
 
 /--The indexed minimum of a function is bounded below by a uniform lower bound-/
 lemma le_cinfi [nonempty ι] {f : ι → α} {c : α} (H : ∀x, c ≤ f x) : c ≤ infi f :=

src/topology/metric_space/gluing.lean

@@ -110,7 +110,7 @@ private lemma glue_dist_triangle (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
           (B _ _),
         intros x y hx, simpa },
       rw [this, comp],
-      refine cinfi_le_cinfi (B _ _) (λp, _),
+      refine cinfi_mono (B _ _) (λp, _),
       calc
         dist z (Φ p) + dist x (Ψ p) ≤ (dist y z + dist y (Φ p)) + dist x (Ψ p) :
           add_le_add (dist_triangle_left _ _ _) le_rfl
@@ -128,7 +128,7 @@ private lemma glue_dist_triangle (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
           (B _ _),
         intros x y hx, simpa },
       rw [this, comp],
-      refine cinfi_le_cinfi (B _ _) (λp, _),
+      refine cinfi_mono (B _ _) (λp, _),
       calc
         dist z (Φ p) + dist x (Ψ p) ≤ dist z (Φ p) + (dist x y + dist y (Ψ p)) :
           add_le_add le_rfl (dist_triangle _ _ _)
@@ -146,7 +146,7 @@ private lemma glue_dist_triangle (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
           (B _ _),
         intros x y hx, simpa },
       rw [this, comp],
-      refine cinfi_le_cinfi (B _ _) (λp, _),
+      refine cinfi_mono (B _ _) (λp, _),
       calc
         dist x (Φ p) + dist z (Ψ p) ≤ (dist x y + dist y (Φ p)) + dist z (Ψ p) :
           add_le_add (dist_triangle _ _ _) le_rfl
@@ -164,7 +164,7 @@ private lemma glue_dist_triangle (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
           (B _ _),
         intros x y hx, simpa },
       rw [this, comp],
-      refine cinfi_le_cinfi (B _ _) (λp, _),
+      refine cinfi_mono (B _ _) (λp, _),
       calc
         dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + (dist y z + dist y (Ψ p)) :
           add_le_add le_rfl (dist_triangle_left _ _ _)

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -363,8 +363,8 @@ begin
   -- prove the inequality but with `dist f g` inside, by using inequalities comparing
   -- supr to supr and infi to infi
   have Z : (⨆ x, ⨅ y, f (inl x, inr y)) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g :=
-    csupr_le_csupr (HD_bound_aux1 _ (dist f g))
-      (λx, cinfi_le_cinfi ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
+    csupr_mono (HD_bound_aux1 _ (dist f g))
+      (λx, cinfi_mono ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
   -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
   -- (here the addition of `dist f g`) preserve infimum and supremum
   have E1 : ∀ x, (⨅ y, g (inl x, inr y)) + dist f g = ⨅ y, g (inl x, inr y) + dist f g,
@@ -392,8 +392,8 @@ begin
   -- prove the inequality but with `dist f g` inside, by using inequalities comparing
   -- supr to supr and infi to infi
   have Z : (⨆ y, ⨅ x, f (inl x, inr y)) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g :=
-    csupr_le_csupr (HD_bound_aux2 _ (dist f g))
-      (λy, cinfi_le_cinfi  ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
+    csupr_mono (HD_bound_aux2 _ (dist f g))
+      (λy, cinfi_mono  ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
   -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
   -- (here the addition of `dist f g`) preserve infimum and supremum
   have E1 : ∀ y, (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g,