refactor: rename HasSup/HasInf to Sup/Inf (#2475)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -204,7 +204,7 @@ private theorem infₛ_le' {S : Set (Submodule R M)} {p} : p ∈ S → infₛ S
 private theorem le_infₛ' {S : Set (Submodule R M)} {p} : (∀ q ∈ S, p ≤ q) → p ≤ infₛ S :=
   Set.subset_interᵢ₂
 
-instance : HasInf (Submodule R M) :=
+instance : Inf (Submodule R M) :=
   ⟨fun p q ↦
     { carrier := p ∩ q
       zero_mem' := by simp [zero_mem]

Mathlib/Algebra/Order/Field/InjSurj.lean

@@ -28,7 +28,7 @@ namespace Function
 /-- Pullback a `LinearOrderedSemifield` under an injective map. -/
 @[reducible]
 def Injective.linearOrderedSemifield [LinearOrderedSemifield α] [Zero β] [One β] [Add β] [Mul β]
-    [Pow β ℕ] [SMul ℕ β] [NatCast β] [Inv β] [Div β] [Pow β ℤ] [HasSup β] [HasInf β] (f : β → α)
+    [Pow β ℕ] [SMul ℕ β] [NatCast β] [Inv β] [Div β] [Pow β ℤ] [Sup β] [Inf β] (f : β → α)
     (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
     (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
@@ -46,7 +46,7 @@ set_option maxHeartbeats 3000000
 @[reducible]
 def Injective.linearOrderedField [LinearOrderedField α] [Zero β] [One β] [Add β] [Mul β] [Neg β]
     [Sub β] [Pow β ℕ] [SMul ℕ β] [SMul ℤ β] [SMul ℚ β] [NatCast β] [IntCast β]
-    [RatCast β] [Inv β] [Div β] [Pow β ℤ] [HasSup β] [HasInf β] (f : β → α) (hf : Injective f)
+    [RatCast β] [Inv β] [Div β] [Pow β ℤ] [Sup β] [Inf β] (f : β → α) (hf : Injective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)

Mathlib/Algebra/Order/Group/Abs.lean

@@ -28,13 +28,13 @@ section Neg
 -- see Note [lower instance priority]
 /-- `abs a` is the absolute value of `a`. -/
 @[to_additive "`abs a` is the absolute value of `a`"]
-instance (priority := 100) Inv.toHasAbs [Inv α] [HasSup α] : Abs α :=
+instance (priority := 100) Inv.toHasAbs [Inv α] [Sup α] : Abs α :=
   ⟨fun a => a ⊔ a⁻¹⟩
 #align has_inv.to_has_abs Inv.toHasAbs
 #align has_neg.to_has_abs Neg.toHasAbs
 
 @[to_additive]
-theorem abs_eq_sup_inv [Inv α] [HasSup α] (a : α) : |a| = a ⊔ a⁻¹ :=
+theorem abs_eq_sup_inv [Inv α] [Sup α] (a : α) : |a| = a ⊔ a⁻¹ :=
   rfl
 #align abs_eq_sup_inv abs_eq_sup_inv
 #align abs_eq_sup_neg abs_eq_sup_neg

Mathlib/Algebra/Order/Group/InjSurj.lean

@@ -40,7 +40,7 @@ See note [reducible non-instances]. -/
   to_additive
       "Pullback a `LinearOrderedAddCommGroup` under an injective map."]
 def Function.Injective.linearOrderedCommGroup [LinearOrderedCommGroup α] {β : Type _} [One β]
-    [Mul β] [Inv β] [Div β] [Pow β ℕ] [Pow β ℤ] [HasSup β] [HasInf β] (f : β → α)
+    [Mul β] [Inv β] [Div β] [Pow β ℕ] [Pow β ℤ] [Sup β] [Inf β] (f : β → α)
     (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)

Mathlib/Algebra/Order/Kleene.lean

@@ -366,7 +366,7 @@ namespace Function.Injective
 /-- Pullback an `IdemSemiring` instance along an injective function. -/
 @[reducible]
 protected def idemSemiring [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β]
-    [NatCast β] [HasSup β] [Bot β] (f : β → α) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
+    [NatCast β] [Sup β] [Bot β] (f : β → α) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :
@@ -382,7 +382,7 @@ protected def idemSemiring [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β
 /-- Pullback an `IdemCommSemiring` instance along an injective function. -/
 @[reducible]
 protected def idemCommSemiring [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ]
-    [SMul ℕ β] [NatCast β] [HasSup β] [Bot β] (f : β → α) (hf : Injective f) (zero : f 0 = 0)
+    [SMul ℕ β] [NatCast β] [Sup β] [Bot β] (f : β → α) (hf : Injective f) (zero : f 0 = 0)
     (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :
@@ -395,7 +395,7 @@ protected def idemCommSemiring [IdemCommSemiring α] [Zero β] [One β] [Add β]
 /-- Pullback a `KleeneAlgebra` instance along an injective function. -/
 @[reducible]
 protected def kleeneAlgebra [KleeneAlgebra α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β]
-    [NatCast β] [HasSup β] [Bot β] [KStar β] (f : β → α) (hf : Injective f) (zero : f 0 = 0)
+    [NatCast β] [Sup β] [Bot β] [KStar β] (f : β → α) (hf : Injective f) (zero : f 0 = 0)
     (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (nat_cast : ∀ n : ℕ, f n = n) (sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥)

Mathlib/Algebra/Order/Monoid/Basic.lean

@@ -48,7 +48,7 @@ See note [reducible non-instances]. -/
 @[reducible,
   to_additive "Pullback an `OrderedAddCommMonoid` under an injective map."]
 def Function.Injective.linearOrderedCommMonoid [LinearOrderedCommMonoid α] {β : Type _} [One β]
-    [Mul β] [Pow β ℕ] [HasSup β] [HasInf β] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
+    [Mul β] [Pow β ℕ] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
     (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
     LinearOrderedCommMonoid β :=

Mathlib/Algebra/Order/Monoid/Cancel/Basic.lean

@@ -54,7 +54,7 @@ See note [reducible non-instances]. -/
   to_additive Function.Injective.linearOrderedCancelAddCommMonoid
       "Pullback a `LinearOrderedCancelAddCommMonoid` under an injective map."]
 def Function.Injective.linearOrderedCancelCommMonoid {β : Type _} [One β] [Mul β] [Pow β ℕ]
-    [HasSup β] [HasInf β] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
+    [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (one : f 1 = 1)
     (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
     LinearOrderedCancelCommMonoid β :=

Mathlib/Algebra/Order/Ring/InjSurj.lean

@@ -159,7 +159,7 @@ protected def strictOrderedCommRing [StrictOrderedCommRing α] [Zero β] [One β
 /-- Pullback a `LinearOrderedSemiring` under an injective map. -/
 @[reducible]
 protected def linearOrderedSemiring [LinearOrderedSemiring α] [Zero β] [One β] [Add β] [Mul β]
-    [Pow β ℕ] [SMul ℕ β] [NatCast β] [HasSup β] [HasInf β] (f : β → α) (hf : Injective f)
+    [Pow β ℕ] [SMul ℕ β] [NatCast β] [Sup β] [Inf β] (f : β → α) (hf : Injective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ n : ℕ, f n = n)
@@ -173,7 +173,7 @@ protected def linearOrderedSemiring [LinearOrderedSemiring α] [Zero β] [One β
 /-- Pullback a `LinearOrderedSemiring` under an injective map. -/
 @[reducible]
 protected def linearOrderedCommSemiring [LinearOrderedCommSemiring α] [Zero β] [One β] [Add β]
-    [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [HasSup β] [HasInf β] (f : β → α) (hf : Injective f)
+    [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Sup β] [Inf β] (f : β → α) (hf : Injective f)
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ n : ℕ, f n = n)
@@ -187,7 +187,7 @@ protected def linearOrderedCommSemiring [LinearOrderedCommSemiring α] [Zero β]
 /-- Pullback a `LinearOrderedRing` under an injective map. -/
 @[reducible]
 def linearOrderedRing [LinearOrderedRing α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β]
-    [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [HasSup β] [HasInf β] (f : β → α)
+    [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [Sup β] [Inf β] (f : β → α)
     (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
     (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
@@ -203,8 +203,8 @@ def linearOrderedRing [LinearOrderedRing α] [Zero β] [One β] [Add β] [Mul β
 /-- Pullback a `LinearOrderedCommRing` under an injective map. -/
 @[reducible]
 protected def linearOrderedCommRing [LinearOrderedCommRing α] [Zero β] [One β] [Add β] [Mul β]
-    [Neg β] [Sub β] [Pow β ℕ] [SMul ℕ β] [SMul ℤ β] [NatCast β] [IntCast β] [HasSup β]
-    [HasInf β] (f : β → α) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
+    [Neg β] [Sub β] [Pow β ℕ] [SMul ℕ β] [SMul ℤ β] [NatCast β] [IntCast β] [Sup β]
+    [Inf β] (f : β → α) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
     (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x)

Mathlib/Algebra/Order/WithZero.lean

@@ -80,7 +80,7 @@ The following facts are true more generally in a (linearly) ordered commutative
 See note [reducible non-instances]. -/
 @[reducible]
 def Function.Injective.linearOrderedCommMonoidWithZero {β : Type _} [Zero β] [One β] [Mul β]
-    [Pow β ℕ] [HasSup β] [HasInf β] (f : β → α) (hf : Function.Injective f) (zero : f 0 = 0)
+    [Pow β ℕ] [Sup β] [Inf β] (f : β → α) (hf : Function.Injective f) (zero : f 0 = 0)
     (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
     (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
     LinearOrderedCommMonoidWithZero β :=

Mathlib/Algebra/Tropical/Lattice.lean

@@ -34,21 +34,21 @@ variable {R S : Type _}
 
 open Tropical
 
-instance [HasSup R] : HasSup (Tropical R) where
+instance [Sup R] : Sup (Tropical R) where
   sup x y := trop (untrop x ⊔ untrop y)
 
-instance [HasInf R] : HasInf (Tropical R) where
+instance [Inf R] : Inf (Tropical R) where
   inf x y := trop (untrop x ⊓ untrop y)
 
 instance [SemilatticeInf R] : SemilatticeInf (Tropical R) :=
-  { instHasInfTropical,
+  { instInfTropical,
     Tropical.instPartialOrderTropical with
     le_inf := fun _ _ _ ↦ @SemilatticeInf.le_inf R _ _ _ _
     inf_le_left := fun _ _ ↦ inf_le_left
     inf_le_right := fun _ _ ↦ inf_le_right }
 
 instance [SemilatticeSup R] : SemilatticeSup (Tropical R) :=
-  { instHasSupTropical,
+  { instSupTropical,
     Tropical.instPartialOrderTropical with
     sup_le := fun _ _ _ ↦ @SemilatticeSup.sup_le R _ _ _ _
     le_sup_left := fun _ _ ↦ le_sup_left
@@ -62,7 +62,7 @@ instance [SupSet R] : SupSet (Tropical R) where supₛ s := trop (supₛ (untrop
 instance [InfSet R] : InfSet (Tropical R) where infₛ s := trop (infₛ (untrop '' s))
 
 instance [ConditionallyCompleteLattice R] : ConditionallyCompleteLattice (Tropical R) :=
-  { @instHasInfTropical R _, @instHasSupTropical R _,
+  { @instInfTropical R _, @instSupTropical R _,
     instLatticeTropical with
     le_csupₛ  := fun _s _x hs hx ↦
       le_csupₛ (untrop_monotone.map_bddAbove hs) (Set.mem_image_of_mem untrop hx)

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -215,7 +215,7 @@ theorem isSubgraph_eq_le : (IsSubgraph : SimpleGraph V → SimpleGraph V → Pro
 #align simple_graph.is_subgraph_eq_le SimpleGraph.isSubgraph_eq_le
 
 /-- The supremum of two graphs `x ⊔ y` has edges where either `x` or `y` have edges. -/
-instance : HasSup (SimpleGraph V) :=
+instance : Sup (SimpleGraph V) :=
   ⟨fun x y =>
     { Adj := x.Adj ⊔ y.Adj
       symm := fun v w h => by rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm] }⟩
@@ -226,7 +226,7 @@ theorem sup_adj (x y : SimpleGraph V) (v w : V) : (x ⊔ y).Adj v w ↔ x.Adj v
 #align simple_graph.sup_adj SimpleGraph.sup_adj
 
 /-- The infimum of two graphs `x ⊓ y` has edges where both `x` and `y` have edges. -/
-instance : HasInf (SimpleGraph V) :=
+instance : Inf (SimpleGraph V) :=
   ⟨fun x y =>
     { Adj := x.Adj ⊓ y.Adj
       symm := fun v w h => by rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm] }⟩

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -111,7 +111,7 @@ theorem cells_ssubset_iff {μ ν : YoungDiagram} : μ.cells ⊂ ν.cells ↔ μ
   Iff.rfl
 #align young_diagram.cells_ssubset_iff YoungDiagram.cells_ssubset_iff
 
-instance : HasSup YoungDiagram
+instance : Sup YoungDiagram
     where sup μ ν :=
     { cells := μ.cells ∪ ν.cells
       isLowerSet := by
@@ -133,7 +133,7 @@ theorem mem_sup {μ ν : YoungDiagram} {x : ℕ × ℕ} : x ∈ μ ⊔ ν ↔ x
   Finset.mem_union
 #align young_diagram.mem_sup YoungDiagram.mem_sup
 
-instance : HasInf YoungDiagram
+instance : Inf YoungDiagram
     where inf μ ν :=
     { cells := μ.cells ∩ ν.cells
       isLowerSet := by

Mathlib/Data/Finset/Basic.lean

@@ -1296,12 +1296,12 @@ instance : Lattice (Finset α) :=
     inf_le_right := fun _ _ _ h => (mem_ndinter.1 h).2 }
 
 @[simp]
-theorem sup_eq_union : (HasSup.sup : Finset α → Finset α → Finset α) = Union.union :=
+theorem sup_eq_union : (Sup.sup : Finset α → Finset α → Finset α) = Union.union :=
   rfl
 #align finset.sup_eq_union Finset.sup_eq_union
 
 @[simp]
-theorem inf_eq_inter : (HasInf.inf : Finset α → Finset α → Finset α) = Inter.inter :=
+theorem inf_eq_inter : (Inf.inf : Finset α → Finset α → Finset α) = Inter.inter :=
   rfl
 #align finset.inf_eq_inter Finset.inf_eq_inter
 

Mathlib/Data/Nat/PartENat.lean

@@ -130,7 +130,7 @@ instance : Top PartENat :=
 instance : Bot PartENat :=
   ⟨0⟩
 
-instance : HasSup PartENat :=
+instance : Sup PartENat :=
   ⟨fun x y => ⟨x.Dom ∧ y.Dom, fun h => x.get h.1 ⊔ y.get h.2⟩⟩
 
 theorem le_def (x y : PartENat) :

Mathlib/Data/Rat/Order.lean

@@ -211,9 +211,9 @@ instance : SemilatticeInf ℚ := by infer_instance
 
 instance : SemilatticeSup ℚ := by infer_instance
 
-instance : HasInf ℚ := by infer_instance
+instance : Inf ℚ := by infer_instance
 
-instance : HasSup ℚ := by infer_instance
+instance : Sup ℚ := by infer_instance
 
 instance : PartialOrder ℚ := by infer_instance
 

Mathlib/Data/Real/Basic.lean

@@ -458,7 +458,7 @@ instance nontrivial : Nontrivial ℝ :=
 private irreducible_def sup : ℝ → ℝ → ℝ
   | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊔ ·) (fun _ _ hx _ _ hy => sup_equiv_sup hx hy) x y⟩
 
-instance : HasSup ℝ :=
+instance : Sup ℝ :=
   ⟨sup⟩
 
 theorem ofCauchy_sup (a b) : (⟨⟦a ⊔ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩ :=
@@ -475,7 +475,7 @@ theorem mk_sup (a b) : (mk (a ⊔ b) : ℝ) = mk a ⊔ mk b :=
 private irreducible_def inf : ℝ → ℝ → ℝ
   | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊓ ·) (fun _ _ hx _ _ hy => inf_equiv_inf hx hy) x y⟩
 
-instance : HasInf ℝ :=
+instance : Inf ℝ :=
   ⟨inf⟩
 
 theorem ofCauchy_inf (a b) : (⟨⟦a ⊓ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊓ ⟨⟦b⟧⟩ :=

Mathlib/Data/Real/CauSeq.lean

@@ -824,14 +824,14 @@ theorem rat_inf_continuous_lemma {ε : α} {a₁ a₂ b₁ b₂ : α} :
   (abs_min_sub_min_le_max _ _ _ _).trans_lt (max_lt h₁ h₂)
 #align rat_inf_continuous_lemma CauSeq.rat_inf_continuous_lemma
 
-instance : HasSup (CauSeq α abs) :=
+instance : Sup (CauSeq α abs) :=
   ⟨fun f g =>
     ⟨f ⊔ g, fun _ ε0 =>
       (exists_forall_ge_and (f.cauchy₃ ε0) (g.cauchy₃ ε0)).imp fun _ H _ ij =>
         let ⟨H₁, H₂⟩ := H _ le_rfl
         rat_sup_continuous_lemma (H₁ _ ij) (H₂ _ ij)⟩⟩
 
-instance : HasInf (CauSeq α abs) :=
+instance : Inf (CauSeq α abs) :=
   ⟨fun f g =>
     ⟨f ⊓ g, fun _ ε0 =>
       (exists_forall_ge_and (f.cauchy₃ ε0) (g.cauchy₃ ε0)).imp fun _ H _ ij =>

Mathlib/Data/Setoid/Basic.lean

@@ -130,7 +130,7 @@ protected def prod (r : Setoid α) (s : Setoid β) :
 #align setoid.prod Setoid.prod
 
 /-- The infimum of two equivalence relations. -/
-instance : HasInf (Setoid α) :=
+instance : Inf (Setoid α) :=
   ⟨fun r s =>
     ⟨fun x y => r.Rel x y ∧ s.Rel x y,
       ⟨fun x => ⟨r.refl' x, s.refl' x⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩, fun h1 h2 =>
@@ -174,7 +174,7 @@ instance : PartialOrder (Setoid α) where
 instance completeLattice : CompleteLattice (Setoid α) :=
   { (completeLatticeOfInf (Setoid α)) fun _ =>
       ⟨fun _ hr _ _ h => h _ hr, fun _ hr _ _ h _ hr' => hr hr' h⟩ with
-    inf := HasInf.inf
+    inf := Inf.inf
     inf_le_left := fun _ _ _ _ h => h.1
     inf_le_right := fun _ _ _ _ h => h.2
     le_inf := fun _ _ _ h1 h2 _ _ h => ⟨h1 h, h2 h⟩

Mathlib/FieldTheory/Subfield.lean

@@ -585,7 +585,7 @@ namespace Subfield
 
 
 /-- The inf of two subfields is their intersection. -/
-instance : HasInf (Subfield K) :=
+instance : Inf (Subfield K) :=
   ⟨fun s t =>
     { s.toSubring ⊓ t.toSubring with
       inv_mem' := fun _ hx =>

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -980,7 +980,7 @@ theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (
 
 /-- The inf of two subgroups is their intersection. -/
 @[to_additive "The inf of two `add_subgroups`s is their intersection."]
-instance : HasInf (Subgroup G) :=
+instance : Inf (Subgroup G) :=
   ⟨fun H₁ H₂ =>
     { H₁.toSubmonoid ⊓ H₂.toSubmonoid with
       inv_mem' := fun ⟨hx, hx'⟩ => ⟨H₁.inv_mem hx, H₂.inv_mem hx'⟩ }⟩

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -296,7 +296,7 @@ theorem coe_bot : ((⊥ : Submonoid M) : Set M) = {1} :=
 
 /-- The inf of two submonoids is their intersection. -/
 @[to_additive "The inf of two `AddSubmonoid`s is their intersection."]
-instance : HasInf (Submonoid M) :=
+instance : Inf (Submonoid M) :=
   ⟨fun S₁ S₂ =>
     { carrier := S₁ ∩ S₂
       one_mem' := ⟨S₁.one_mem, S₂.one_mem⟩

Mathlib/GroupTheory/Subsemigroup/Basic.lean

@@ -221,7 +221,7 @@ theorem coe_bot : ((⊥ : Subsemigroup M) : Set M) = ∅ :=
 
 /-- The inf of two subsemigroups is their intersection. -/
 @[to_additive "The inf of two `AddSubsemigroup`s is their intersection."]
-instance : HasInf (Subsemigroup M) :=
+instance : Inf (Subsemigroup M) :=
   ⟨fun S₁ S₂ =>
     { carrier := S₁ ∩ S₂
       mul_mem' := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ => ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

Mathlib/LinearAlgebra/LinearPMap.lean

@@ -258,9 +258,9 @@ def eqLocus (f g : E →ₗ.[R] F) : Submodule R E where
         by erw [f.map_smul c ⟨x, hfx⟩, g.map_smul c ⟨x, hgx⟩, hx]⟩
 #align linear_pmap.eq_locus LinearPMap.eqLocus
 
-instance hasInf : HasInf (E →ₗ.[R] F) :=
+instance inf : Inf (E →ₗ.[R] F) :=
   ⟨fun f g => ⟨f.eqLocus g, f.toFun.comp <| ofLe fun _x hx => hx.fst⟩⟩
-#align linear_pmap.has_inf LinearPMap.hasInf
+#align linear_pmap.has_inf LinearPMap.inf
 
 instance bot : Bot (E →ₗ.[R] F) :=
   ⟨⟨⊥, 0⟩⟩

Mathlib/MeasureTheory/MeasurableSpace.lean

@@ -1725,7 +1725,7 @@ theorem coe_union (s t : Subtype (MeasurableSet : Set α → Prop)) : ↑(s ∪
   rfl
 #align measurable_set.coe_union MeasurableSet.coe_union
 
-noncomputable instance : HasSup (Subtype (MeasurableSet : Set α → Prop)) :=
+noncomputable instance : Sup (Subtype (MeasurableSet : Set α → Prop)) :=
   ⟨fun x y => x ∪ y⟩
 
 -- porting note: new lemma
@@ -1740,7 +1740,7 @@ theorem coe_inter (s t : Subtype (MeasurableSet : Set α → Prop)) : ↑(s ∩
   rfl
 #align measurable_set.coe_inter MeasurableSet.coe_inter
 
-noncomputable instance : HasInf (Subtype (MeasurableSet : Set α → Prop)) :=
+noncomputable instance : Inf (Subtype (MeasurableSet : Set α → Prop)) :=
   ⟨fun x y => x ∩ y⟩
 
 -- porting note: new lemma