refactor: use OrderSupInfSet

[astrainfinita]

---

• depends on: [Merged by Bors] - chore: clean up sSup and sInf usage #35297
• depends on: chore: use IsLUB IsGLB in CompleteLattice #35328
• depends on: chore: use IsLUB IsGLB in ConditionallyCompleteLattice #35774
• depends on: refactor: use OrderSupInfSet in ConditionallyCompleteLattice #35674

Zulip

[github-actions]

PR summary 738faa5527

Import changes exceeding 2%

%	File
+45.07%	Mathlib.Order.Bounds.Defs

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Bounds.Defs	71	103	+32 (+45.07%)
Mathlib.Order.Bounds.Basic	212	213	+1 (+0.47%)
Mathlib.Order.Bounds.Image	216	217	+1 (+0.46%)
Mathlib.Order.CompleteLattice.Basic	230	231	+1 (+0.43%)
Mathlib.Order.CompleteLattice.Lemmas	233	234	+1 (+0.43%)
Mathlib.Algebra.Tropical.Lattice	288	289	+1 (+0.35%)

Import changes for all files

Files	Import difference
139 files Mathlib.Algebra.Algebra.Field Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.CharP.Basic Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.Field.Rat Mathlib.Algebra.IsPrimePow Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.Rat Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Field.Basic Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Floor.Defs Mathlib.Algebra.Order.Floor.Semiring Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.PiLex Mathlib.Algebra.Order.Group.Pointwise.Interval Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Field Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Abs Mathlib.Algebra.Order.Ring.Cast Mathlib.Algebra.Order.Ring.Int Mathlib.Algebra.Quandle Mathlib.Algebra.Ring.BooleanRing Mathlib.Algebra.Ring.Identities Mathlib.Algebra.Star.Rat Mathlib.Algebra.Star.SelfAdjoint Mathlib.Algebra.Star.StarProjection Mathlib.Algebra.Tropical.Lattice Mathlib.CategoryTheory.ObjectProperty.CompleteLattice Mathlib.Combinatorics.Enumerative.Stirling Mathlib.Combinatorics.Graph.Basic Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Data.BitVec Mathlib.Data.Fin.FlagRange Mathlib.Data.Fin.Parity Mathlib.Data.Finite.Vector Mathlib.Data.Fintype.Vector Mathlib.Data.Int.AbsoluteValue Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Lemmas Mathlib.Data.Int.Log Mathlib.Data.Int.ModEq Mathlib.Data.Int.Order.Lemmas Mathlib.Data.Int.Order.Units Mathlib.Data.List.Sym Mathlib.Data.Multiset.Sym Mathlib.Data.NNRat.Defs Mathlib.Data.Nat.Cast.Order.Field Mathlib.Data.Nat.ChineseRemainder Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Nat.ModEq Mathlib.Data.Nat.Prime.Infinite Mathlib.Data.Nat.WithBot Mathlib.Data.Num.Prime Mathlib.Data.Num.ZNum Mathlib.Data.PNat.Xgcd Mathlib.Data.Rat.BigOperators Mathlib.Data.Rat.Cast.CharZero Mathlib.Data.Rat.Cast.Defs Mathlib.Data.Rat.NatSqrt.Defs Mathlib.Data.Rat.Sqrt Mathlib.Data.Setoid.Basic Mathlib.Data.Sym.Basic Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Data.UInt Mathlib.Data.ZMod.Defs Mathlib.GroupTheory.Congruence.BigOperators Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.Order.Antichain Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.OrderIso Mathlib.Order.Circular.ZMod Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.GameAdd Mathlib.Order.Hom.Set Mathlib.Order.Interval.Set.Fin Mathlib.Order.Interval.Set.IsoIoo Mathlib.Order.Interval.Set.OrderEmbedding Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.UnorderedInterval Mathlib.Order.Lattice.Congruence Mathlib.Order.LatticeIntervals Mathlib.Order.Minimal Mathlib.Order.Monotone.Odd Mathlib.Order.Monotone.Union Mathlib.Order.PiLex Mathlib.Order.Preorder.Chain Mathlib.Order.Preorder.Finite Mathlib.Order.ScottContinuity Mathlib.Order.WellFounded Mathlib.RingTheory.Congruence.BigOperators Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Coprime.Basic Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.PGame.Algebra Mathlib.SetTheory.PGame.Order Mathlib.Tactic.Bound Mathlib.Tactic.CancelDenoms Mathlib.Tactic.FieldSimp.Discharger Mathlib.Tactic.FieldSimp Mathlib.Tactic.Field Mathlib.Tactic.Finiteness Mathlib.Tactic.Group Mathlib.Tactic.Linarith.Frontend Mathlib.Tactic.LinearCombination' Mathlib.Tactic.LinearCombination Mathlib.Tactic.ModCases Mathlib.Tactic.NormNum.DivMod Mathlib.Tactic.NormNum.Eq Mathlib.Tactic.NormNum.Ineq Mathlib.Tactic.NormNum.Inv Mathlib.Tactic.NormNum.ModEq Mathlib.Tactic.Positivity.Basic Mathlib.Tactic.Positivity.Core Mathlib.Tactic.Positivity Mathlib.Tactic.Qify Mathlib.Tactic.Ring.Basic Mathlib.Tactic.Ring.Common Mathlib.Tactic.Ring.Compare Mathlib.Tactic.Ring.PNat Mathlib.Tactic.Ring.RingNF Mathlib.Tactic.Ring Mathlib.Topology.Defs.Filter	1
Mathlib.Data.Int.GCD	3
Mathlib.Order.Nat	9
Mathlib.Order.Bounds.Defs	32

---

Declarations diff

+ IsGreatest.isLUB
+ OrderDual.orderSupInfSet
+ OrderSupInfSet
+ OrderSupInfSet.choose
+ OrderSupInfSet.ofSupSet
+ Set.Icc.instInfSet
+ Set.Icc.instSupSet
+ Set.Icc.isGLB_sInf
+ Set.Icc.isLUB_sSup
+ Set.isGLB_sInter
+ Set.isLUB_sUnion
+ Subfunctor.isGLB_sInf
+ Subfunctor.isLUB_sSup
+ UniformSpace.isGLB_sInf
+ WithBot.isGLB_image_coe
+ WithBot.isLUB_image_coe
+ WithTop.instOrderSupInfSet
+ WithTop.isGLB_image_coe
+ WithTop.isLUB_image_coe
+ exists_isLUB_iff_isLUB_sSup
+ exists_isLUB_of_nonempty_of_bddAbove
+ instInfSet
+ instOrderSupInfSet
+ instPartialOrder
+ instSupSet
+ instance : InfSet (AffineSubspace k P)
+ instance : InfSet (Subfunctor F)
+ instance : InfSet (fixedPoints f)
+ instance : NoBotOrder ℤ := ⟨fun x ↦ ⟨x - 1, (Int.sub_one_lt_of_le le_rfl).not_ge⟩⟩
+ instance : NoTopOrder ℤ := ⟨fun x ↦ ⟨x + 1, (Int.lt_add_one_of_le le_rfl).not_ge⟩⟩
+ instance : OrderSupInfSet (Nucleus X) := .ofInfSet fun _ _ ↦ Nucleus.isGLB_sInf _
+ instance : SupSet (AffineSubspace k P)
+ instance : SupSet (IdealSheafData X)
+ instance : SupSet (Subfunctor F)
+ instance : SupSet (fixedPoints f)
+ instance [Preorder α] [OrderSupInfSet α] [Preorder β] [OrderSupInfSet β] :
+ instance {α : Type*} {β : α → Type*} [∀ i, Preorder (β i)] [∀ i, OrderSupInfSet (β i)] :
+ isGLB_mk_fun
+ isLUB_mk_fun
+ isLUB_sSup_of_exists_isLUB
+ ordConnectedSubsetConditionallyCompleteLinearOrderOfBotTop
+ sSup_apply'
+ subset_upperBounds_lowerBounds
+++++++++++ isGLB_sInf
+++++++++-++ isLUB_sSup
+-- le_sSup
+-- sSup_le
- IsGLB.iInf_eq
- IsLeast.isGLB
- Pi.infSet
- WithBot.instInfSet
- WithBot.instSupSet
- csInf_le
- instance : CompleteSemilatticeInf (Nucleus X)
- isGLB_csInf
- le_csInf
- le_sInf
- sInf_apply
- sInf_le
- sInf_univ
- subset_lowerBounds_upperBounds
-+- sInf_empty

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: clean up sSup and sInf usage #35297
• chore: use IsLUB IsGLB in CompleteLattice #35328
• chore: use IsLUB IsGLB in ConditionallyCompleteLattice #35774
• refactor: use OrderSupInfSet in ConditionallyCompleteLattice #35674
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.