chore(order/bounded_lattice): use ⦃⦄ in disjoint.symm (#3893)

src/data/set/disjointed.lean

@@ -32,7 +32,7 @@ by simpa [pairwise, function.on_fun] using @hr a b
 
 theorem pairwise_disjoint_on_bool [semilattice_inf_bot α] {a b : α} :
   pairwise (disjoint on (λ c, cond c a b)) ↔ disjoint a b :=
-pairwise_on_bool $ λ _ _, disjoint.symm
+pairwise_on_bool disjoint.symm
 
 theorem pairwise.pairwise_on {p : α → α → Prop} (h : pairwise p) (s : set α) : s.pairwise_on p :=
 λ x hx y hy, h x y

src/order/bounded_lattice.lean

@@ -916,7 +916,7 @@ eq_bot_iff.symm
 theorem disjoint.comm {a b : α} : disjoint a b ↔ disjoint b a :=
 by rw [disjoint, disjoint, inf_comm]
 
-@[symm] theorem disjoint.symm {a b : α} : disjoint a b → disjoint b a :=
+@[symm] theorem disjoint.symm ⦃a b : α⦄ : disjoint a b → disjoint b a :=
 disjoint.comm.1
 
 @[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq