Theorem: Tutorial.Surjective.of_comp (Tutorial/Basic/Lecture4.lean)

State before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
⊢ Surjective g
Tactic:
sorry
State after:
no goals