## Stream: new members

### Topic: Composing surjections, proof using pattern matching

#### Martin C. Martin (Aug 04 2022 at 21:02):

The first exercise in Chapter 8 of Theorem proving in Lean is "Use pattern matching to prove that the composition of surjective functions is surjective:

open function

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

lemma surjective_comp {g : β → γ} {f : α → β}
(hg : surjective g) (hf : surjective f) :
surjective (g ∘ f) := sorry


Here's what I have, which is incomplete, and I feel like I'm barking up the wrong tree:

lemma surjective_comp {g : β → γ} {f : α → β}
(hg : surjective g) (hf : surjective f) :
surjective (g ∘ f)
| c := exists.elim (hg c)
(assume b hgb, exists.elim (hf b) (assume a hfa, exists.intro a sorry))


I just used the pattern matching to get c, can it be used for more of the proof? Can the proof be simplified further, hopefully leveraging the pattern matching in a way I'm not seeing, but otherwise using tactics or something?

#### Alex J. Best (Aug 04 2022 at 23:40):

Here's a pattern matching solution, no idea what is intended:

lemma surjective_comp {g : β → γ} {f : α → β}
(hg : surjective g) (hf : surjective f) :
surjective (g ∘ f)
| x := match hg x with
| ⟨y, hy⟩ := match hf y with
| ⟨z, hz⟩ := ⟨z, by rw [← hy, ← hz]⟩
end
end


BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

#### Martin C. Martin (Aug 05 2022 at 01:22):

Alex J. Best said:

BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

Perhaps copilot is the new stack overflow. :) Thanks Alex.

Last updated: Dec 20 2023 at 11:08 UTC