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

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