Theorem: gf_surjective (FM2023Exrcise/section03_functions/sheet3.lean)

State before:
⊢ Surjective (g ∘ f)
Tactic:
intro z
State after:
z : Z
⊢ ∃ a, (g ∘ f) a = z

State before:
z : Z
⊢ ∃ a, (g ∘ f) a = z
Tactic:
use X.a
State after:
no goals