Theorem: Section3sheet1.gf_surjective (FormalisingMathematics2024/Section03functions/Sheet3.lean)

State before:
⊢ Surjective (g ∘ f)
Tactic:
sorry
State after:
no goals