refactor(data/set/basic): simpler proof of union_subset_iff (#5904)

12X smaller proof term

co-authors: `lean-gptf`, Stanislas Polu

src/data/set/basic.lean

@@ -469,7 +469,7 @@ theorem union_subset {s t r : set α} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t 
 by finish [subset_def, union_def]
 
 @[simp] theorem union_subset_iff {s t u : set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
-by finish [iff_def, subset_def]
+by simp only [subset_def, or_imp_distrib, forall_and_distrib, mem_union_eq, iff_self]
 
 theorem union_subset_union {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) : s₁ ∪ t₁ ⊆ s₂ ∪ t₂ :=
 by finish [subset_def]