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

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
⊢ Surjective (g ∘ f)
Tactic:
rw [Surjective]
State after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
⊢ ∀ (y : Z), ∃ x, (g ∘ f) x = y

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

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

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
sorry
State after:
no goals