trans C \ E
case left
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ C \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C \ E ⊆ (C ∪ D) \ E