intro
| Or.inl hs₁ =>
  left
  exact hs x hs₁
| Or.inr ht₁ =>
  right
  exact ht x ht₁
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂
no goals