Theorem: F1 (LeanTeaching/Ex2/2.lean)

State before:
⊢ Surjective fun n => n + 5
Tactic:
sorry
State after:
no goals