chore(Order): Make more arguments explicit (#11033)

Those lemmas have historically been very annoying to use in `rw` since all their arguments were implicit. One too many people complained about it on Zulip, so I'm changing them.

Downstream code broken by this change can fix it by adding appropriately many `_`s.

Also marks `CauSeq.ext` `@[ext]`.

## `Order.BoundedOrder`

* `top_sup_eq`
* `sup_top_eq`
* `bot_sup_eq`
* `sup_bot_eq`
* `top_inf_eq`
* `inf_top_eq`
* `bot_inf_eq`
* `inf_bot_eq`

## `Order.Lattice`

* `sup_idem`
* `sup_comm`
* `sup_assoc`
* `sup_left_idem`
* `sup_right_idem`
* `inf_idem`
* `inf_comm`
* `inf_assoc`
* `inf_left_idem`
* `inf_right_idem`
* `sup_inf_left`
* `sup_inf_right`
* `inf_sup_left`
* `inf_sup_right`

## `Order.MinMax`

* `max_min_distrib_left`
* `max_min_distrib_right`
* `min_max_distrib_left`
* `min_max_distrib_right`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: YaelDillies

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -528,11 +528,11 @@ instance completeLattice : CompleteLattice (LieSubalgebra R L) :=
 instance addCommMonoid : AddCommMonoid (LieSubalgebra R L)
     where
   add := (· ⊔ ·)
-  add_assoc _ _ _ := sup_assoc
+  add_assoc := sup_assoc
   zero := ⊥
-  zero_add _ := bot_sup_eq
-  add_zero _ := sup_bot_eq
-  add_comm _ _ := sup_comm
+  zero_add := bot_sup_eq
+  add_zero := sup_bot_eq
+  add_comm := sup_comm
 
 instance : CanonicallyOrderedAddCommMonoid (LieSubalgebra R L) :=
   { LieSubalgebra.addCommMonoid,

Mathlib/Algebra/Lie/Submodule.lean

@@ -558,11 +558,11 @@ theorem iSup_eq_top_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R
 
 instance : AddCommMonoid (LieSubmodule R L M) where
   add := (· ⊔ ·)
-  add_assoc _ _ _ := sup_assoc
+  add_assoc := sup_assoc
   zero := ⊥
-  zero_add _ := bot_sup_eq
-  add_zero _ := sup_bot_eq
-  add_comm _ _ := sup_comm
+  zero_add := bot_sup_eq
+  add_zero := sup_bot_eq
+  add_comm := sup_comm
 
 @[simp]
 theorem add_eq_sup : N + N' = N ⊔ N' :=

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -167,11 +167,11 @@ variable [Semiring R] [AddCommMonoid M] [Module R M]
 instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M)
     where
   add := (· ⊔ ·)
-  add_assoc _ _ _ := sup_assoc
+  add_assoc := sup_assoc
   zero := ⊥
-  zero_add _ := bot_sup_eq
-  add_zero _ := sup_bot_eq
-  add_comm _ _ := sup_comm
+  zero_add := bot_sup_eq
+  add_zero := sup_bot_eq
+  add_comm := sup_comm
 #align submodule.pointwise_add_comm_monoid Submodule.pointwiseAddCommMonoid
 
 @[simp]

Mathlib/Algebra/Order/CauSeq/Basic.lean

@@ -181,8 +181,8 @@ theorem mk_to_fun (f) (hf : IsCauSeq abv f) : @coeFn (CauSeq β abv) _ _ ⟨f, h
   rfl -/
 #noalign cau_seq.mk_to_fun
 
-theorem ext {f g : CauSeq β abv} (h : ∀ i, f i = g i) : f = g :=
-  Subtype.eq (funext h)
+@[ext]
+theorem ext {f g : CauSeq β abv} (h : ∀ i, f i = g i) : f = g := Subtype.eq (funext h)
 #align cau_seq.ext CauSeq.ext
 
 theorem isCauSeq (f : CauSeq β abv) : IsCauSeq abv f :=
@@ -904,21 +904,17 @@ protected theorem lt_inf {a b c : CauSeq α abs} (hb : a < b) (hc : a < c) : a <
 #align cau_seq.lt_inf CauSeq.lt_inf
 
 @[simp]
-protected theorem sup_idem (a : CauSeq α abs) : a ⊔ a = a :=
-  Subtype.ext sup_idem
+protected theorem sup_idem (a : CauSeq α abs) : a ⊔ a = a := Subtype.ext (sup_idem _)
 #align cau_seq.sup_idem CauSeq.sup_idem
 
 @[simp]
-protected theorem inf_idem (a : CauSeq α abs) : a ⊓ a = a :=
-  Subtype.ext inf_idem
+protected theorem inf_idem (a : CauSeq α abs) : a ⊓ a = a := Subtype.ext (inf_idem _)
 #align cau_seq.inf_idem CauSeq.inf_idem
 
-protected theorem sup_comm (a b : CauSeq α abs) : a ⊔ b = b ⊔ a :=
-  Subtype.ext sup_comm
+protected theorem sup_comm (a b : CauSeq α abs) : a ⊔ b = b ⊔ a := Subtype.ext (sup_comm _ _)
 #align cau_seq.sup_comm CauSeq.sup_comm
 
-protected theorem inf_comm (a b : CauSeq α abs) : a ⊓ b = b ⊓ a :=
-  Subtype.ext inf_comm
+protected theorem inf_comm (a b : CauSeq α abs) : a ⊓ b = b ⊓ a := Subtype.ext (inf_comm _ _)
 #align cau_seq.inf_comm CauSeq.inf_comm
 
 protected theorem sup_eq_right {a b : CauSeq α abs} (h : a ≤ b) : a ⊔ b ≈ b := by
@@ -998,11 +994,11 @@ protected theorem le_inf {a b c : CauSeq α abs} (hb : a ≤ b) (hc : a ≤ c) :
 
 
 protected theorem sup_inf_distrib_left (a b c : CauSeq α abs) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) :=
-  Subtype.ext <| funext fun _ => max_min_distrib_left
+  ext fun _ ↦ max_min_distrib_left _ _ _
 #align cau_seq.sup_inf_distrib_left CauSeq.sup_inf_distrib_left
 
 protected theorem sup_inf_distrib_right (a b c : CauSeq α abs) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=
-  Subtype.ext <| funext fun _ => max_min_distrib_right
+  ext fun _ ↦ max_min_distrib_right _ _ _
 #align cau_seq.sup_inf_distrib_right CauSeq.sup_inf_distrib_right
 
 end Abs

Mathlib/Algebra/Order/Group/Abs.lean

@@ -193,8 +193,8 @@ lemma mabs_div_sup_mul_mabs_div_inf [CovariantClass α α (· * ·) (· ≤ ·)]
     _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
         rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
     _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
-        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, @sup_comm _ _ c (a ⊔ c), sup_right_idem,
-          sup_assoc, inf_assoc, @inf_comm _ _ c (a ⊓ c), inf_right_idem, inf_assoc]
+        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
+          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
     _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
     _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
         rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]

Mathlib/Algebra/Order/Group/PosPart.lean

@@ -92,7 +92,7 @@ def leOnePart (a : α) : α := a⁻¹ ⊔ 1
 @[to_additive] lemma leOnePart_anti : Antitone (leOnePart : α → α) :=
   fun _a _b hab ↦ sup_le_sup_right (inv_le_inv_iff.2 hab) _
 
-@[to_additive (attr := simp)] lemma oneLePart_one : (1 : α)⁺ᵐ = 1 := sup_idem
+@[to_additive (attr := simp)] lemma oneLePart_one : (1 : α)⁺ᵐ = 1 := sup_idem _
 #align lattice_ordered_comm_group.pos_one oneLePart_one
 #align lattice_ordered_comm_group.pos_zero posPart_zero
 
@@ -186,7 +186,7 @@ lemma oneLePart_mul_leOnePart
     [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)] (a : α) :
     a⁺ᵐ * a⁻ᵐ = |a|ₘ := by
   rw [oneLePart, sup_mul, one_mul, leOnePart, mul_sup, mul_one, mul_inv_self, sup_assoc,
-    ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
+    ← sup_assoc a, sup_eq_right.2 le_sup_right]
   exact sup_eq_left.2 <| one_le_mabs a
 #align lattice_ordered_comm_group.pos_mul_neg oneLePart_mul_leOnePart
 #align lattice_ordered_comm_group.pos_add_neg posPart_add_negPart

Mathlib/Algebra/Order/Support.lean

@@ -24,14 +24,14 @@ variable [One M]
 @[to_additive]
 lemma mulSupport_sup [SemilatticeSup M] (f g : α → M) :
     mulSupport (fun x ↦ f x ⊔ g x) ⊆ mulSupport f ∪ mulSupport g :=
-  mulSupport_binop_subset (· ⊔ ·) sup_idem f g
+  mulSupport_binop_subset (· ⊔ ·) (sup_idem _) f g
 #align function.mul_support_sup Function.mulSupport_sup
 #align function.support_sup Function.support_sup
 
 @[to_additive]
 lemma mulSupport_inf [SemilatticeInf M] (f g : α → M) :
     mulSupport (fun x ↦ f x ⊓ g x) ⊆ mulSupport f ∪ mulSupport g :=
-  mulSupport_binop_subset (· ⊓ ·) inf_idem f g
+  mulSupport_binop_subset (· ⊓ ·) (inf_idem _) f g
 #align function.mul_support_inf Function.mulSupport_inf
 #align function.support_inf Function.support_inf
 

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -442,14 +442,14 @@ def GeneralizedBooleanAlgebra.toNonUnitalCommRing [GeneralizedBooleanAlgebra α]
   zero := ⊥
   zero_add := bot_symmDiff
   add_zero := symmDiff_bot
-  zero_mul _ := bot_inf_eq
-  mul_zero _ := inf_bot_eq
+  zero_mul := bot_inf_eq
+  mul_zero := inf_bot_eq
   neg := id
   add_left_neg := symmDiff_self
   add_comm := symmDiff_comm
   mul := (· ⊓ ·)
-  mul_assoc _ _ _ := inf_assoc
-  mul_comm _ _ := inf_comm
+  mul_assoc := inf_assoc
+  mul_comm := inf_comm
   left_distrib := inf_symmDiff_distrib_left
   right_distrib := inf_symmDiff_distrib_right
 #align generalized_boolean_algebra.to_non_unital_comm_ring GeneralizedBooleanAlgebra.toNonUnitalCommRing
@@ -469,12 +469,12 @@ variable [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ]
 * `1` unfolds to `⊤`
 -/
 @[reducible]
-def BooleanAlgebra.toBooleanRing : BooleanRing α :=
-  { GeneralizedBooleanAlgebra.toNonUnitalCommRing with
-    one := ⊤
-    one_mul := fun _ => top_inf_eq
-    mul_one := fun _ => inf_top_eq
-    mul_self := fun b => inf_idem }
+def BooleanAlgebra.toBooleanRing : BooleanRing α where
+  __ := GeneralizedBooleanAlgebra.toNonUnitalCommRing
+  one := ⊤
+  one_mul := top_inf_eq
+  mul_one := inf_top_eq
+  mul_self := inf_idem
 #align boolean_algebra.to_boolean_ring BooleanAlgebra.toBooleanRing
 
 scoped[BooleanRingOfBooleanAlgebra]

Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

@@ -266,7 +266,7 @@ lemma XYIdeal_mul_XYIdeal {x₁ x₂ y₁ y₂ : F} (h₁ : W.equation x₁ y₁
         XYIdeal W (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)
           (C <| W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) := by
   have sup_rw : ∀ a b c d : Ideal W.CoordinateRing, a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c :=
-    fun _ _ c _ => by rw [← sup_assoc, @sup_comm _ _ c, sup_sup_sup_comm, ← sup_assoc]
+    fun _ _ c _ => by rw [← sup_assoc, sup_comm c, sup_sup_sup_comm, ← sup_assoc]
   rw [XYIdeal_add_eq, XIdeal, mul_comm, XYIdeal_eq₁ W x₁ y₁ <| W.slope x₁ x₂ y₁ y₂, XYIdeal,
     XYIdeal_eq₂ h₁ h₂ hxy, XYIdeal, span_pair_mul_span_pair]
   simp_rw [span_insert, sup_rw, Ideal.sup_mul, span_singleton_mul_span_singleton]

Mathlib/AlgebraicGeometry/Properties.lean

@@ -165,7 +165,7 @@ theorem eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : Opens X
     specialize H (X.presheaf.map i.op s)
     erw [Scheme.basicOpen_res] at H
     rw [hs] at H
-    specialize H inf_bot_eq ⟨x, hx⟩
+    specialize H (inf_bot_eq _) ⟨x, hx⟩
     erw [TopCat.Presheaf.germ_res_apply] at H
     exact H
   · rintro X Y f hf