Theorem: Tutorial.Surjective.comp (Solution/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:
have ⟨x, hx⟩ := hfsurj y
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 : X
hx : f x = y
⊢ ∃ 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 : X
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z
Tactic:
exists x
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 : X
hx : f x = y
⊢ (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 : X
hx : f x = y
⊢ (g ∘ f) x = z
Tactic:
simp
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 : X
hx : f x = y
⊢ 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 : X
hx : f x = y
⊢ g (f x) = z
Tactic:
rw [hx, hy]
State after:
no goals