chore(Order): remove redundant instance fields (#30752)

This PR continues the cleanup from #30734, mosly removing `bot := ⊥`.

I also want to remove occurrences of `sup := (· ⊔ ·)`, but the problem is that the `sup` and `min` fields are different, making things more awkward than they should be. (See also #24614)

I found these redundant instance fields using VSCode's built-in search.

Author: JovanGerb

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -130,7 +130,7 @@ lemma volume_needleSpace : ℙ (needleSpace d) = ENNReal.ofReal (d * π) := by
 
 lemma measurable_needleCrossesIndicator : Measurable (needleCrossesIndicator l) := by
   unfold needleCrossesIndicator
-  refine Measurable.indicator measurable_const (IsClosed.measurableSet (IsClosed.inter ?l ?r))
+  refine Measurable.indicator measurable_const (IsClosed.measurableSet (IsClosed.and ?l ?r))
   all_goals simp only [tsub_le_iff_right, zero_add, ← neg_le_iff_add_nonneg']
   case' l => refine isClosed_le continuous_fst ?_
   case' r => refine isClosed_le (Continuous.neg continuous_fst) ?_

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -76,7 +76,6 @@ instance uniqueBot : Unique (⊥ : Submodule R M) :=
   ⟨inferInstance, fun x ↦ Subtype.ext <| (mem_bot R).1 x.mem⟩
 
 instance : OrderBot (Submodule R M) where
-  bot := ⊥
   bot_le p x := by simp +contextual [zero_mem]
 
 protected theorem eq_bot_iff (p : Submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
@@ -145,7 +144,6 @@ theorem mem_top {x : M} : x ∈ (⊤ : Submodule R M) :=
   trivial
 
 instance : OrderTop (Submodule R M) where
-  top := ⊤
   le_top _ _ _ := trivial
 
 theorem eq_top_iff' {p : Submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=

Mathlib/Algebra/Order/Kleene.lean

@@ -324,7 +324,6 @@ protected abbrev idemSemiring [IdemSemiring α] [Zero β] [One β] [Add β] [Mul
   { hf.semiring f zero one add mul nsmul npow natCast, hf.semilatticeSup _ sup,
     ‹Bot β› with
     add_eq_sup := fun a b ↦ hf <| by rw [sup, add, add_eq_sup]
-    bot := ⊥
     bot_le := fun a ↦ bot.trans_le <| @bot_le _ _ _ <| f a }
 
 -- See note [reducible non-instances]

Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

@@ -112,7 +112,6 @@ instance : LE (Prepartition I) :=
   ⟨fun π π' => ∀ ⦃I⦄, I ∈ π → ∃ I' ∈ π', I ≤ I'⟩
 
 instance partialOrder : PartialOrder (Prepartition I) where
-  le := (· ≤ ·)
   le_refl _ I hI := ⟨I, hI, le_rfl⟩
   le_trans _ _ _ h₁₂ h₂₃ _ hI₁ :=
     let ⟨_, hI₂, hI₁₂⟩ := h₁₂ hI₁

Mathlib/Analysis/NormedSpace/ENormedSpace.lean

@@ -156,23 +156,19 @@ theorem top_map {x : V} (hx : x ≠ 0) : (⊤ : ENormedSpace 𝕜 V) x = ⊤ :=
   if_neg hx
 
 noncomputable instance : OrderTop (ENormedSpace 𝕜 V) where
-  top := ⊤
   le_top e x := by obtain h | h := eq_or_ne x 0 <;> simp [top_map, h]
 
-noncomputable instance : SemilatticeSup (ENormedSpace 𝕜 V) :=
-  { ENormedSpace.partialOrder with
-    le := (· ≤ ·)
-    lt := (· < ·)
-    sup := fun e₁ e₂ =>
-      { toFun := fun x => max (e₁ x) (e₂ x)
-        eq_zero' := fun _ h => e₁.eq_zero_iff.1 (ENNReal.max_eq_zero_iff.1 h).1
-        map_add_le' := fun _ _ =>
-          max_le (le_trans (e₁.map_add_le _ _) <| add_le_add (le_max_left _ _) (le_max_left _ _))
-            (le_trans (e₂.map_add_le _ _) <| add_le_add (le_max_right _ _) (le_max_right _ _))
-        map_smul_le' := fun c x => le_of_eq <| by simp only [map_smul, mul_max] }
-    le_sup_left := fun _ _ _ => le_max_left _ _
-    le_sup_right := fun _ _ _ => le_max_right _ _
-    sup_le := fun _ _ _ h₁ h₂ x => max_le (h₁ x) (h₂ x) }
+noncomputable instance : SemilatticeSup (ENormedSpace 𝕜 V) where
+  sup := fun e₁ e₂ =>
+    { toFun := fun x => max (e₁ x) (e₂ x)
+      eq_zero' := fun _ h => e₁.eq_zero_iff.1 (ENNReal.max_eq_zero_iff.1 h).1
+      map_add_le' := fun _ _ =>
+        max_le (le_trans (e₁.map_add_le _ _) <| add_le_add (le_max_left _ _) (le_max_left _ _))
+          (le_trans (e₂.map_add_le _ _) <| add_le_add (le_max_right _ _) (le_max_right _ _))
+      map_smul_le' := fun c x => le_of_eq <| by simp only [map_smul, mul_max] }
+  le_sup_left := fun _ _ _ => le_max_left _ _
+  le_sup_right := fun _ _ _ => le_max_right _ _
+  sup_le := fun _ _ _ h₁ h₂ x => max_le (h₁ x) (h₂ x)
 
 @[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07"),
   simp, norm_cast]

Mathlib/Combinatorics/Digraph/Basic.lean

@@ -167,29 +167,20 @@ instance distribLattice : DistribLattice (Digraph V) :=
   { adj_injective.distribLattice Digraph.Adj (fun _ _ ↦ rfl) fun _ _ ↦ rfl with
     le := fun G H ↦ ∀ ⦃a b⦄, G.Adj a b → H.Adj a b }
 
-instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Digraph V) :=
-  { Digraph.distribLattice with
-    le := (· ≤ ·)
-    sup := (· ⊔ ·)
-    inf := (· ⊓ ·)
-    compl := HasCompl.compl
-    sdiff := (· \ ·)
-    top := Digraph.completeDigraph V
-    bot := Digraph.emptyDigraph V
-    le_top := fun _ _ _ _ ↦ trivial
-    bot_le := fun _ _ _ h ↦ h.elim
-    sdiff_eq := fun _ _ ↦ rfl
-    inf_compl_le_bot := fun _ _ _ h ↦ absurd h.1 h.2
-    top_le_sup_compl := fun G v w _ ↦ by tauto
-    sSup := sSup
-    le_sSup := fun _ G hG _ _ hab ↦ ⟨G, hG, hab⟩
-    sSup_le := fun s G hG a b ↦ by
-      rintro ⟨H, hH, hab⟩
-      exact hG _ hH hab
-    sInf := sInf
-    sInf_le := fun _ _ hG _ _ hab ↦ hab hG
-    le_sInf := fun _ _ hG _ _ hab ↦ fun _ hH ↦ hG _ hH hab
-    iInf_iSup_eq := fun f ↦ by ext; simp [Classical.skolem] }
+instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Digraph V) where
+  top := Digraph.completeDigraph V
+  bot := Digraph.emptyDigraph V
+  le_top _ _ _ _ := trivial
+  bot_le _ _ _ h := h.elim
+  inf_compl_le_bot _ _ _ h := absurd h.1 h.2
+  top_le_sup_compl G v w _ := by tauto
+  le_sSup _ G hG _ _ hab := ⟨G, hG, hab⟩
+  sSup_le s G hG a b := by
+    rintro ⟨H, hH, hab⟩
+    exact hG _ hH hab
+  sInf_le _ _ hG _ _ hab := hab hG
+  le_sInf _ _ hG _ _ hab _ hH := hG _ hH hab
+  iInf_iSup_eq f := by ext; simp [Classical.skolem]
 
 @[simp] theorem top_adj (v w : V) : (⊤ : Digraph V).Adj v w := trivial
 

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -296,37 +296,28 @@ instance distribLattice : DistribLattice (SimpleGraph V) :=
       adj_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl with
     le := fun G H => ∀ ⦃a b⦄, G.Adj a b → H.Adj a b }
 
-instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGraph V) :=
-  { SimpleGraph.distribLattice with
-    le := (· ≤ ·)
-    sup := (· ⊔ ·)
-    inf := (· ⊓ ·)
-    compl := HasCompl.compl
-    sdiff := (· \ ·)
-    top.Adj := Ne
-    bot.Adj _ _ := False
-    le_top := fun x _ _ h => x.ne_of_adj h
-    bot_le := fun _ _ _ h => h.elim
-    sdiff_eq := fun x y => by
-      ext v w
-      refine ⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩
-      rintro rfl
-      exact x.irrefl h.1
-    inf_compl_le_bot := fun _ _ _ h => False.elim <| h.2.2 h.1
-    top_le_sup_compl := fun G v w hvw => by
-      by_cases h : G.Adj v w
-      · exact Or.inl h
-      · exact Or.inr ⟨hvw, h⟩
-    sSup := sSup
-    le_sSup := fun _ G hG _ _ hab => ⟨G, hG, hab⟩
-    sSup_le := fun s G hG a b => by
-      rintro ⟨H, hH, hab⟩
-      exact hG _ hH hab
-    sInf := sInf
-    sInf_le := fun _ _ hG _ _ hab => hab.1 hG
-    le_sInf := fun _ _ hG _ _ hab => ⟨fun _ hH => hG _ hH hab, hab.ne⟩
-    iInf_iSup_eq := fun f => by ext; simp [Classical.skolem] }
-
+instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGraph V) where
+  top.Adj := Ne
+  bot.Adj _ _ := False
+  le_top x _ _ h := x.ne_of_adj h
+  bot_le _ _ _ h := h.elim
+  sdiff_eq x y := by
+    ext v w
+    refine ⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩
+    rintro rfl
+    exact x.irrefl h.1
+  inf_compl_le_bot _ _ _ h := False.elim <| h.2.2 h.1
+  top_le_sup_compl G v w hvw := by
+    by_cases h : G.Adj v w
+    · exact Or.inl h
+    · exact Or.inr ⟨hvw, h⟩
+  le_sSup _ G hG _ _ hab := ⟨G, hG, hab⟩
+  sSup_le s G hG a b := by
+    rintro ⟨H, hH, hab⟩
+    exact hG _ hH hab
+  sInf_le _ _ hG _ _ hab := hab.1 hG
+  le_sInf _ _ hG _ _ hab := ⟨fun _ hH => hG _ hH hab, hab.ne⟩
+  iInf_iSup_eq f := by ext; simp [Classical.skolem]
 /-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices. -/
 abbrev completeGraph (V : Type u) : SimpleGraph V := ⊤
 

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -438,35 +438,25 @@ instance distribLattice : DistribLattice G.Subgraph :=
     le := fun x y => x.verts ⊆ y.verts ∧ ∀ ⦃v w : V⦄, x.Adj v w → y.Adj v w }
 
 instance : BoundedOrder (Subgraph G) where
-  top := ⊤
-  bot := ⊥
   le_top x := ⟨Set.subset_univ _, fun _ _ => x.adj_sub⟩
   bot_le _ := ⟨Set.empty_subset _, fun _ _ => False.elim⟩
 
 /-- Note that subgraphs do not form a Boolean algebra, because of `verts`. -/
-def completelyDistribLatticeMinimalAxioms : CompletelyDistribLattice.MinimalAxioms G.Subgraph :=
-  { Subgraph.distribLattice with
-    le := (· ≤ ·)
-    sup := (· ⊔ ·)
-    inf := (· ⊓ ·)
-    top := ⊤
-    bot := ⊥
-    le_top := fun G' => ⟨Set.subset_univ _, fun _ _ => G'.adj_sub⟩
-    bot_le := fun _ => ⟨Set.empty_subset _, fun _ _ => False.elim⟩
-    sSup := sSup
-    -- Porting note: needed `apply` here to modify elaboration; previously the term itself was fine.
-    le_sSup := fun s G' hG' => ⟨by apply Set.subset_iUnion₂ G' hG', fun _ _ hab => ⟨G', hG', hab⟩⟩
-    sSup_le := fun s G' hG' =>
-      ⟨Set.iUnion₂_subset fun _ hH => (hG' _ hH).1, by
-        rintro a b ⟨H, hH, hab⟩
-        exact (hG' _ hH).2 hab⟩
-    sInf := sInf
-    sInf_le := fun _ G' hG' => ⟨Set.iInter₂_subset G' hG', fun _ _ hab => hab.1 hG'⟩
-    le_sInf := fun _ G' hG' =>
-      ⟨Set.subset_iInter₂ fun _ hH => (hG' _ hH).1, fun _ _ hab =>
-        ⟨fun _ hH => (hG' _ hH).2 hab, G'.adj_sub hab⟩⟩
-    iInf_iSup_eq := fun f => Subgraph.ext (by simpa using iInf_iSup_eq)
-      (by ext; simp [Classical.skolem]) }
+def completelyDistribLatticeMinimalAxioms : CompletelyDistribLattice.MinimalAxioms G.Subgraph where
+  le_top G' := ⟨Set.subset_univ _, fun _ _ => G'.adj_sub⟩
+  bot_le _ := ⟨Set.empty_subset _, fun _ _ => False.elim⟩
+  -- Porting note: needed `apply` here to modify elaboration; previously the term itself was fine.
+  le_sSup s G' hG' := ⟨by apply Set.subset_iUnion₂ G' hG', fun _ _ hab => ⟨G', hG', hab⟩⟩
+  sSup_le s G' hG' :=
+    ⟨Set.iUnion₂_subset fun _ hH => (hG' _ hH).1, by
+      rintro a b ⟨H, hH, hab⟩
+      exact (hG' _ hH).2 hab⟩
+  sInf_le _ G' hG' := ⟨Set.iInter₂_subset G' hG', fun _ _ hab => hab.1 hG'⟩
+  le_sInf _ G' hG' :=
+    ⟨Set.subset_iInter₂ fun _ hH => (hG' _ hH).1, fun _ _ hab =>
+      ⟨fun _ hH => (hG' _ hH).2 hab, G'.adj_sub hab⟩⟩
+  iInf_iSup_eq f := Subgraph.ext (by simpa using iInf_iSup_eq)
+    (by ext; simp [Classical.skolem])
 
 instance : CompletelyDistribLattice G.Subgraph :=
   .ofMinimalAxioms completelyDistribLatticeMinimalAxioms

Mathlib/Computability/Reduce.lean

@@ -372,7 +372,6 @@ private theorem le_trans {d₁ d₂ d₃ : ManyOneDegree} : d₁ ≤ d₂ → d
   apply ManyOneReducible.trans
 
 instance instPartialOrder : PartialOrder ManyOneDegree where
-  le := (· ≤ ·)
   le_refl := le_refl
   le_trans _ _ _ := le_trans
   le_antisymm _ _ := le_antisymm

Mathlib/Data/Finsupp/Lex.lean

@@ -80,8 +80,7 @@ instance Lex.partialOrder [PartialOrder N] : PartialOrder (Lex (α →₀ N)) wh
 
 /-- The linear order on `Finsupp`s obtained by the lexicographic ordering. -/
 instance Lex.linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N)) where
-  lt := (· < ·)
-  le := (· ≤ ·)
+  __ := Lex.partialOrder
   __ := LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective
 
 theorem Lex.single_strictAnti : StrictAnti fun (a : α) ↦ toLex (single a 1) := by