feat(data/set/basic): allow dot notation for trans and antisymm (#7681)

Allow to write
```lean
example {α : Type*} {a b c : set α} (h : a ⊆ b)  (h': b ⊆ c) : a ⊆ c :=
h.trans h'

example {α : Type*} {a b : set α} (h : a ⊆ b)  (h': b ⊆ a) : 
  a = b := h.antisymm h'

example {α : Type*} {a b c : finset α} (h : a ⊆ b)  (h': b ⊆ c) : a ⊆ c :=
h.trans h'

example {α : Type*} {a b : finset α} (h : a ⊆ b)  (h': b ⊆ a) : a = b :=
h.antisymm h'
```

src/data/set/basic.lean

@@ -81,6 +81,18 @@ universe variables u v w x
 run_cmd do e ← tactic.get_env,
   tactic.set_env $ e.mk_protected `set.compl
 
+lemma has_subset.subset.trans {α : Type*} [has_subset α] [is_trans α (⊆)]
+  {a b c : α} (h : a ⊆ b) (h' : b ⊆ c) : a ⊆ c := trans h h'
+
+lemma has_subset.subset.antisymm {α : Type*} [has_subset α] [is_antisymm α (⊆)]
+  {a b : α} (h : a ⊆ b) (h' : b ⊆ a) : a = b := antisymm h h'
+
+lemma has_ssubset.ssubset.trans {α : Type*} [has_ssubset α] [is_trans α (⊂)]
+  {a b c : α} (h : a ⊂ b) (h' : b ⊂ c) : a ⊂ c := trans h h'
+
+lemma has_ssubset.ssubset.asymm {α : Type*} [has_ssubset α] [is_asymm α (⊂)]
+  {a b : α} (h : a ⊂ b) : ¬(b ⊂ a) := asymm h
+
 namespace set
 
 variable {α : Type*}