Theorem: Section3sheet1solutions.gf_surjective (FormalisingMathematics2024/Solutions/Section03functions/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