. intro ⟨s, h, _⟩
  induction l with
  | nil => contradiction
  | cons _ _ ih =>
    simp at h
    cases h <;> simp
    case inl h =>
      apply Or.inl; rw [<- h]
      assumption
    case inr _ =>
      apply Or.inr
      apply ih
      assumption
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
no goals