Theorem: Set.subset_tetraunion₄ (Logic/Vorspiel/Vorspiel.lean)

State before:
F : Type u_1
s₁ s₂ s₃ s₄ : Set F
⊢ s₄ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄
Tactic:
simp only [subset_union_right]
State after:
no goals