Theorem: Set.subset_union_three₁ (Arithmetization/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
s t u : Set α
⊢ s ⊆ s ∪ t
Tactic:
simp
State after:
no goals