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>

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

Mathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -72,7 +72,7 @@ theorem hasDerivAtFilter_iff_tendsto_slope {x : 𝕜} {L : Filter 𝕜} :
 
 theorem hasDerivWithinAt_iff_tendsto_slope :
     HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f') := by
-  simp only [HasDerivWithinAt, nhdsWithin, diff_eq, inf_assoc.symm, inf_principal.symm]
+  simp only [HasDerivWithinAt, nhdsWithin, diff_eq, ← inf_assoc, inf_principal.symm]
   exact hasDerivAtFilter_iff_tendsto_slope
 #align has_deriv_within_at_iff_tendsto_slope hasDerivWithinAt_iff_tendsto_slope
 

Mathlib/Analysis/Normed/Order/Lattice.lean

@@ -100,7 +100,7 @@ theorem dual_solid (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) : ‖a‖ ≤ ‖b‖
   rw [← neg_inf]
   rw [abs]
   nth_rw 1 [← neg_neg b]
-  rwa [← neg_inf, neg_le_neg_iff, @inf_comm _ _ _ b, @inf_comm _ _ _ a]
+  rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]
 #align dual_solid dual_solid
 
 -- see Note [lower instance priority]
@@ -125,7 +125,7 @@ theorem norm_inf_sub_inf_le_add_norm (a b c d : α) : ‖a ⊓ b - c ⊓ d‖ 
     _ ≤ |a - c| + |b - d| := by
       apply add_le_add
       · exact abs_inf_sub_inf_le_abs _ _ _
-      · rw [@inf_comm _ _ c, @inf_comm _ _ c]
+      · rw [inf_comm c, inf_comm c]
         exact abs_inf_sub_inf_le_abs _ _ _
 #align norm_inf_sub_inf_le_add_norm norm_inf_sub_inf_le_add_norm
 
@@ -139,7 +139,7 @@ theorem norm_sup_sub_sup_le_add_norm (a b c d : α) : ‖a ⊔ b - c ⊔ d‖ 
     _ ≤ |a - c| + |b - d| := by
       apply add_le_add
       · exact abs_sup_sub_sup_le_abs _ _ _
-      · rw [@sup_comm _ _ c, @sup_comm _ _ c]
+      · rw [sup_comm c, sup_comm c]
         exact abs_sup_sub_sup_le_abs _ _ _
 #align norm_sup_sub_sup_le_add_norm norm_sup_sub_sup_le_add_norm
 

Mathlib/CategoryTheory/Generator.lean

@@ -338,7 +338,7 @@ theorem eq_of_isDetecting [HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 
     (P Q : Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q :=
   calc
     P = P ⊓ Q := Eq.symm <| inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).1 hf
-    _ = Q ⊓ P := inf_comm
+    _ = Q ⊓ P := inf_comm ..
     _ = Q := inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).2 hf
 
 #align category_theory.subobject.eq_of_is_detecting CategoryTheory.Subobject.eq_of_isDetecting

Mathlib/Computability/Language.lean

@@ -154,7 +154,7 @@ instance instSemiring : Semiring (Language α) where
 
 @[simp]
 theorem add_self (l : Language α) : l + l = l :=
-  sup_idem
+  sup_idem _
 #align language.add_self Language.add_self
 
 /-- Maps the alphabet of a language. -/

Mathlib/Data/DFinsupp/Order.lean

@@ -87,7 +87,7 @@ instance [∀ i, PartialOrder (α i)] : PartialOrder (Π₀ i, α i) :=
 
 instance [∀ i, SemilatticeInf (α i)] : SemilatticeInf (Π₀ i, α i) :=
   { (inferInstance : PartialOrder (DFinsupp α)) with
-    inf := zipWith (fun _ ↦ (· ⊓ ·)) fun _ ↦ inf_idem
+    inf := zipWith (fun _ ↦ (· ⊓ ·)) fun _ ↦ inf_idem _
     inf_le_left := fun _ _ _ ↦ inf_le_left
     inf_le_right := fun _ _ _ ↦ inf_le_right
     le_inf := fun _ _ _ hf hg i ↦ le_inf (hf i) (hg i) }
@@ -101,7 +101,7 @@ theorem inf_apply [∀ i, SemilatticeInf (α i)] (f g : Π₀ i, α i) (i : ι)
 
 instance [∀ i, SemilatticeSup (α i)] : SemilatticeSup (Π₀ i, α i) :=
   { (inferInstance : PartialOrder (DFinsupp α)) with
-    sup := zipWith (fun _ ↦ (· ⊔ ·)) fun _ ↦ sup_idem
+    sup := zipWith (fun _ ↦ (· ⊔ ·)) fun _ ↦ sup_idem _
     le_sup_left := fun _ _ _ ↦ le_sup_left
     le_sup_right := fun _ _ _ ↦ le_sup_right
     sup_le := fun _ _ _ hf hg i ↦ sup_le (hf i) (hg i) }

Mathlib/Data/ENNReal/Basic.lean

@@ -505,7 +505,7 @@ theorem iSup_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) :
 
 theorem iInf_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} :
     ⨅ n, f n = (⨅ n : ℝ≥0, f n) ⊓ f ∞ :=
-  (iInf_option f).trans inf_comm
+  (iInf_option f).trans (inf_comm _ _)
 #align ennreal.infi_ennreal ENNReal.iInf_ennreal
 
 theorem iSup_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} :

Mathlib/Data/Finset/Basic.lean

@@ -1457,24 +1457,21 @@ theorem union_subset_union_right (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂
   union_subset_union Subset.rfl h
 #align finset.union_subset_union_right Finset.union_subset_union_right
 
-theorem union_comm (s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
-  sup_comm
+theorem union_comm (s₁ s₂ : Finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ := sup_comm _ _
 #align finset.union_comm Finset.union_comm
 
 instance : Std.Commutative (α := Finset α) (· ∪ ·) :=
   ⟨union_comm⟩
 
 @[simp]
-theorem union_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
-  sup_assoc
+theorem union_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := sup_assoc _ _ _
 #align finset.union_assoc Finset.union_assoc
 
 instance : Std.Associative (α := Finset α) (· ∪ ·) :=
   ⟨union_assoc⟩
 
 @[simp]
-theorem union_idempotent (s : Finset α) : s ∪ s = s :=
-  sup_idem
+theorem union_idempotent (s : Finset α) : s ∪ s = s := sup_idem _
 #align finset.union_idempotent Finset.union_idempotent
 
 instance : Std.IdempotentOp (α := Finset α) (· ∪ ·) :=
@@ -1788,39 +1785,35 @@ instance : DistribLattice (Finset α) :=
         or_imp, true_or_iff, imp_true_iff, true_and_iff, or_true_iff] }
 
 @[simp]
-theorem union_left_idem (s t : Finset α) : s ∪ (s ∪ t) = s ∪ t :=
-  sup_left_idem
+theorem union_left_idem (s t : Finset α) : s ∪ (s ∪ t) = s ∪ t := sup_left_idem _ _
 #align finset.union_left_idem Finset.union_left_idem
 
 -- Porting note: @[simp] can prove this
-theorem union_right_idem (s t : Finset α) : s ∪ t ∪ t = s ∪ t :=
-  sup_right_idem
+theorem union_right_idem (s t : Finset α) : s ∪ t ∪ t = s ∪ t := sup_right_idem _ _
 #align finset.union_right_idem Finset.union_right_idem
 
 @[simp]
-theorem inter_left_idem (s t : Finset α) : s ∩ (s ∩ t) = s ∩ t :=
-  inf_left_idem
+theorem inter_left_idem (s t : Finset α) : s ∩ (s ∩ t) = s ∩ t := inf_left_idem _ _
 #align finset.inter_left_idem Finset.inter_left_idem
 
 -- Porting note: @[simp] can prove this
-theorem inter_right_idem (s t : Finset α) : s ∩ t ∩ t = s ∩ t :=
-  inf_right_idem
+theorem inter_right_idem (s t : Finset α) : s ∩ t ∩ t = s ∩ t := inf_right_idem _ _
 #align finset.inter_right_idem Finset.inter_right_idem
 
 theorem inter_distrib_left (s t u : Finset α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u :=
-  inf_sup_left
+  inf_sup_left _ _ _
 #align finset.inter_distrib_left Finset.inter_distrib_left
 
 theorem inter_distrib_right (s t u : Finset α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u :=
-  inf_sup_right
+  inf_sup_right _ _ _
 #align finset.inter_distrib_right Finset.inter_distrib_right
 
 theorem union_distrib_left (s t u : Finset α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u) :=
-  sup_inf_left
+  sup_inf_left _ _ _
 #align finset.union_distrib_left Finset.union_distrib_left
 
 theorem union_distrib_right (s t u : Finset α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u) :=
-  sup_inf_right
+  sup_inf_right _ _ _
 #align finset.union_distrib_right Finset.union_distrib_right
 
 theorem union_union_distrib_left (s t u : Finset α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u) :=