Theorem: Set.subset_triunion₃ (Logic/Vorspiel/Vorspiel.lean)

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