exact Finset.union_subset_left_right (A \ E) (B \ E) C D h1 h2
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ C ∪ D
no goals