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

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