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

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