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

State before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
⊢ Surjective g
Tactic:
intro z
State after:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
⊢ ∃ x, g x = z

State before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
⊢ ∃ x, g x = z
Tactic:
have ⟨x, hx⟩ := h z
State after:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
x : X
hx : (g ∘ f) x = z
⊢ ∃ x, g x = z

State before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
z : Z
x : X
hx : (g ∘ f) x = z
⊢ ∃ x, g x = z
Tactic:
exists f x
State after:
no goals