open Or in intro
| inl ⟨hs, ht⟩ => constructor; exact hs; left; exact ht
| inr ⟨hs, hu⟩ => constructor; exact hs; right; exact hu
case a.mpr
α : Sort u_1
β : ?m.21867
γ : ?m.21870
s t u : Set α
x : α
⊢ x ∈ (s.inter t).union (s.inter u) → x ∈ s.inter (t.union u)
no goals