chore: unify binary inf and min

[sven-manthe]

Unify binary inf and min, as discussed in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60sup.60.2F.60inf.60.20or.20.60max.60.2F.60min.60.20for.20set.20interval.20lemmas.3F.

---

Regressions: The instance for the product of metric spaces and some dependent instances are noncomputable now. I had the impression that noncomputability for reals is usual and unproblematic throughout mathlib, but could have a look at it otherwise.
Things that still need to be done: Optionally unify notation in some lemmas to always use min and max for total orders.

[FR-vdash-bot]

The instance for the product of metric spaces and some dependent instances are noncomputable now.

It can be fixed by adjusting the priority of instances. But leanprover/lean4#2905 causes the need to change the priority of instances of a lot of ordered algebraic typeclasses. You can also try to create shortcut instances only for ENNReal to see if it fixes everything.

[sven-manthe]

The instance for the product of metric spaces and some dependent instances are noncomputable now.

It can be fixed by adjusting the priority of instances. But leanprover/lean4#2905 causes the need to change the priority of instances of a lot of ordered algebraic typeclasses. You can also try to create shortcut instances only for ENNReal to see if it fixes everything.

I wasn't able to create the shortcut instances (Max on R≥0 is still deduced from some noncomputable ordered algebra instance). And I do not know enough about the typeclass inference algorithm and the classes in mathlib to play around with priorities

[github-actions]

PR summary 543c823f68

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance (priority := 100) ContinuousInf.measurableInf [Min γ] [ContinuousInf γ] :
+ instance (priority := 100) ContinuousInf.measurableInf₂ [SecondCountableTopology γ] [Min γ]
+ instance (priority := 100) ContinuousSup.measurableSup [Max γ] [ContinuousSup γ] :
+ instance (priority := 100) ContinuousSup.measurableSup₂ [SecondCountableTopology γ] [Max γ]
+ instance (priority := 100) InfTopHomClass.toTopHomClass [Min α] [Min β] [Top α]
+ instance (priority := 100) OrderDual.continuousInf (L : Type*) [TopologicalSpace L] [Max L]
+ instance (priority := 100) OrderDual.continuousSup (L : Type*) [TopologicalSpace L] [Min L]
+ instance (priority := 100) OrderDual.instMeasurableInf [Max M] [MeasurableSup M] :
+ instance (priority := 100) OrderDual.instMeasurableInf₂ [Max M] [MeasurableSup₂ M] :
+ instance (priority := 100) OrderDual.instMeasurableSup [Min M] [MeasurableInf M] :
+ instance (priority := 100) OrderDual.instMeasurableSup₂ [Min M] [MeasurableInf₂ M] :
+ instance (priority := 100) SupBotHomClass.toBotHomClass [Max α] [Max β] [Bot α]
+ instance : Add (LieSubalgebra R L) where add := max
+ instance : Add (LieSubmodule R L M) where add := max
+ instance : Bot (NonUnitalSubsemiring R)
+ instance : Inhabited (NonUnitalSubsemiring R)
+ instance : Max (Associates α)
+ instance : Max (BotHom α β)
+ instance : Max (CauSeq α abs)
+ instance : Max (ClopenUpperSet α)
+ instance : Max (Clopens α) := ⟨fun s t => ⟨s ∪ t, s.isClopen.union t.isClopen⟩⟩
+ instance : Max (CompactOpens α)
+ instance : Max (Compacts α)
+ instance : Max (Complementeds α)
+ instance : Max (Digraph V)
+ instance : Max (Filtration ι m)
+ instance : Max (FiniteGaloisIntermediateField k K)
+ instance : Max (FractionalIdeal S P)
+ instance : Max (GroupNorm E)
+ instance : Max (GroupSeminorm E)
+ instance : Max (HomogeneousIdeal 𝒜)
+ instance : Max (I.Filtration M)
+ instance : Max (Ideal P)
+ instance : Max (L.BoundedFormula α n)
+ instance : Max (LieSubmodule R L M)
+ instance : Max (LowerSet α)
+ instance : Max (NonarchAddGroupNorm E)
+ instance : Max (NonarchAddGroupSeminorm E)
+ instance : Max (NonemptyCompacts α)
+ instance : Max (NonemptyInterval α)
+ instance : Max (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊔ V.1, Or.inl U.2⟩⟩
+ instance : Max (OpenSubgroup G)
+ instance : Max (PositiveCompacts α)
+ instance : Max (SimpleGraph V)
+ instance : Max (SupBotHom α β)
+ instance : Max (SupHom α β)
+ instance : Max (TopHom α β)
+ instance : Max (UpperSet α)
+ instance : Max G.Finsubgraph
+ instance : Max G.Subgraph
+ instance : Max PartENat
+ instance : Max YoungDiagram
+ instance : Max {x // x ∈ L} := Sublattice.instSupCoe
+ instance : Max ℝ
+ instance : Min (Associates α)
+ instance : Min (BotHom α β)
+ instance : Min (CauSeq α abs)
+ instance : Min (ClopenUpperSet α)
+ instance : Min (Clopens α) := ⟨fun s t => ⟨s ∩ t, s.isClopen.inter t.isClopen⟩⟩
+ instance : Min (Complementeds α)
+ instance : Min (ConvexCone 𝕜 E)
+ instance : Min (Digraph V)
+ instance : Min (DiscreteQuotient X)
+ instance : Min (ExtensionOf i f)
+ instance : Min (Filtration ι m)
+ instance : Min (FiniteGaloisIntermediateField k K)
+ instance : Min (Finpartition a)
+ instance : Min (FractionalIdeal S P)
+ instance : Min (GroupSeminorm E)
+ instance : Min (GroupTopology α) where min x y := ⟨x.1 ⊓ y.1, topologicalGroup_inf x.2 y.2⟩
+ instance : Min (HomogeneousIdeal 𝒜)
+ instance : Min (I.Filtration M)
+ instance : Min (Ideal P)
+ instance : Min (InfHom α β)
+ instance : Min (InfTopHom α β)
+ instance : Min (L.BoundedFormula α n)
+ instance : Min (LieSubalgebra R L)
+ instance : Min (LieSubmodule R L M)
+ instance : Min (LowerSet α)
+ instance : Min (NonUnitalSubring R)
+ instance : Min (NonUnitalSubsemiring R)
+ instance : Min (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊓ V.1, U.2, V.2⟩⟩
+ instance : Min (Setoid α)
+ instance : Min (SimpleGraph V)
+ instance : Min (SimplicialComplex 𝕜 E)
+ instance : Min (StructureGroupoid H)
+ instance : Min (Subfield K)
+ instance : Min (Subgroup G)
+ instance : Min (Subgroupoid C)
+ instance : Min (Submodule R M)
+ instance : Min (Submonoid M)
+ instance : Min (Subring R)
+ instance : Min (Subsemigroup M)
+ instance : Min (Subsemiring R)
+ instance : Min (TopHom α β)
+ instance : Min (UniformSpace α)
+ instance : Min (UpperSet α)
+ instance : Min G.Finsubgraph
+ instance : Min G.Subgraph
+ instance : Min YoungDiagram
+ instance : Min {x // x ∈ L} := Sublattice.instInfCoe
+ instance : Min ℝ
+ instance [ContinuousMul G] : Max (OpenNormalSubgroup G)
+ instance [Max α] : Max (ULift.{v} α) where max x y := up <| x.down ⊔ y.down
+ instance [Max α] [Max β] : Max (α × β)
+ instance [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] : CoeTC F (SupBotHom α β)
+ instance [Max α] [Max β] [SupHomClass F α β] : CoeTC F (SupHom α β)
+ instance [Min α] : Min (ULift.{v} α) where min x y := up <| x.down ⊓ y.down
+ instance [Min α] [Min β] : Min (α × β)
+ instance [Min α] [Min β] [InfHomClass F α β] : CoeTC F (InfHom α β)
+ instance [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] : CoeTC F (InfTopHom α β)
+ instance [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] :
+ instance [SemilatticeInf α] : Min α where min a b := SemilatticeInf.inf a b
+ instance [SemilatticeInf β] : Min (α →o β)
+ instance [SemilatticeSup α] : Max α where max a b := SemilatticeSup.sup a b
+ instance [SemilatticeSup β] : Max (α →o β)
+ instance [T2Space α] : Min (Compacts α)
+ instance [∀ i, Max (α' i)] : Max (∀ i, α' i)
+ instance [∀ i, Min (α' i)] : Min (∀ i, α' i)
++ le_total_ideal
+-++++++------++-- instSup
+-+- sup_apply
+-+- sup_def
+-+-+- sup
- inf_eq_min
- instInfTropical
- instSupTropical
- instance (priority := 100) ContinuousInf.measurableInf [Inf γ] [ContinuousInf γ] :
- instance (priority := 100) ContinuousInf.measurableInf₂ [SecondCountableTopology γ] [Inf γ]
- instance (priority := 100) ContinuousSup.measurableSup [Sup γ] [ContinuousSup γ] :
- instance (priority := 100) ContinuousSup.measurableSup₂ [SecondCountableTopology γ] [Sup γ]
- instance (priority := 100) InfTopHomClass.toTopHomClass [Inf α] [Inf β] [Top α]
- instance (priority := 100) OrderDual.continuousInf (L : Type*) [TopologicalSpace L] [Sup L]
- instance (priority := 100) OrderDual.continuousSup (L : Type*) [TopologicalSpace L] [Inf L]
- instance (priority := 100) OrderDual.instMeasurableInf [Sup M] [MeasurableSup M] :
- instance (priority := 100) OrderDual.instMeasurableInf₂ [Sup M] [MeasurableSup₂ M] :
- instance (priority := 100) OrderDual.instMeasurableSup [Inf M] [MeasurableInf M] :
- instance (priority := 100) OrderDual.instMeasurableSup₂ [Inf M] [MeasurableInf₂ M] :
- instance (priority := 100) SupBotHomClass.toBotHomClass [Sup α] [Sup β] [Bot α]
- instance : Add (LieSubalgebra R L) where add := Sup.sup
- instance : Add (LieSubmodule R L M) where add := Sup.sup
- instance : Inf (Associates α)
- instance : Inf (BotHom α β)
- instance : Inf (CauSeq α abs)
- instance : Inf (ClopenUpperSet α)
- instance : Inf (Clopens α) := ⟨fun s t => ⟨s ∩ t, s.isClopen.inter t.isClopen⟩⟩
- instance : Inf (Complementeds α)
- instance : Inf (ConvexCone 𝕜 E)
- instance : Inf (Digraph V)
- instance : Inf (DiscreteQuotient X)
- instance : Inf (ExtensionOf i f)
- instance : Inf (Filtration ι m)
- instance : Inf (FiniteGaloisIntermediateField k K)
- instance : Inf (Finpartition a)
- instance : Inf (FractionalIdeal S P)
- instance : Inf (GroupSeminorm E)
- instance : Inf (GroupTopology α) where inf x y := ⟨x.1 ⊓ y.1, topologicalGroup_inf x.2 y.2⟩
- instance : Inf (HomogeneousIdeal 𝒜)
- instance : Inf (I.Filtration M)
- instance : Inf (Ideal P)
- instance : Inf (InfHom α β)
- instance : Inf (InfTopHom α β)
- instance : Inf (L.BoundedFormula α n)
- instance : Inf (LieSubalgebra R L)
- instance : Inf (LieSubmodule R L M)
- instance : Inf (LowerSet α)
- instance : Inf (NonUnitalSubring R)
- instance : Inf (NonUnitalSubsemiring R)
- instance : Inf (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊓ V.1, U.2, V.2⟩⟩
- instance : Inf (Setoid α)
- instance : Inf (SimpleGraph V)
- instance : Inf (SimplicialComplex 𝕜 E)
- instance : Inf (StructureGroupoid H)
- instance : Inf (Subfield K)
- instance : Inf (Subgroup G)
- instance : Inf (Subgroupoid C)
- instance : Inf (Submodule R M)
- instance : Inf (Submonoid M)
- instance : Inf (Subring R)
- instance : Inf (Subsemigroup M)
- instance : Inf (Subsemiring R)
- instance : Inf (TopHom α β)
- instance : Inf (TwoSidedIdeal R)
- instance : Inf (UniformSpace α)
- instance : Inf (UpperSet α)
- instance : Inf G.Finsubgraph
- instance : Inf G.Subgraph
- instance : Inf YoungDiagram
- instance : Inf {x // x ∈ L} := Sublattice.instInfCoe
- instance : Inf ℝ
- instance : Sup (Associates α)
- instance : Sup (BotHom α β)
- instance : Sup (Box ι)
- instance : Sup (CauSeq α abs)
- instance : Sup (ClopenUpperSet α)
- instance : Sup (Clopens α) := ⟨fun s t => ⟨s ∪ t, s.isClopen.union t.isClopen⟩⟩
- instance : Sup (CompactOpens α)
- instance : Sup (Compacts α)
- instance : Sup (Complementeds α)
- instance : Sup (Digraph V)
- instance : Sup (Filtration ι m)
- instance : Sup (FiniteGaloisIntermediateField k K)
- instance : Sup (FractionalIdeal S P)
- instance : Sup (GroupNorm E)
- instance : Sup (GroupSeminorm E)
- instance : Sup (HomogeneousIdeal 𝒜)
- instance : Sup (I.Filtration M)
- instance : Sup (Ideal P)
- instance : Sup (L.BoundedFormula α n)
- instance : Sup (LieSubmodule R L M)
- instance : Sup (LowerSet α)
- instance : Sup (NonarchAddGroupNorm E)
- instance : Sup (NonarchAddGroupSeminorm E)
- instance : Sup (NonemptyCompacts α)
- instance : Sup (NonemptyInterval α)
- instance : Sup (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊔ V.1, Or.inl U.2⟩⟩
- instance : Sup (OpenSubgroup G)
- instance : Sup (PositiveCompacts α)
- instance : Sup (SimpleGraph V)
- instance : Sup (SupBotHom α β)
- instance : Sup (SupHom α β)
- instance : Sup (TopHom α β)
- instance : Sup (TwoSidedIdeal R)
- instance : Sup (UpperSet α)
- instance : Sup G.Finsubgraph
- instance : Sup G.Subgraph
- instance : Sup PartENat
- instance : Sup YoungDiagram
- instance : Sup {x // x ∈ L} := Sublattice.instSupCoe
- instance : Sup ℝ
- instance [ContinuousMul G] : Sup (OpenNormalSubgroup G)
- instance [Inf α] : Inf (ULift.{v} α) where inf x y := up <| x.down ⊓ y.down
- instance [Inf α] [Inf β] : Inf (α × β)
- instance [Inf α] [Inf β] [InfHomClass F α β] : CoeTC F (InfHom α β)
- instance [Inf α] [Inf β] [Top α] [Top β] [InfTopHomClass F α β] : CoeTC F (InfTopHom α β)
- instance [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] : NonUnitalCStarAlgebra (A × B)
- instance [SemilatticeInf β] : Inf (α →o β)
- instance [SemilatticeSup β] : Sup (α →o β)
- instance [Sup α] : Sup (ULift.{v} α) where sup x y := up <| x.down ⊔ y.down
- instance [Sup α] [Sup β] : Sup (α × β)
- instance [Sup α] [Sup β] [Bot α] [Bot β] [SupBotHomClass F α β] : CoeTC F (SupBotHom α β)
- instance [Sup α] [Sup β] [SupHomClass F α β] : CoeTC F (SupHom α β)
- instance [T2Space α] : Inf (Compacts α)
- instance [∀ i, Inf (α' i)] : Inf (∀ i, α' i)
- instance [∀ i, Sup (α' i)] : Sup (∀ i, α' i)
-+-+ inf_apply
-+-+ inf_def
-+----++-+ inf
-+----------++++++++++--++ instInf
-- sup_eq_max

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 script/declarations_diff.sh contains some details about this script.