Theorem: S3 (LeanTeaching/Ex2/4.lean)

State before:
α β : Type
f✝ : α → β
t✝ : Set α
f : α → β
s : Set β
t : Set α
⊢ t ∪ f ⁻¹' s ⊆ f ⁻¹' (f '' t ∪ s)
Tactic:
sorry
State after:
no goals