trans D
case right
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ C ∪ D
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ D

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