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_triunion₂]
State after:
no goals