missing transitivity tags

Stream: general

[Johan Commelin]

Should all of these be tagged with @[trans]? Or is there a reason to only do that for sets?

git grep "subset.trans" | grep theorem
src/data/finset.lean:theorem subset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := subset.trans
src/data/multiset.lean:theorem subset.trans {s t u : multiset α} : s ⊆ t → t ⊆ u → s ⊆ u :=
src/data/set/basic.lean:@[trans] theorem subset.trans {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c :=
src/set_theory/lists.lean:theorem subset.trans {l₁ l₂ l₃ : lists' α tt}

[Kevin Buzzard]

This takes us back to Chris' point. If we just used le and make them partial orders then le_trans would kick in.